Skip to content

Commit

Permalink
KNOWNBUG test for continuous assignment to variable
Browse files Browse the repository at this point in the history
SystemVerilog allows continous assignments to variables.

This test exposes that inconsistent constraints get generated for this case.

This replicates issue #635.
  • Loading branch information
kroening committed Aug 27, 2024
1 parent 0fc2ab6 commit e548bdf
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 0 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
KNOWNBUG
continuous_assignment_to_variable_systemverilog2.sv
--bound 1
^\[main\.cover1\] cover 1: PROVED$
^EXIT=0$
^SIGNAL=0$
--
--
This creates inconsistent constraints, which yields UNSAT.
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
module main(input clk);

bit state = 0;

always_ff @(posedge clk)
state = 1;

logic data;

// continuous assignment to variable
assign data = state;

cover1: cover property (@(posedge clk) (1));

endmodule

0 comments on commit e548bdf

Please sign in to comment.