From eb6ba55bf165711fe29c73b2010e81f8b5445d2c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 23 Jun 2024 11:16:30 -0700 Subject: [PATCH] SystemVerilog: concurrent assertion items go into module namespace Concurrent assertion items (assert/assume/cover) that are module items with a block label go into the module name space, not into a separate "property" name space. Assertion items without block item now get a label based on the kind of the assertion item (assert/assume/cover). --- regression/ebmc/BDD/BDD2.desc | 4 ++-- regression/ebmc/BDD/BDD3.desc | 4 ++-- regression/ebmc/BDD/BDD_SVA1.desc | 18 +++++++++--------- regression/ebmc/Next-in-Property1/test.desc | 2 +- regression/ebmc/SVA-LTL/freeze.desc | 4 ++-- .../ebmc/SVA-LTL/lasso1-counterexample.desc | 2 +- .../ebmc/SVA-LTL/lasso1-small-bound.desc | 2 +- .../simple_counterexamples_to_Fp.p0.desc | 4 ++-- .../simple_counterexamples_to_Fp.p1.desc | 4 ++-- .../simple_counterexamples_to_Fp.p2.desc | 4 ++-- .../SVA-LTL/simple_passing_LTL_properties.desc | 18 +++++++++--------- regression/ebmc/example3/test.desc | 4 ++-- regression/ebmc/example4_reset/test.desc | 4 ++-- regression/ebmc/example4_trace/test.desc | 4 ++-- regression/ebmc/ic3/bobmiterbm1multi.1033.desc | 2 +- regression/ebmc/ic3/bobmiterbm1multi.1080.desc | 2 +- regression/ebmc/ic3/non_inductive1.desc | 2 +- regression/ebmc/ic3/not_supported1.desc | 2 +- regression/ebmc/ic3/sm98a7multi.desc | 2 +- .../k-induction/k-induction-unsupported2.desc | 4 ++-- regression/ebmc/k-induction/k-induction4.desc | 2 +- .../ebmc/liveness-to-safety/failing1.desc | 2 +- .../ebmc/liveness-to-safety/failing1.k-1.desc | 2 +- .../ebmc/liveness-to-safety/failing2.desc | 4 ++-- .../ebmc/liveness-to-safety/failing2.k-6.desc | 4 ++-- .../ebmc/liveness-to-safety/passing1.desc | 2 +- .../ebmc/liveness-to-safety/passing1.k-10.desc | 2 +- .../ebmc/liveness-to-safety/passing2.desc | 4 ++-- .../ebmc/liveness-to-safety/passing2.k-10.desc | 4 ++-- regression/ebmc/netlist/netlist-trace1.desc | 2 +- regression/ebmc/neural-liveness/counter1.desc | 2 +- .../ebmc/ranking-function/clock24h.day.desc | 4 ++-- .../ebmc/ranking-function/clock24h.hour.desc | 4 ++-- .../ebmc/ranking-function/clock24h.minute.desc | 4 ++-- .../ebmc/ranking-function/counter1.fail.desc | 2 +- .../ebmc/ranking-function/counter1.pass.desc | 2 +- .../ebmc/ranking-function/counter2.fail.desc | 2 +- .../ebmc/ranking-function/counter2.pass.desc | 2 +- .../ranking-function/counter_in_module1.desc | 2 +- .../counter_with_reset1.fail.desc | 4 ++-- .../counter_with_reset1.pass.desc | 4 ++-- .../lexicographic_ranking_function1.desc | 2 +- regression/ebmc/ranking-function/signed1.desc | 2 +- .../ebmc/ring_buffer_induction/test.desc | 6 +++--- regression/verilog/SVA/case1.desc | 2 +- regression/verilog/SVA/cover1.desc | 4 ++-- regression/verilog/SVA/eventually2.desc | 2 +- regression/verilog/SVA/if1.desc | 4 ++-- regression/verilog/SVA/s_eventually3.desc | 2 +- .../verilog/SVA/system_verilog_assertion2.desc | 2 +- regression/verilog/SVA/unbounded1.desc | 2 +- regression/verilog/enums/enum1.desc | 2 +- regression/verilog/enums/enum4.desc | 2 +- regression/verilog/enums/enum_cast1.desc | 4 ++-- .../verilog/enums/enum_initializers1.desc | 4 ++-- .../verilog/expressions/static_cast1.desc | 2 +- .../verilog/modules/type_parameters1.desc | 4 ++-- regression/verilog/synthesis/always_ff1.desc | 2 +- ...s_assignment_to_variable_systemverilog.desc | 2 +- src/verilog/verilog_typecheck.cpp | 14 +++++++++++--- 60 files changed, 112 insertions(+), 104 deletions(-) diff --git a/regression/ebmc/BDD/BDD2.desc b/regression/ebmc/BDD/BDD2.desc index e9eea062f..85427a098 100644 --- a/regression/ebmc/BDD/BDD2.desc +++ b/regression/ebmc/BDD/BDD2.desc @@ -3,6 +3,6 @@ BDD2.sv --module main --bdd ^EXIT=10$ ^SIGNAL=0$ -^\[main.property.my_prop1\] always main.counter < 199: PROVED$ -^\[main.property.my_prop2\] always main.counter < 198: REFUTED$ +^\[main\.my_prop1\] always main.counter < 199: PROVED$ +^\[main\.my_prop2\] always main.counter < 198: REFUTED$ -- diff --git a/regression/ebmc/BDD/BDD3.desc b/regression/ebmc/BDD/BDD3.desc index 452545bf3..e92d3ff12 100644 --- a/regression/ebmc/BDD/BDD3.desc +++ b/regression/ebmc/BDD/BDD3.desc @@ -3,6 +3,6 @@ BDD3.sv --module main --bdd ^EXIT=10$ ^SIGNAL=0$ -^\[main.property.my_prop1\] always main.counter <= 10: PROVED$ -^\[main.property.my_prop2\] always main.counter < 10: REFUTED$ +^\[main\.my_prop1\] always main\.counter <= 10: PROVED$ +^\[main\.my_prop2\] always main\.counter < 10: REFUTED$ -- diff --git a/regression/ebmc/BDD/BDD_SVA1.desc b/regression/ebmc/BDD/BDD_SVA1.desc index 4acac1423..a2664728e 100644 --- a/regression/ebmc/BDD/BDD_SVA1.desc +++ b/regression/ebmc/BDD/BDD_SVA1.desc @@ -3,14 +3,14 @@ BDD_SVA1.sv --bdd ^EXIT=10$ ^SIGNAL=0$ -^\[top\.property\.p0\] always top\.my_bit: PROVED$ -^\[top\.property\.p1\] always top\.my_bit: PROVED$ -^\[top\.property\.p2\] always \(top\.counter == 3 \|-> \(nexttime top\.counter == 4\)\): FAILURE: property not supported by BDD engine$ -^\[top\.property\.p3\] always \(top\.counter == 3 \|=> top\.counter == 4\): FAILURE: property not supported by BDD engine$ -^\[top\.property\.p4\] always \(top\.counter == 3 \|=> \(nexttime top\.counter == 5\)\): FAILURE: property not supported by BDD engine$ -^\[top\.property\.p5\] always s_eventually top\.counter == 8: PROVED$ -^\[top\.property\.p6\] always \(top\.counter == 0 \|-> \(s_eventually top\.counter == 8\)\): FAILURE: property not supported by BDD engine$ -^\[top\.property\.p7\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until top\.counter == 6\)\): FAILURE: property not supported by BDD engine$ -^\[top\.property\.p8\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until_with top\.counter == 5\)\): FAILURE: property not supported by BDD engine$ +^\[top\.p0\] always top\.my_bit: PROVED$ +^\[top\.p1\] always top\.my_bit: PROVED$ +^\[top\.p2\] always \(top\.counter == 3 \|-> \(nexttime top\.counter == 4\)\): FAILURE: property not supported by BDD engine$ +^\[top\.p3\] always \(top\.counter == 3 \|=> top\.counter == 4\): FAILURE: property not supported by BDD engine$ +^\[top\.p4\] always \(top\.counter == 3 \|=> \(nexttime top\.counter == 5\)\): FAILURE: property not supported by BDD engine$ +^\[top\.p5\] always s_eventually top\.counter == 8: PROVED$ +^\[top\.p6\] always \(top\.counter == 0 \|-> \(s_eventually top\.counter == 8\)\): FAILURE: property not supported by BDD engine$ +^\[top\.p7\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until top\.counter == 6\)\): FAILURE: property not supported by BDD engine$ +^\[top\.p8\] always \(top\.counter == 0 \|-> \(top\.counter <= 5 until_with top\.counter == 5\)\): FAILURE: property not supported by BDD engine$ -- ^warning: ignoring diff --git a/regression/ebmc/Next-in-Property1/test.desc b/regression/ebmc/Next-in-Property1/test.desc index ccbd06de9..b0a1ff780 100644 --- a/regression/ebmc/Next-in-Property1/test.desc +++ b/regression/ebmc/Next-in-Property1/test.desc @@ -3,5 +3,5 @@ main.sv --module top --bound 10 ^EXIT=0$ ^SIGNAL=0$ -^\[top.property.p1\] always \(top.counter\[0\] |-> \(##1 top.counter <= 5\)\): SUCCESS$ +^\[top\.p1\] always \(top\.counter\[0\] |-> \(##1 top\.counter <= 5\)\): SUCCESS$ -- diff --git a/regression/ebmc/SVA-LTL/freeze.desc b/regression/ebmc/SVA-LTL/freeze.desc index f14bf322f..5492870a3 100644 --- a/regression/ebmc/SVA-LTL/freeze.desc +++ b/regression/ebmc/SVA-LTL/freeze.desc @@ -1,8 +1,8 @@ CORE freeze.sv --bound 1 -^\[main\.property\.p1\] always s_eventually main\.w: REFUTED$ -^\[main\.property\.p2\] always s_eventually !main\.w: REFUTED$ +^\[main\.p1\] always s_eventually main\.w: REFUTED$ +^\[main\.p2\] always s_eventually !main\.w: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/SVA-LTL/lasso1-counterexample.desc b/regression/ebmc/SVA-LTL/lasso1-counterexample.desc index 7476d478f..52c674d4d 100644 --- a/regression/ebmc/SVA-LTL/lasso1-counterexample.desc +++ b/regression/ebmc/SVA-LTL/lasso1-counterexample.desc @@ -3,7 +3,7 @@ lasso1.sv --bound 10 --waveform ^EXIT=10$ ^SIGNAL=0$ -^\[top\.property\.p0\] .* REFUTED$ +^\[top\.p0\] .* REFUTED$ ^ 0 1 2 3 4 5 6 7 8 9 10$ ^top\.counter 0 1 2 3 4 5 6 7 8 9 3$ -- diff --git a/regression/ebmc/SVA-LTL/lasso1-small-bound.desc b/regression/ebmc/SVA-LTL/lasso1-small-bound.desc index b501019cb..fef735300 100644 --- a/regression/ebmc/SVA-LTL/lasso1-small-bound.desc +++ b/regression/ebmc/SVA-LTL/lasso1-small-bound.desc @@ -3,6 +3,6 @@ lasso1.sv --bound 5 ^EXIT=0$ ^SIGNAL=0$ -^\[top\.property\.p0\] .* PROVED up to bound 5$ +^\[top\.p0\] .* PROVED up to bound 5$ -- -- diff --git a/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p0.desc b/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p0.desc index a0e8df414..9b570658b 100644 --- a/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p0.desc +++ b/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p0.desc @@ -1,8 +1,8 @@ CORE simple_counterexamples_to_Fp.sv ---bound 10 --property top.property.p0 +--bound 10 --property top.p0 ^Adding lasso constraints$ ^EXIT=10$ ^SIGNAL=0$ -^\[top\.property\.p0\] .* REFUTED$ +^\[top\.p0\] .* REFUTED$ -- diff --git a/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p1.desc b/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p1.desc index 7f000724a..c26ab4679 100644 --- a/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p1.desc +++ b/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p1.desc @@ -1,8 +1,8 @@ CORE simple_counterexamples_to_Fp.sv ---bound 10 --property top.property.p1 +--bound 10 --property top.p1 ^Adding lasso constraints$ ^EXIT=10$ ^SIGNAL=0$ -^\[top\.property\.p1\] .* REFUTED$ +^\[top\.p1\] .* REFUTED$ -- diff --git a/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p2.desc b/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p2.desc index 1eca882fb..bdfe3b928 100644 --- a/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p2.desc +++ b/regression/ebmc/SVA-LTL/simple_counterexamples_to_Fp.p2.desc @@ -1,8 +1,8 @@ CORE simple_counterexamples_to_Fp.sv ---bound 10 --property top.property.p2 +--bound 10 --property top.p2 ^Adding lasso constraints$ ^EXIT=10$ ^SIGNAL=0$ -^\[top\.property\.p2\] .* REFUTED$ +^\[top\.p2\] .* REFUTED$ -- diff --git a/regression/ebmc/SVA-LTL/simple_passing_LTL_properties.desc b/regression/ebmc/SVA-LTL/simple_passing_LTL_properties.desc index 338266616..38ed7523c 100644 --- a/regression/ebmc/SVA-LTL/simple_passing_LTL_properties.desc +++ b/regression/ebmc/SVA-LTL/simple_passing_LTL_properties.desc @@ -4,13 +4,13 @@ simple_passing_LTL_properties.sv ^Adding lasso constraints$ ^EXIT=0$ ^SIGNAL=0$ -^\[top.property.p0\] .* PROVED up to bound 10$ -^\[top.property.p1\] .* PROVED up to bound 10$ -^\[top.property.p2\] .* PROVED up to bound 10$ -^\[top.property.p3\] .* PROVED up to bound 10$ -^\[top.property.p4\] .* PROVED up to bound 10$ -^\[top.property.p5\] .* PROVED up to bound 10$ -^\[top.property.p6\] .* PROVED up to bound 10$ -^\[top.property.p7\] .* PROVED up to bound 10$ -^\[top.property.p8\] .* PROVED up to bound 10$ +^\[top\.p0\] .* PROVED up to bound 10$ +^\[top\.p1\] .* PROVED up to bound 10$ +^\[top\.p2\] .* PROVED up to bound 10$ +^\[top\.p3\] .* PROVED up to bound 10$ +^\[top\.p4\] .* PROVED up to bound 10$ +^\[top\.p5\] .* PROVED up to bound 10$ +^\[top\.p6\] .* PROVED up to bound 10$ +^\[top\.p7\] .* PROVED up to bound 10$ +^\[top\.p8\] .* PROVED up to bound 10$ -- diff --git a/regression/ebmc/example3/test.desc b/regression/ebmc/example3/test.desc index e055eac41..39dd59755 100644 --- a/regression/ebmc/example3/test.desc +++ b/regression/ebmc/example3/test.desc @@ -1,8 +1,8 @@ CORE example3.sv --bound 10 -^\[counter\.property\.1\] .* PROVED up to bound 10$ -^\[counter\.property\.2\] .* REFUTED$ +^\[counter\.assert\.1\] .* PROVED up to bound 10$ +^\[counter\.assert\.2\] .* REFUTED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/ebmc/example4_reset/test.desc b/regression/ebmc/example4_reset/test.desc index 1d3e5a34b..4f4bc99be 100644 --- a/regression/ebmc/example4_reset/test.desc +++ b/regression/ebmc/example4_reset/test.desc @@ -1,8 +1,8 @@ CORE example4.sv --bound 10 --reset "reset==1" -^\[counter\.property\.1\] .* PROVED up to bound 10$ -^\[counter\.property\.2\] .* PROVED up to bound 10$ +^\[counter\.assert\.1\] .* PROVED up to bound 10$ +^\[counter\.assert\.2\] .* PROVED up to bound 10$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/ebmc/example4_trace/test.desc b/regression/ebmc/example4_trace/test.desc index 1448a26aa..8714401a5 100644 --- a/regression/ebmc/example4_trace/test.desc +++ b/regression/ebmc/example4_trace/test.desc @@ -1,8 +1,8 @@ CORE broken-smt-backend example4.sv --bound 10 --trace -^\[counter\.property\.1\] .* PROVED up to bound 10$ -^\[counter\.property\.2\] .* REFUTED$ +^\[counter\.assert\.1\] .* PROVED up to bound 10$ +^\[counter\.assert\.2\] .* REFUTED$ ^ counter\.state = 254 \(11111110\)$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/ebmc/ic3/bobmiterbm1multi.1033.desc b/regression/ebmc/ic3/bobmiterbm1multi.1033.desc index 9acda0126..4a46e6e95 100644 --- a/regression/ebmc/ic3/bobmiterbm1multi.1033.desc +++ b/regression/ebmc/ic3/bobmiterbm1multi.1033.desc @@ -1,6 +1,6 @@ CORE bobmiterbm1multi.sv ---ic3 --property bobmiterbm1multi.property.1033 +--ic3 --property bobmiterbm1multi.assert.1033 ^EXIT=2$ ^SIGNAL=0$ ^property HOLDS diff --git a/regression/ebmc/ic3/bobmiterbm1multi.1080.desc b/regression/ebmc/ic3/bobmiterbm1multi.1080.desc index da6e4638e..d531e7011 100644 --- a/regression/ebmc/ic3/bobmiterbm1multi.1080.desc +++ b/regression/ebmc/ic3/bobmiterbm1multi.1080.desc @@ -1,6 +1,6 @@ CORE bobmiterbm1multi.sv ---ic3 --property bobmiterbm1multi.property.1080 +--ic3 --property bobmiterbm1multi.assert.1080 ^EXIT=1$ ^SIGNAL=0$ ^property FAILED diff --git a/regression/ebmc/ic3/non_inductive1.desc b/regression/ebmc/ic3/non_inductive1.desc index 76e1360cf..2c33d649d 100644 --- a/regression/ebmc/ic3/non_inductive1.desc +++ b/regression/ebmc/ic3/non_inductive1.desc @@ -1,6 +1,6 @@ CORE non_inductive1.sv ---ic3 --property main.property.p0 +--ic3 --property main.p0 ^EXIT=2$ ^SIGNAL=0$ ^property HOLDS$ diff --git a/regression/ebmc/ic3/not_supported1.desc b/regression/ebmc/ic3/not_supported1.desc index 10db048bc..0c8ee4ee4 100644 --- a/regression/ebmc/ic3/not_supported1.desc +++ b/regression/ebmc/ic3/not_supported1.desc @@ -1,7 +1,7 @@ CORE not_supported1.sv --ic3 -^\[main\.property\.p0\] always s_eventually main\.my_bit: FAILURE: property not supported by IC3 engine$ +^\[main\.p0\] always s_eventually main\.my_bit: FAILURE: property not supported by IC3 engine$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ic3/sm98a7multi.desc b/regression/ebmc/ic3/sm98a7multi.desc index 4a2c5ad14..3139728a8 100644 --- a/regression/ebmc/ic3/sm98a7multi.desc +++ b/regression/ebmc/ic3/sm98a7multi.desc @@ -1,6 +1,6 @@ CORE sm98a7multi.sv ---ic3 --property sm98a7multi.property.2 --constr +--ic3 --property sm98a7multi.assert.2 --constr ^EXIT=1$ ^SIGNAL=0$ ^property FAILED diff --git a/regression/ebmc/k-induction/k-induction-unsupported2.desc b/regression/ebmc/k-induction/k-induction-unsupported2.desc index c4c9da52d..6f0045012 100644 --- a/regression/ebmc/k-induction/k-induction-unsupported2.desc +++ b/regression/ebmc/k-induction/k-induction-unsupported2.desc @@ -3,7 +3,7 @@ k-induction-unsupported2.sv --module main --k-induction ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.x == 10: FAILURE: property unsupported by k-induction$ -^\[main\.property\.p1\] always main\.x <= 10: PROVED$ +^\[main\.p0\] always s_eventually main\.x == 10: FAILURE: property unsupported by k-induction$ +^\[main\.p1\] always main\.x <= 10: PROVED$ -- ^warning: ignoring diff --git a/regression/ebmc/k-induction/k-induction4.desc b/regression/ebmc/k-induction/k-induction4.desc index cb45d55bd..1f8760b59 100644 --- a/regression/ebmc/k-induction/k-induction4.desc +++ b/regression/ebmc/k-induction/k-induction4.desc @@ -3,6 +3,6 @@ k-induction4.sv --module main --bound 1 --k-induction ^EXIT=10$ ^SIGNAL=0$ -^\[main.property.p1] .* INCONCLUSIVE$ +^\[main\.p1] .* INCONCLUSIVE$ -- ^warning: ignoring diff --git a/regression/ebmc/liveness-to-safety/failing1.desc b/regression/ebmc/liveness-to-safety/failing1.desc index 758794bb7..85541780c 100644 --- a/regression/ebmc/liveness-to-safety/failing1.desc +++ b/regression/ebmc/liveness-to-safety/failing1.desc @@ -3,5 +3,5 @@ failing1.sv --bound 1 --liveness-to-safety ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.my_bit: REFUTED$ +^\[main\.p0\] always s_eventually main\.my_bit: REFUTED$ -- diff --git a/regression/ebmc/liveness-to-safety/failing1.k-1.desc b/regression/ebmc/liveness-to-safety/failing1.k-1.desc index 19a219ce7..98c1b849c 100644 --- a/regression/ebmc/liveness-to-safety/failing1.k-1.desc +++ b/regression/ebmc/liveness-to-safety/failing1.k-1.desc @@ -3,5 +3,5 @@ failing1.sv --k-induction --bound 1 --liveness-to-safety ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.my_bit: REFUTED$ +^\[main\.p0\] always s_eventually main\.my_bit: REFUTED$ -- diff --git a/regression/ebmc/liveness-to-safety/failing2.desc b/regression/ebmc/liveness-to-safety/failing2.desc index 7a6c16400..7890ce387 100644 --- a/regression/ebmc/liveness-to-safety/failing2.desc +++ b/regression/ebmc/liveness-to-safety/failing2.desc @@ -3,6 +3,6 @@ failing2.sv --bound 6 --liveness-to-safety ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.counter == 0: REFUTED$ -^\[main\.property\.p1\] always s_eventually main\.counter == 6: REFUTED$ +^\[main\.p0\] always s_eventually main\.counter == 0: REFUTED$ +^\[main\.p1\] always s_eventually main\.counter == 6: REFUTED$ -- diff --git a/regression/ebmc/liveness-to-safety/failing2.k-6.desc b/regression/ebmc/liveness-to-safety/failing2.k-6.desc index 736ad9fe7..cdc2d4911 100644 --- a/regression/ebmc/liveness-to-safety/failing2.k-6.desc +++ b/regression/ebmc/liveness-to-safety/failing2.k-6.desc @@ -3,6 +3,6 @@ failing2.sv --k-induction --bound 6 --liveness-to-safety ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.counter == 0: REFUTED$ -^\[main\.property\.p1\] always s_eventually main\.counter == 6: REFUTED$ +^\[main\.p0\] always s_eventually main\.counter == 0: REFUTED$ +^\[main\.p1\] always s_eventually main\.counter == 6: REFUTED$ -- diff --git a/regression/ebmc/liveness-to-safety/passing1.desc b/regression/ebmc/liveness-to-safety/passing1.desc index d980c7e16..0a765d3fb 100644 --- a/regression/ebmc/liveness-to-safety/passing1.desc +++ b/regression/ebmc/liveness-to-safety/passing1.desc @@ -3,5 +3,5 @@ passing1.sv --bound 10 --liveness-to-safety ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.my_bit: PROVED up to bound 10$ +^\[main\.p0\] always s_eventually main\.my_bit: PROVED up to bound 10$ -- diff --git a/regression/ebmc/liveness-to-safety/passing1.k-10.desc b/regression/ebmc/liveness-to-safety/passing1.k-10.desc index 82cd43dac..7f0ebc620 100644 --- a/regression/ebmc/liveness-to-safety/passing1.k-10.desc +++ b/regression/ebmc/liveness-to-safety/passing1.k-10.desc @@ -3,5 +3,5 @@ passing1.sv --k-induction --bound 10 --liveness-to-safety ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.my_bit: PROVED$ +^\[main\.p0\] always s_eventually main\.my_bit: PROVED$ -- diff --git a/regression/ebmc/liveness-to-safety/passing2.desc b/regression/ebmc/liveness-to-safety/passing2.desc index 0036c2ca0..044b35892 100644 --- a/regression/ebmc/liveness-to-safety/passing2.desc +++ b/regression/ebmc/liveness-to-safety/passing2.desc @@ -3,6 +3,6 @@ passing2.sv --bound 10 --liveness-to-safety ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.counter == 0: PROVED up to bound 10$ -^\[main\.property\.p1\] always s_eventually main\.counter == 8: PROVED up to bound 10$ +^\[main\.p0\] always s_eventually main\.counter == 0: PROVED up to bound 10$ +^\[main\.p1\] always s_eventually main\.counter == 8: PROVED up to bound 10$ -- diff --git a/regression/ebmc/liveness-to-safety/passing2.k-10.desc b/regression/ebmc/liveness-to-safety/passing2.k-10.desc index fe9192357..75cabbf86 100644 --- a/regression/ebmc/liveness-to-safety/passing2.k-10.desc +++ b/regression/ebmc/liveness-to-safety/passing2.k-10.desc @@ -3,6 +3,6 @@ passing2.sv --k-induction --bound 10 --liveness-to-safety ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.counter == 0: INCONCLUSIVE$ -^\[main\.property\.p1\] always s_eventually main\.counter == 8: INCONCLUSIVE$ +^\[main\.p0\] always s_eventually main\.counter == 0: INCONCLUSIVE$ +^\[main\.p1\] always s_eventually main\.counter == 8: INCONCLUSIVE$ -- diff --git a/regression/ebmc/netlist/netlist-trace1.desc b/regression/ebmc/netlist/netlist-trace1.desc index 270cdc9c5..608e5663a 100644 --- a/regression/ebmc/netlist/netlist-trace1.desc +++ b/regression/ebmc/netlist/netlist-trace1.desc @@ -1,7 +1,7 @@ CORE netlist-trace1.sv --bound 10 --trace --aig -^\[counter\.property\.1\] always counter\.state != 3: REFUTED$ +^\[counter\.assert\.1\] always counter\.state != 3: REFUTED$ ^ counter\.state = 3 \(00000011\)$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/ebmc/neural-liveness/counter1.desc b/regression/ebmc/neural-liveness/counter1.desc index da00acbd7..d5f1585a0 100644 --- a/regression/ebmc/neural-liveness/counter1.desc +++ b/regression/ebmc/neural-liveness/counter1.desc @@ -1,7 +1,7 @@ CORE counter1.sv --traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n" -^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$ +^\[main\.p0\] always s_eventually main.counter == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/clock24h.day.desc b/regression/ebmc/ranking-function/clock24h.day.desc index 75c088ebd..58865dac3 100644 --- a/regression/ebmc/ranking-function/clock24h.day.desc +++ b/regression/ebmc/ranking-function/clock24h.day.desc @@ -1,7 +1,7 @@ CORE clock24h.sv ---property main.property.p_day --ranking-function "{23-hours,59-minutes,59-seconds}" -^\[main\.property\.p_day\] .*: PROVED$ +--property main.p_day --ranking-function "{23-hours,59-minutes,59-seconds}" +^\[main\.p_day\] .*: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/clock24h.hour.desc b/regression/ebmc/ranking-function/clock24h.hour.desc index e0144bce3..dd10eaa7b 100644 --- a/regression/ebmc/ranking-function/clock24h.hour.desc +++ b/regression/ebmc/ranking-function/clock24h.hour.desc @@ -1,7 +1,7 @@ CORE clock24h.sv ---property main.property.p_hour --ranking-function "{59-minutes,59-seconds}" -^\[main\.property\.p_hour\] .*: PROVED$ +--property main.p_hour --ranking-function "{59-minutes,59-seconds}" +^\[main\.p_hour\] .*: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/clock24h.minute.desc b/regression/ebmc/ranking-function/clock24h.minute.desc index 0c2f09f6d..42f874287 100644 --- a/regression/ebmc/ranking-function/clock24h.minute.desc +++ b/regression/ebmc/ranking-function/clock24h.minute.desc @@ -1,7 +1,7 @@ CORE clock24h.sv ---property main.property.p_minute --ranking-function "59-seconds" -^\[main\.property\.p_minute\] .*: PROVED$ +--property main.p_minute --ranking-function "59-seconds" +^\[main\.p_minute\] .*: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/counter1.fail.desc b/regression/ebmc/ranking-function/counter1.fail.desc index 4cc91cf35..1721a065f 100644 --- a/regression/ebmc/ranking-function/counter1.fail.desc +++ b/regression/ebmc/ranking-function/counter1.fail.desc @@ -1,7 +1,7 @@ CORE counter1.sv --ranking-function "(-counter)" -^\[main\.property\.p0\] always s_eventually main.counter == 0: INCONCLUSIVE$ +^\[main\.p0\] always s_eventually main.counter == 0: INCONCLUSIVE$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/counter1.pass.desc b/regression/ebmc/ranking-function/counter1.pass.desc index ff9e340a9..98d94860a 100644 --- a/regression/ebmc/ranking-function/counter1.pass.desc +++ b/regression/ebmc/ranking-function/counter1.pass.desc @@ -1,7 +1,7 @@ CORE counter1.sv --ranking-function counter -^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$ +^\[main\.p0\] always s_eventually main.counter == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/counter2.fail.desc b/regression/ebmc/ranking-function/counter2.fail.desc index 51ace528e..35ee4b2af 100644 --- a/regression/ebmc/ranking-function/counter2.fail.desc +++ b/regression/ebmc/ranking-function/counter2.fail.desc @@ -1,7 +1,7 @@ CORE counter2.sv --ranking-function counter --numbered-trace -^\[main\.property\.p0\] always s_eventually main.counter == 10: INCONCLUSIVE$ +^\[main\.p0\] always s_eventually main.counter == 10: INCONCLUSIVE$ ^main\.counter@0 = .*$ ^main\.counter@1 = .*$ ^EXIT=10$ diff --git a/regression/ebmc/ranking-function/counter2.pass.desc b/regression/ebmc/ranking-function/counter2.pass.desc index e7f0c9544..754ab4570 100644 --- a/regression/ebmc/ranking-function/counter2.pass.desc +++ b/regression/ebmc/ranking-function/counter2.pass.desc @@ -1,7 +1,7 @@ CORE counter2.sv --ranking-function 10-counter -^\[main\.property\.p0\] always s_eventually main.counter == 10: PROVED$ +^\[main\.p0\] always s_eventually main.counter == 10: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/counter_in_module1.desc b/regression/ebmc/ranking-function/counter_in_module1.desc index a06dd16d4..14478d3b1 100644 --- a/regression/ebmc/ranking-function/counter_in_module1.desc +++ b/regression/ebmc/ranking-function/counter_in_module1.desc @@ -1,7 +1,7 @@ CORE counter_in_module1.sv --ranking-function my_instance.counter -^\[main\.property\.p0\] always s_eventually main\.my_instance\.counter == 0: PROVED$ +^\[main\.p0\] always s_eventually main\.my_instance\.counter == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/counter_with_reset1.fail.desc b/regression/ebmc/ranking-function/counter_with_reset1.fail.desc index b9ec64d23..eb3ddc837 100644 --- a/regression/ebmc/ranking-function/counter_with_reset1.fail.desc +++ b/regression/ebmc/ranking-function/counter_with_reset1.fail.desc @@ -1,7 +1,7 @@ CORE counter_with_reset1.sv ---property main.property.p0 --ranking-function 10-counter -^\[main\.property\.p0\] always s_eventually main.counter == 10: INCONCLUSIVE$ +--property main.p0 --ranking-function 10-counter +^\[main\.p0\] always s_eventually main.counter == 10: INCONCLUSIVE$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/counter_with_reset1.pass.desc b/regression/ebmc/ranking-function/counter_with_reset1.pass.desc index b79ed3a37..1d5735d53 100644 --- a/regression/ebmc/ranking-function/counter_with_reset1.pass.desc +++ b/regression/ebmc/ranking-function/counter_with_reset1.pass.desc @@ -1,7 +1,7 @@ CORE counter_with_reset1.sv ---property main.property.p1 --ranking-function 10-counter -^\[main\.property\.p1\] always s_eventually main.reset \|\| main.counter == 10: PROVED$ +--property main.p1 --ranking-function 10-counter +^\[main\.p1\] always s_eventually main.reset \|\| main.counter == 10: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc b/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc index db8806132..210fb890b 100644 --- a/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc +++ b/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc @@ -1,7 +1,7 @@ CORE lexicographic_ranking_function1.sv --ranking-function "{digit1, digit2}" -^\[main\.property\.p0\] always s_eventually main\.digit1 == 0: PROVED$ +^\[main\.p0\] always s_eventually main\.digit1 == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ranking-function/signed1.desc b/regression/ebmc/ranking-function/signed1.desc index 20e0ae91d..d0a42d173 100644 --- a/regression/ebmc/ranking-function/signed1.desc +++ b/regression/ebmc/ranking-function/signed1.desc @@ -1,7 +1,7 @@ CORE signed1.sv --ranking-function "(-$signed({1'b0,counter}))" -^\[main\.property\.p0\] always s_eventually main.counter == 0: PROVED$ +^\[main\.p0\] always s_eventually main.counter == 0: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc/ring_buffer_induction/test.desc b/regression/ebmc/ring_buffer_induction/test.desc index b5856fe8e..9c422de4a 100644 --- a/regression/ebmc/ring_buffer_induction/test.desc +++ b/regression/ebmc/ring_buffer_induction/test.desc @@ -1,9 +1,9 @@ CORE ring_buffer.sv --k-induction -^\[ring_buffer\.property\.1\] assume always \(ring_buffer\.empty |-> !ring_buffer\.read\): ASSUMED$ -^\[ring_buffer\.property\.2\] assume always \(ring_buffer\.full |-> !ring_buffer\.write\): ASSUMED$ -^\[ring_buffer\.property\.3\] always \(ring_buffer\.writeptr - ring_buffer\.readptr & 15\) == ring_buffer\.count: PROVED$ +^\[ring_buffer\.assert\.1\] assume always \(ring_buffer\.empty |-> !ring_buffer\.read\): ASSUMED$ +^\[ring_buffer\.assert\.2\] assume always \(ring_buffer\.full |-> !ring_buffer\.write\): ASSUMED$ +^\[ring_buffer\.assert\.3\] always \(ring_buffer\.writeptr - ring_buffer\.readptr & 15\) == ring_buffer\.count: PROVED$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/verilog/SVA/case1.desc b/regression/verilog/SVA/case1.desc index aaea35756..5e52fd0c6 100644 --- a/regression/verilog/SVA/case1.desc +++ b/regression/verilog/SVA/case1.desc @@ -1,7 +1,7 @@ CORE case1.sv --bound 20 --numbered-trace -^\[main\.property\.p0\] always \(case\(main\.x\) 10: 0; endcase\): REFUTED$ +^\[main\.p0\] always \(case\(main\.x\) 10: 0; endcase\): REFUTED$ ^Counterexample with 11 states:$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/verilog/SVA/cover1.desc b/regression/verilog/SVA/cover1.desc index f980b8f87..88ce2095a 100644 --- a/regression/verilog/SVA/cover1.desc +++ b/regression/verilog/SVA/cover1.desc @@ -1,11 +1,11 @@ CORE cover1.sv --bound 10 --numbered-trace -^\[main\.property\.p0\] cover main\.counter == 1: PROVED$ +^\[main\.p0\] cover main\.counter == 1: PROVED$ ^Trace with 2 states:$ ^main\.counter@0 = 0$ ^main\.counter@1 = 1$ -^\[main\.property\.p1\] cover main\.counter == 100: REFUTED up to bound 10$ +^\[main\.p1\] cover main\.counter == 100: REFUTED up to bound 10$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/eventually2.desc b/regression/verilog/SVA/eventually2.desc index 9b6ac059b..49ad04bcb 100644 --- a/regression/verilog/SVA/eventually2.desc +++ b/regression/verilog/SVA/eventually2.desc @@ -1,7 +1,7 @@ CORE eventually2.sv --bound 20 -^\[main\.property\.p0\] always \(eventually \[0:2\] main\.counter == 3\): REFUTED$ +^\[main\.p0\] always \(eventually \[0:2\] main\.counter == 3\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/if1.desc b/regression/verilog/SVA/if1.desc index ede656c1a..6857b32f1 100644 --- a/regression/verilog/SVA/if1.desc +++ b/regression/verilog/SVA/if1.desc @@ -1,8 +1,8 @@ CORE broken-smt-backend if1.sv --bound 2 -^\[main\.property\.p0\] always if\(main\.counter == 0\) nexttime main\.counter == 1: PROVED up to bound 2$ -^\[main\.property\.p1\] always if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3: REFUTED$ +^\[main\.p0\] always if\(main\.counter == 0\) nexttime main\.counter == 1: PROVED up to bound 2$ +^\[main\.p1\] always if\(main\.counter == 0\) nexttime main\.counter == 1 else nexttime main\.counter == 3: REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/s_eventually3.desc b/regression/verilog/SVA/s_eventually3.desc index bc13adab8..26547670e 100644 --- a/regression/verilog/SVA/s_eventually3.desc +++ b/regression/verilog/SVA/s_eventually3.desc @@ -3,6 +3,6 @@ s_eventually3.sv --module main --bound 11 ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p0\] always s_eventually main\.counter <= 5: REFUTED$ +^\[main\.p0\] always s_eventually main\.counter <= 5: REFUTED$ -- ^warning: ignoring diff --git a/regression/verilog/SVA/system_verilog_assertion2.desc b/regression/verilog/SVA/system_verilog_assertion2.desc index e78fda5c7..1a3d67b8f 100644 --- a/regression/verilog/SVA/system_verilog_assertion2.desc +++ b/regression/verilog/SVA/system_verilog_assertion2.desc @@ -4,6 +4,6 @@ system_verilog_assertion2.sv ^EXIT=10$ ^SIGNAL=0$ ^Counterexample:$ -^\[main.property.my_label\] .* REFUTED$ +^\[main\.my_label\] .* REFUTED$ -- ^warning: ignoring diff --git a/regression/verilog/SVA/unbounded1.desc b/regression/verilog/SVA/unbounded1.desc index 7e55e0bd6..879f96491 100644 --- a/regression/verilog/SVA/unbounded1.desc +++ b/regression/verilog/SVA/unbounded1.desc @@ -1,7 +1,7 @@ CORE unbounded1.sv --module main --bound 1 -^\[main\.property\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$ +^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$ ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/verilog/enums/enum1.desc b/regression/verilog/enums/enum1.desc index df52901e5..5ab23a212 100644 --- a/regression/verilog/enums/enum1.desc +++ b/regression/verilog/enums/enum1.desc @@ -3,7 +3,7 @@ enum1.sv --bound 3 --numbered-trace ^EXIT=10$ ^SIGNAL=0$ -^\[main\.property\.p1\] always main\.my_light != main.YELLOW2: REFUTED$ +^\[main\.p1\] always main\.my_light != main.YELLOW2: REFUTED$ ^main\.my_light@0 = main\.RED$ ^main\.my_light@1 = main\.YELLOW1$ ^main\.my_light@2 = main\.GREEN$ diff --git a/regression/verilog/enums/enum4.desc b/regression/verilog/enums/enum4.desc index aae52effe..e8960a8bf 100644 --- a/regression/verilog/enums/enum4.desc +++ b/regression/verilog/enums/enum4.desc @@ -3,5 +3,5 @@ enum4.sv --bound 0 ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p1\] always main.A == main.A: PROVED up to bound 0$ +^\[main\.p1\] always main.A == main.A: PROVED up to bound 0$ -- diff --git a/regression/verilog/enums/enum_cast1.desc b/regression/verilog/enums/enum_cast1.desc index 4493d9b09..d7ee9ba60 100644 --- a/regression/verilog/enums/enum_cast1.desc +++ b/regression/verilog/enums/enum_cast1.desc @@ -3,6 +3,6 @@ enum_cast1.sv --bound 0 ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p1\] always main.A == 1: PROVED up to bound 0$ -^\[main\.property\.p2\] always main.B == 2: PROVED up to bound 0$ +^\[main\.p1\] always main.A == 1: PROVED up to bound 0$ +^\[main\.p2\] always main.B == 2: PROVED up to bound 0$ -- diff --git a/regression/verilog/enums/enum_initializers1.desc b/regression/verilog/enums/enum_initializers1.desc index d8940f27b..77900bc5c 100644 --- a/regression/verilog/enums/enum_initializers1.desc +++ b/regression/verilog/enums/enum_initializers1.desc @@ -1,8 +1,8 @@ CORE enum_initializers1.sv --bound 0 -^\[main\.property\.pA\] always main.A == 1: PROVED up to bound 0$ -^\[main\.property\.pB\] always main.B == 11: PROVED up to bound 0$ +^\[main\.pA\] always main.A == 1: PROVED up to bound 0$ +^\[main\.pB\] always main.B == 11: PROVED up to bound 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/expressions/static_cast1.desc b/regression/verilog/expressions/static_cast1.desc index 56b3ee2f5..3400a5beb 100644 --- a/regression/verilog/expressions/static_cast1.desc +++ b/regression/verilog/expressions/static_cast1.desc @@ -3,6 +3,6 @@ static_cast1.sv --module main --bound 0 ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p0\] always 255 == 255: PROVED up to bound 0$ +^\[main\.p0\] always 255 == 255: PROVED up to bound 0$ -- ^warning: ignoring diff --git a/regression/verilog/modules/type_parameters1.desc b/regression/verilog/modules/type_parameters1.desc index 2fd0d7490..f2641706d 100644 --- a/regression/verilog/modules/type_parameters1.desc +++ b/regression/verilog/modules/type_parameters1.desc @@ -1,8 +1,8 @@ CORE type_parameters1.sv --bound 0 -^\[main\.property\.p1\] always 1 == 1: PROVED up to bound 0$ -^\[main\.property\.p2\] always 32 == 32: PROVED up to bound 0$ +^\[main\.p1\] always 1 == 1: PROVED up to bound 0$ +^\[main\.p2\] always 32 == 32: PROVED up to bound 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/always_ff1.desc b/regression/verilog/synthesis/always_ff1.desc index c1a5ce533..dd5dd5cf6 100644 --- a/regression/verilog/synthesis/always_ff1.desc +++ b/regression/verilog/synthesis/always_ff1.desc @@ -3,6 +3,6 @@ always_ff1.sv --module main --k-induction ^EXIT=0$ ^SIGNAL=0$ -^\[main\.property\.p0\] always main\.x >= 1 && main\.x <= 10: PROVED$ +^\[main\.p0\] always main\.x >= 1 && main\.x <= 10: PROVED$ -- ^warning: ignoring diff --git a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc index 9c5e915a2..a4b74babe 100644 --- a/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc +++ b/regression/verilog/synthesis/continuous_assignment_to_variable_systemverilog.desc @@ -1,7 +1,7 @@ CORE continuous_assignment_to_variable_systemverilog.sv --bound 0 -^\[main\.property\.p1\] always main\.some_reg == main\.i: PROVED up to bound 0$ +^\[main\.p1\] always main\.some_reg == main\.i: PROVED up to bound 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/verilog/verilog_typecheck.cpp b/src/verilog/verilog_typecheck.cpp index 563f7a274..59f3391df 100644 --- a/src/verilog/verilog_typecheck.cpp +++ b/src/verilog/verilog_typecheck.cpp @@ -1023,21 +1023,29 @@ void verilog_typecheckt::convert_assert_assume_cover( irep_idt base_name; + // The label is optional. if(identifier == irep_idt()) { + std::string kind = module_item.id() == ID_verilog_assert_property ? "assert" + : module_item.id() == ID_verilog_assume_property + ? "assume" + : module_item.id() == ID_verilog_cover_property ? "cover" + : ""; + assertion_counter++; - base_name = std::to_string(assertion_counter); + base_name = kind + "." + std::to_string(assertion_counter); } else base_name = identifier; + // The assert/assume/cover module items use the module name space std::string full_identifier = - id2string(module_identifier) + ".property." + id2string(base_name); + id2string(module_identifier) + '.' + id2string(base_name); if(symbol_table.symbols.find(full_identifier) != symbol_table.symbols.end()) { throw errort().with_location(module_item.source_location()) - << "property identifier `" << base_name << "' already used"; + << "identifier `" << base_name << "' already used"; } module_item.identifier(full_identifier);