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