mirror of
https://github.com/YosysHQ/yosys
synced 2025-07-30 16:03:17 +00:00
Merge branch 'eddie/fix_sat_init' into eddie/fix1427
This commit is contained in:
commit
c6a55d948a
2 changed files with 24 additions and 1 deletions
|
@ -2,3 +2,23 @@ read_verilog -sv initval.v
|
|||
proc;;
|
||||
|
||||
sat -seq 10 -prove-asserts
|
||||
|
||||
read_verilog <<EOT
|
||||
module gold(input clk, input i, output reg [1:0] o);
|
||||
initial o = 2'b10;
|
||||
always @(posedge clk)
|
||||
o[0] <= {i,i};
|
||||
endmodule
|
||||
|
||||
module gate(input clk, input i, output reg [1:0] o);
|
||||
initial o = 2'b10;
|
||||
always @(posedge clk)
|
||||
o[0] <= i;
|
||||
always @*
|
||||
o[1] <= o[0];
|
||||
endmodule
|
||||
EOT
|
||||
|
||||
proc
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 1 -falsify -prove-asserts -show-ports miter
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue