mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-13 04:28:18 +00:00
Revert "Add test that is expecting to fail"
This reverts commit c28d4b8047
.
This commit is contained in:
parent
ea54b5ea61
commit
3fb604c75d
|
@ -2,23 +2,3 @@ read_verilog -sv initval.v
|
||||||
proc;;
|
proc;;
|
||||||
|
|
||||||
sat -seq 10 -prove-asserts
|
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…
Reference in a new issue