mirror of https://github.com/YosysHQ/yosys.git
25 lines
478 B
Plaintext
25 lines
478 B
Plaintext
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
|