From a6a73c2735404e1a698e588a7a315289bd48aab5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 19 Jun 2025 14:44:56 +0900 Subject: [PATCH] word-level BMC: precondition for timeframe This adds a PRECONDITION on the starting timeframe to the word-level SVA sequence encoding. --- src/trans-word-level/sequence.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp index 62d5567ed..2dc4a020f 100644 --- a/src/trans-word-level/sequence.cpp +++ b/src/trans-word-level/sequence.cpp @@ -82,6 +82,8 @@ sequence_matchest instantiate_sequence( const mp_integer &t, const mp_integer &no_timeframes) { + PRECONDITION(t < no_timeframes); + if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something { auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr);