1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
read_verilog <<EOT
module test (
input clk, d,
output reg q
);
wire nop = 1'h0;
always @(posedge clk, posedge nop) begin
if (nop) q <= 1'b0;
else q <= d;
end
endmodule
EOT
prep -top test
write_verilog const_arst.v
design -stash gold
read_verilog const_arst.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
|
