mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-20 14:20:32 +00:00
25 lines
546 B
Text
25 lines
546 B
Text
read_verilog <<EOT
|
|
module test (
|
|
input clk, rst, d,
|
|
output reg q
|
|
);
|
|
wire nop = 1'h0;
|
|
always @(posedge clk, posedge nop, posedge rst) begin
|
|
if (rst) q <= 1'b0;
|
|
else if (nop) q <= 1'b1;
|
|
else q <= d;
|
|
end
|
|
endmodule
|
|
EOT
|
|
prep -top test
|
|
write_verilog const_sr.v
|
|
design -stash gold
|
|
read_verilog const_sr.v
|
|
prep -top test
|
|
design -stash gate
|
|
design -copy-from gold -as gold A:top
|
|
design -copy-from gate -as gate A:top
|
|
miter -equiv -flatten -make_assert gold gate miter
|
|
prep -top miter
|
|
clk2fflogic
|
|
sat -set-init-zero -tempinduct -prove-asserts -verify
|