From 19700132f1d8e5f58f357b9011ee5256b4711b05 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 6 Jul 2025 07:26:42 -0400 Subject: [PATCH] SVA: not/implies/iff operators yield a property The SVA not/implies/iff operators yield a property, even when applied to a sequence, and hence, use as a sequence should be errored. --- regression/verilog/SVA/sequence_not1.desc | 6 +++--- regression/verilog/SVA/sequence_not1.sv | 7 ++----- src/verilog/verilog_typecheck_sva.cpp | 4 +++- 3 files changed, 8 insertions(+), 9 deletions(-) diff --git a/regression/verilog/SVA/sequence_not1.desc b/regression/verilog/SVA/sequence_not1.desc index d54da4be8..164163141 100644 --- a/regression/verilog/SVA/sequence_not1.desc +++ b/regression/verilog/SVA/sequence_not1.desc @@ -1,9 +1,9 @@ -KNOWNBUG +CORE sequence_not1.sv -^EXIT=0$ +^file .* line 9: sequence required, but got property$ +^EXIT=2$ ^SIGNAL=0$ -- ^warning: ignoring -- -The grammar for 'SVA sequence not' is missing. diff --git a/regression/verilog/SVA/sequence_not1.sv b/regression/verilog/SVA/sequence_not1.sv index b235aed0c..f4e580fac 100644 --- a/regression/verilog/SVA/sequence_not1.sv +++ b/regression/verilog/SVA/sequence_not1.sv @@ -5,10 +5,7 @@ module main(input clk); always @(posedge clk) x<=x+1; - // should pass - initial p0: assert property (not x == 1); - - // Given a sequence, 'not' yields a sequence, not a property - initial p1: assert property ((not x == 1)[*1]); + // Given a sequence, 'not' yields a property, not a sequence + assert property ((not x == 1)[*1]); endmodule diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp index 744242b5e..29e21bde9 100644 --- a/src/verilog/verilog_typecheck_sva.cpp +++ b/src/verilog/verilog_typecheck_sva.cpp @@ -28,7 +28,9 @@ void verilog_typecheck_exprt::require_sva_sequence(exprt &expr) type.id() == ID_signedbv || type.id() == ID_verilog_unsignedbv || type.id() == ID_verilog_signedbv) { - if(has_temporal_operator(expr)) + if( + has_temporal_operator(expr) || expr.id() == ID_sva_not || + expr.id() == ID_sva_implies || expr.id() == ID_sva_iff) { throw errort().with_location(expr.source_location()) << "sequence required, but got property";