5 files changed, 89 insertions, 1 deletions
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index de7bc68cf..bcf2b964a 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -55,5 +55,5 @@ done
 
 for y in *.ys; do
     echo "Running $y."
-    ../../yosys $y -ql ${y%.*}.log
+    ../../yosys -ql ${y%.*}.log $y
 done
diff --git a/tests/arch/xilinx/dsp_abc9.ys b/tests/arch/xilinx/dsp_abc9.ys
new file mode 100644
index 000000000..909e54149
--- /dev/null
+++ b/tests/arch/xilinx/dsp_abc9.ys
@@ -0,0 +1,37 @@
+read_verilog <<EOT
+module top(input [24:0] A, input [17:0] B, output [47:0] P);
+DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
+endmodule
+EOT
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt
+scc -expect 0
+
+
+design -reset
+read_verilog <<EOT
+module top(input signed [24:0] A, input signed [17:0] B, output [47:0] P);
+assign P = A * B;
+endmodule
+EOT
+synth_xilinx -abc9
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt -full -fine
+select -assert-count 1 t:$mul
+select -assert-count 0 t:* t:$mul %D
+
+
+design -reset
+read_verilog -icells -formal <<EOT
+module top(output [42:0] P);
+\$__MUL25X18 mul (.A(42), .B(42), .Y(P));
+assert property (P == 42*42);
+endmodule
+EOT
+techmap -map +/xilinx/xc7_dsp_map.v
+verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
+synth_xilinx -abc9
+techmap -autoproc -wb -map +/xilinx/cells_sim.v
+opt -full -fine
+select -assert-count 0 t:* t:$assert %d
+sat -verify -prove-asserts
diff --git a/tests/verilog/.gitignore b/tests/verilog/.gitignore
index b48f808a1..34da23437 100644
--- a/tests/verilog/.gitignore
+++ b/tests/verilog/.gitignore
@@ -1,3 +1,5 @@
 /*.log
 /*.out
 /run-test.mk
+/const_arst.v
+/const_sr.v
diff --git a/tests/verilog/const_arst.ys b/tests/verilog/const_arst.ys
new file mode 100644
index 000000000..df720575c
--- /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
index 000000000..c1406b0a0
--- /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