mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-28 18:29:25 +00:00
34 lines
687 B
Text
34 lines
687 B
Text
read_verilog <<EOT
|
|
module top (y, clk, w);
|
|
output reg y = 1'b0;
|
|
input clk, w;
|
|
reg [1:0] i = 2'b00;
|
|
always @(posedge clk)
|
|
// If the constant below is set to 2'b00, the correct output is generated.
|
|
// vvvv
|
|
for (i = 1'b0; i < 2'b01; i = i + 2'b01)
|
|
y <= w || i[1:1];
|
|
endmodule
|
|
EOT
|
|
|
|
synth
|
|
design -stash gate
|
|
|
|
read_verilog <<EOT
|
|
module gold (y, clk, w);
|
|
input clk;
|
|
wire [1:0] i;
|
|
input w;
|
|
output y;
|
|
reg y = 1'h0;
|
|
always @(posedge clk)
|
|
y <= w;
|
|
assign i = 2'h0;
|
|
endmodule
|
|
EOT
|
|
proc gold
|
|
|
|
design -import gate -as gate
|
|
|
|
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
|
sat -seq 10 -verify -prove-asserts -show-ports miter
|