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

@@ -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$
 --

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$
 --

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

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$
 --

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$
 --

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$
 --

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$
 --
 --

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$
 --

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$
 --

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$
 --

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$
 --

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$
 

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$
 

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$

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

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

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$

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$
 --

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

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

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

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$
 --

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$
 --

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$
 --

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$
 --

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$
 --

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$
 --

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$
 --

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$
 --

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$

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$
 --

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$
 --

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$
 --

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$
 --

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$
 --

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$
 --

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$

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$
 --

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$
 --

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$
 --