mirror of https://github.com/YosysHQ/yosys.git
Add test that is expecting to fail
This commit is contained in:
parent
6028f5df1a
commit
c28d4b8047
|
@ -2,3 +2,23 @@ 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 New Issue