add tests

diff --git a/tests/verilog/const_arst.ys b/tests/verilog/const_arst.ys
new file mode 100644 (file)
index 0000000..df72057
--- /dev/null
+++ b/tests/verilog/const_arst.ys
@@ -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

diff --git a/tests/verilog/const_sr.ys b/tests/verilog/const_sr.ys
new file mode 100644 (file)
index 0000000..c1406b0
--- /dev/null
+++ b/tests/verilog/const_sr.ys
@@ -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