add tests

This commit is contained in:
N. Engelhardt 2020-09-28 18:12:40 +02:00
parent 8f1d53e66f
commit dc4a617694
2 changed files with 49 additions and 0 deletions

View File

@ -0,0 +1,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

25
tests/verilog/const_sr.ys Normal file
View File

@ -0,0 +1,25 @@
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