mirror of
https://github.com/YosysHQ/yosys
synced 2025-07-24 13:18:56 +00:00
now ignore init attributes on non-register wires in sat command
This commit is contained in:
parent
ee8ad72fd9
commit
3b52121d32
3 changed files with 43 additions and 4 deletions
15
tests/sat/initval.v
Normal file
15
tests/sat/initval.v
Normal file
|
@ -0,0 +1,15 @@
|
|||
module test(input clk, input [3:0] bar, output [3:0] foo);
|
||||
reg [3:0] foo = 0;
|
||||
reg [3:0] last_bar = 0;
|
||||
|
||||
always @*
|
||||
foo[1:0] <= bar[1:0];
|
||||
|
||||
always @(posedge clk)
|
||||
foo[3:2] <= bar[3:2];
|
||||
|
||||
always @(posedge clk)
|
||||
last_bar <= bar;
|
||||
|
||||
assert property (foo == {last_bar[3:2], bar[1:0]});
|
||||
endmodule
|
4
tests/sat/initval.ys
Normal file
4
tests/sat/initval.ys
Normal file
|
@ -0,0 +1,4 @@
|
|||
read_verilog -sv initval.v
|
||||
proc;;
|
||||
|
||||
sat -seq 10 -prove-asserts
|
Loading…
Add table
Add a link
Reference in a new issue