diff --git a/regression/verilog/SVA/always_with_range1.desc b/regression/verilog/SVA/always_with_range1.desc index 6f3d73896..4d68ce32b 100644 --- a/regression/verilog/SVA/always_with_range1.desc +++ b/regression/verilog/SVA/always_with_range1.desc @@ -1,9 +1,9 @@ CORE always_with_range1.sv --bound 20 -^\[main\.property\.1\] always \[0:9\] main\.x < 10: PROVED up to bound 20$ -^\[main\.property\.2\] always \[0:\$\] main\.x < 10: REFUTED$ -^\[main\.property\.3\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$ +^\[main\.property\.p0\] always \[0:9\] main\.x < 10: PROVED up to bound 20$ +^\[main\.property\.p1\] always \[0:\$\] main\.x < 10: REFUTED$ +^\[main\.property\.p2\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/cover2.desc b/regression/verilog/SVA/cover2.desc index 882140a8d..b418d1cef 100644 --- a/regression/verilog/SVA/cover2.desc +++ b/regression/verilog/SVA/cover2.desc @@ -1,11 +1,11 @@ CORE cover2.sv --bound 10 --numbered-trace -^\[main\.property\.1\] cover main\.counter == 1: PROVED$ +^\[main\.property\.p0\] cover main\.counter == 1: PROVED$ ^Trace with 2 states:$ ^main\.counter@0 = 0$ ^main\.counter@1 = 1$ -^\[main\.property\.2\] cover main\.counter == 100: REFUTED up to bound 10$ +^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 10$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/initial1.desc b/regression/verilog/SVA/initial1.desc index a8c48a345..01f6bca09 100644 --- a/regression/verilog/SVA/initial1.desc +++ b/regression/verilog/SVA/initial1.desc @@ -1,11 +1,11 @@ CORE initial1.sv --module main --bound 1 -^\[main\.property\.1\] main\.counter == 0: PROVED up to bound 1$ -^\[main\.property\.2\] main\.counter == 100: REFUTED$ -^\[main\.property\.3\] ##1 main\.counter == 1: PROVED up to bound 1$ -^\[main\.property\.4\] ##1 main\.counter == 100: REFUTED$ -^\[main\.property\.5\] s_nexttime main\.counter == 1: PROVED up to bound 1$ +^\[main\.property\.p0\] main\.counter == 0: PROVED up to bound 1$ +^\[main\.property\.p1\] main\.counter == 100: REFUTED$ +^\[main\.property\.p2\] ##1 main\.counter == 1: PROVED up to bound 1$ +^\[main\.property\.p3\] ##1 main\.counter == 100: REFUTED$ +^\[main\.property\.p4\] s_nexttime main\.counter == 1: PROVED up to bound 1$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/initial1.sv b/regression/verilog/SVA/initial1.sv index 7bb6a06a7..0520f2e57 100644 --- a/regression/verilog/SVA/initial1.sv +++ b/regression/verilog/SVA/initial1.sv @@ -21,9 +21,9 @@ module main(input clk); initial p2: assert property (##1 counter == 1); // expected to fail - initial p2: assert property (##1 counter == 100); + initial p3: assert property (##1 counter == 100); // expected to pass if there are timeframes 0 and 1 - initial p3: assert property (s_nexttime counter == 1); + initial p4: assert property (s_nexttime counter == 1); endmodule diff --git a/regression/verilog/SVA/sequence1.desc b/regression/verilog/SVA/sequence1.desc index e1d993b6c..0df063cdc 100644 --- a/regression/verilog/SVA/sequence1.desc +++ b/regression/verilog/SVA/sequence1.desc @@ -1,7 +1,7 @@ CORE sequence1.sv --bound 20 --numbered-trace -^\[main\.property\.1\] ##\[0:9\] main\.x == 100: REFUTED$ +^\[main\.property\.p0\] ##\[0:9\] main\.x == 100: REFUTED$ ^Counterexample with 10 states:$ ^main\.x@0 = 0$ ^main\.x@9 = 9$ diff --git a/regression/verilog/SVA/sequence2.desc b/regression/verilog/SVA/sequence2.desc index 07bda663c..3f50b5054 100644 --- a/regression/verilog/SVA/sequence2.desc +++ b/regression/verilog/SVA/sequence2.desc @@ -1,7 +1,7 @@ CORE sequence2.sv --bound 10 --numbered-trace -^\[main\.property\.1] ##\[0:\$\] main\.x == 10: REFUTED$ +^\[main\.property\.p0] ##\[0:\$\] main\.x == 10: REFUTED$ ^Counterexample with 7 states:$ ^main\.x@0 = 0$ ^main\.x@1 = 1$ diff --git a/regression/verilog/SVA/sequence3.desc b/regression/verilog/SVA/sequence3.desc index 31647fa6f..d301c6a3a 100644 --- a/regression/verilog/SVA/sequence3.desc +++ b/regression/verilog/SVA/sequence3.desc @@ -1,9 +1,9 @@ CORE sequence3.sv --bound 20 --numbered-trace -^\[main\.property\.1\] ##\[\*\] main\.x == 6: REFUTED$ +^\[main\.property\.p0\] ##\[\*\] main\.x == 6: REFUTED$ ^Counterexample with 2 states:$ -^\[main\.property\.2\] ##\[\+\] main\.x == 0: REFUTED$ +^\[main\.property\.p1\] ##\[\+\] main\.x == 0: REFUTED$ ^Counterexample with 7 states:$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 4b873188d..9695e6fb9 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1481,7 +1481,21 @@ void verilog_typecheckt::convert_statement( else if(statement.id()==ID_force) convert_force(to_verilog_force(statement)); else if(statement.id() == ID_verilog_label_statement) - convert_statement(to_verilog_label_statement(statement).statement()); + { + // We stick the label on any assert/assume/conver statement + auto &label_statement = to_verilog_label_statement(statement); + auto &sub_statement = label_statement.statement(); + + if( + sub_statement.id() == ID_verilog_assert_property || + sub_statement.id() == ID_verilog_assume_property || + sub_statement.id() == ID_verilog_cover_property) + { + sub_statement.set(ID_identifier, label_statement.label()); + } + + convert_statement(sub_statement); + } else if(statement.id() == ID_wait) { }