From a8c9854f497ed882e067cc78d141435a0610ded2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 22 Oct 2025 10:24:23 -0700 Subject: [PATCH] SystemVerilog: labeled immediate assert/assume/cover statements The label in front of an immediate assert/assume/cover statement is now used to form the identifier of the item. --- CHANGELOG | 1 + regression/ebmc-spot/sva-buechi/initial2.bmc.desc | 4 ++-- regression/ebmc-spot/sva-buechi/initial2.k.desc | 4 ++-- regression/verilog/SVA/initial2.desc | 4 ++-- regression/verilog/SVA/initial2.sv | 4 ++-- src/verilog/parser.y | 13 ++++++++++++- 6 files changed, 21 insertions(+), 9 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index 608287b9c..659ff0bea 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,7 @@ * Verilog: semantic fix for output register ports * SystemVerilog: cover sequence +* SystemVerilog: labeled immediate assert/assume/cover statements * SystemVerilog: semantics fix for explicit casts # EBMC 5.7 diff --git a/regression/ebmc-spot/sva-buechi/initial2.bmc.desc b/regression/ebmc-spot/sva-buechi/initial2.bmc.desc index d7a98733e..dc5b85d87 100644 --- a/regression/ebmc-spot/sva-buechi/initial2.bmc.desc +++ b/regression/ebmc-spot/sva-buechi/initial2.bmc.desc @@ -1,8 +1,8 @@ CORE ../../verilog/SVA/initial2.sv --buechi --module main -^\[main\.assert\.1\] main\.counter == 1: PROVED \(1-induction\)$ -^\[main\.assert\.2\] main\.counter == 2: PROVED \(1-induction\)$ +^\[main\.p0\] main\.counter == 1: PROVED \(1-induction\)$ +^\[main\.p1\] main\.counter == 2: PROVED \(1-induction\)$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/ebmc-spot/sva-buechi/initial2.k.desc b/regression/ebmc-spot/sva-buechi/initial2.k.desc index fa0aeab7a..e975119ef 100644 --- a/regression/ebmc-spot/sva-buechi/initial2.k.desc +++ b/regression/ebmc-spot/sva-buechi/initial2.k.desc @@ -1,8 +1,8 @@ CORE ../../verilog/SVA/initial2.sv --buechi --k-induction --bound 1 --module main -^\[main\.assert\.1\] main\.counter == 1: PROVED$ -^\[main\.assert\.2\] main\.counter == 2: PROVED$ +^\[main\.p0\] main\.counter == 1: PROVED$ +^\[main\.p1\] main\.counter == 2: PROVED$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/initial2.desc b/regression/verilog/SVA/initial2.desc index 22b6a1662..cd4547272 100644 --- a/regression/verilog/SVA/initial2.desc +++ b/regression/verilog/SVA/initial2.desc @@ -1,8 +1,8 @@ CORE initial2.sv --module main -^\[main\.assert\.1\] main\.counter == 1: PROVED .*$ -^\[main\.assert\.2\] main\.counter == 2: PROVED .*$ +^\[main\.p0\] main\.counter == 1: PROVED .*$ +^\[main\.p1\] main\.counter == 2: PROVED .*$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/SVA/initial2.sv b/regression/verilog/SVA/initial2.sv index c47d12884..cf254b372 100644 --- a/regression/verilog/SVA/initial2.sv +++ b/regression/verilog/SVA/initial2.sv @@ -6,12 +6,12 @@ module main(input clk); initial begin counter = 1; // expected to pass - assert(counter == 1); + p0: assert(counter == 1); counter = 2; end // expected to pass - initial assert property (counter == 2); + initial p1: assert property (counter == 2); always_ff @(posedge clk) counter = counter + 1; diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 61e5b98d9..6e550094c 100644 --- a/src/verilog/parser.y +++ b/src/verilog/parser.y @@ -3661,7 +3661,18 @@ statement: attribute_instance_brace block_identifier TOK_COLON attribute_instance_brace statement_item { init($$, ID_verilog_label_statement); stack_expr($$).set(ID_base_name, stack_expr($2).id()); - mto($$, $5); } + + // We'll stick the label onto any assertion + auto statement = stack_expr($5).id(); + if(statement == ID_verilog_immediate_assert || + statement == ID_verilog_immediate_assume || + statement == ID_verilog_immediate_cover) + { + stack_expr($5).set(ID_identifier, stack_expr($2).id()); + } + + mto($$, $5); + } | attribute_instance_brace statement_item { $$=$2; } ;