Merge pull request #3 from YosysHQ/Sergey/tests_ice40

Merge my changes to tests_ice40 branch

18 files changed, 271 insertions, 243 deletions

diff --git a/tests/ice40/dpram.ys b/tests/ice40/dpram.ys
index 77364e5ae..4f6a253ea 100644
--- a/tests/ice40/dpram.ys
+++ b/tests/ice40/dpram.ys
@@ -6,13 +6,10 @@ equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
 memory
 opt -full
 
-# TODO
-#equiv_opt -run prove: -assert null
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
+sat -verify -prove-asserts -seq 3 -set-init-zero -show-inputs -show-outputs miter
 
 design -load postopt
 cd top
 select -assert-count 1 t:SB_RAM40_4K
 select -assert-none t:SB_RAM40_4K %% t:* %D
-write_verilog dpram_synth.v
diff --git a/tests/ice40/dpram_tb.v b/tests/ice40/dpram_tb.v
deleted file mode 100644
index dede64614..000000000
--- a/tests/ice40/dpram_tb.v
+++ /dev/null
@@ -1,81 +0,0 @@
-module testbench;
-    reg clk;
-
-    initial begin
-       //  $dumpfile("testbench.vcd");
-       //  $dumpvars(0, testbench);
-
-        #5 clk = 0;
-        repeat (10000) begin
-            #5 clk = 1;
-            #5 clk = 0;
-        end
-    end
-
-
-    reg [7:0] data_a = 0;
-	reg [7:0] addr_a = 0;
-	reg [7:0] addr_b = 0;
-    reg we_a = 0;
-    reg re_a = 1;
-	wire [7:0] q_a;
-	reg mem_init = 0;
-
-	reg [7:0] pq_a;
-
-    always @(posedge clk) begin
-    #3;
-    data_a <= data_a + 17;
-
-    addr_a <= addr_a + 1;
-    addr_b <= addr_b + 1;
-    end
-
-    always @(posedge addr_a) begin
-    #10;
-        if(addr_a > 6'h3E)
-            mem_init <= 1;
-    end
-
-	always @(posedge clk) begin
-    //#3;
-    we_a <= !we_a;
-    end
-
-    reg [7:0] mem [(1<<8)-1:0];
-
-    always @(posedge clk) // Write memory.
-	begin
-	if (we_a)
-	mem[addr_a] <= data_a; // Using write address bus.
-	end
-	always @(posedge clk) // Read memory.
-	begin
-	pq_a <= mem[addr_b]; // Using read address bus.
-	end
-
-	top uut (
-		.din(data_a),
-		.write_en(we_a),
-		.waddr(addr_a),
-		.wclk(clk),
-		.raddr(addr_b),
-		.rclk(clk),
-		.dout(q_a)
-		);
-
-	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a), .B(pq_a));
-
-endmodule
-
-module uut_mem_checker(input clk, input init, input en, input [7:0] A, input [7:0] B);
-    always @(posedge clk)
-    begin
-        #1;
-        if (en == 1 & init == 1 & A !== B)
-        begin
-            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
-            $stop;
-        end
-    end
-endmodule
diff --git a/tests/ice40/latches.ys b/tests/ice40/latches.ys
index fe0d1f70e..f3562559e 100644
--- a/tests/ice40/latches.ys
+++ b/tests/ice40/latches.ys
@@ -1,6 +1,15 @@
 read_verilog latches.v
+design -save read
+
+proc
+async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock
+flatten
+synth_ice40
+equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+
+design -load read
 synth_ice40
 cd top
 select -assert-count 4 t:SB_LUT4
 select -assert-none t:SB_LUT4 %% t:* %D
-write_verilog latches_synth.v
diff --git a/tests/ice40/latches_tb.v b/tests/ice40/latches_tb.v
deleted file mode 100644
index b0585264b..000000000
--- a/tests/ice40/latches_tb.v
+++ /dev/null
@@ -1,57 +0,0 @@
-module testbench;
-    reg clk;
-
-    initial begin
-        // $dumpfile("testbench.vcd");
-        // $dumpvars(0, testbench);
-
-        #5 clk = 0;
-        repeat (10000) begin
-            #5 clk = 1;
-            #5 clk = 0;
-        end
-    end
-
-
-    reg [2:0] dinA = 0;
-    wire doutB,doutB1,doutB2;
-	reg lat,latn,latsr = 0;
-
-    top uut (
-        .clk (clk ),
-        .a (dinA[0] ),
-        .pre (dinA[1] ),
-        .clr (dinA[2] ),
-        .b (doutB ),
-        .b1 (doutB1 ),
-        .b2 (doutB2 )
-    );
-
-    always @(posedge clk) begin
-    #3;
-    dinA <= dinA + 1;
-    end
-
-    	always @*
-		if ( clk )
-			lat <= dinA[0];
-
-
-    	always @*
-		if ( !clk )
-			latn <= dinA[0];
-
-
-		always @*
-		if ( dinA[2] )
-			latsr <= 1'b0;
-		else if ( dinA[1] )
-			latsr <= 1'b1;
-		else if ( clk )
-			latsr <= dinA[0];
-
-	assert_dff lat_test(.clk(clk), .test(doutB), .pat(lat));
-    assert_dff latn_test(.clk(clk), .test(doutB1), .pat(latn));
-    assert_dff latsr_test(.clk(clk), .test(doutB2), .pat(latsr));
-
-endmodule
diff --git a/tests/ice40/memory.ys b/tests/ice40/memory.ys
index 9b7490cd8..a66afbae6 100644
--- a/tests/ice40/memory.ys
+++ b/tests/ice40/memory.ys
@@ -6,13 +6,10 @@ equiv_opt -run :prove -map +/ice40/cells_sim.v synth_ice40
 memory
 opt -full
 
-# TODO
-#equiv_opt -run prove: -assert null
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
-#sat -verify -prove-asserts -tempinduct -show-inputs -show-outputs miter
+sat -verify -prove-asserts -seq 5 -set-init-zero -show-inputs -show-outputs miter
 
 design -load postopt
 cd top
 select -assert-count 1 t:SB_RAM40_4K
 select -assert-none t:SB_RAM40_4K %% t:* %D
-write_verilog memory_synth.v
diff --git a/tests/ice40/memory_tb.v b/tests/ice40/memory_tb.v
deleted file mode 100644
index be69374eb..000000000
--- a/tests/ice40/memory_tb.v
+++ /dev/null
@@ -1,79 +0,0 @@
-module testbench;
-    reg clk;
-
-    initial begin
-       //  $dumpfile("testbench.vcd");
-       //  $dumpvars(0, testbench);
-
-        #5 clk = 0;
-        repeat (10000) begin
-            #5 clk = 1;
-            #5 clk = 0;
-        end
-    end
-
-
-    reg [7:0] data_a = 0;
-	reg [5:0] addr_a = 0;
-    reg we_a = 0;
-    reg re_a = 1;
-	wire [7:0] q_a;
-	reg mem_init = 0;
-
-	reg [7:0] pq_a;
-
-    top uut (
-    .data_a(data_a),
-	.addr_a(addr_a),
-	.we_a(we_a),
-	.clk(clk),
-	.q_a(q_a)
-    );
-
-    always @(posedge clk) begin
-    #3;
-    data_a <= data_a + 17;
-
-    addr_a <= addr_a + 1;
-    end
-
-    always @(posedge addr_a) begin
-    #10;
-        if(addr_a > 6'h3E)
-            mem_init <= 1;
-    end
-
-	always @(posedge clk) begin
-    //#3;
-    we_a <= !we_a;
-    end
-
-    // Declare the RAM variable for check
-	reg [7:0] ram[63:0];
-
-	// Port A for check
-	always @ (posedge clk)
-	begin
-		if (we_a)
-		begin
-			ram[addr_a] <= data_a;
-			pq_a <= data_a;
-		end
-		pq_a <= ram[addr_a];
-	end
-
-	uut_mem_checker port_a_test(.clk(clk), .init(mem_init), .en(!we_a), .A(q_a), .B(pq_a));
-
-endmodule
-
-module uut_mem_checker(input clk, input init, input en, input [7:0] A, input [7:0] B);
-    always @(posedge clk)
-    begin
-        #1;
-        if (en == 1 & init == 1 & A !== B)
-        begin
-            $display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
-            $stop;
-        end
-    end
-endmodule
diff --git a/tests/ice40/run-test.sh b/tests/ice40/run-test.sh
index bd9d35314..941dcaecd 100755
--- a/tests/ice40/run-test.sh
+++ b/tests/ice40/run-test.sh
@@ -21,13 +21,13 @@ for x in *.ys; do
 	fi
 done
 
-for s in *.sh; do
-	if [ "$s" != "run-test.sh" ]; then
-		echo "all:: run-$s"
-		echo "run-$s:"
-		echo "	@echo 'Running $s..'"
-		echo "	@bash $s"
-	fi
-done
+#for s in *.sh; do
+#	if [ "$s" != "run-test.sh" ]; then
+#		echo "all:: run-$s"
+#		echo "run-$s:"
+#		echo "	@echo 'Running $s..'"
+#		echo "	@bash $s"
+#	fi
+#done
 } > run-test.mk
 exec ${MAKE:-make} -f run-test.mk
diff --git a/tests/opt/opt_expr.ys b/tests/opt/opt_expr.ys
index f0306efa1..ecc2c8da8 100644
--- a/tests/opt/opt_expr.ys
+++ b/tests/opt/opt_expr.ys
@@ -221,3 +221,73 @@ check
 equiv_opt opt_expr -fine
 design -load postopt
 select -assert-count 1 t:$alu r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
+
+###########
+
+design -reset
+read_verilog -icells <<EOT
+module opt_expr_shiftx_1bit(input [2:0] a, input [1:0] b, output y);
+    \$shiftx #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(4), .B_WIDTH(2), .Y_WIDTH(1)) shiftx (.A({1'bx,a}), .B(b), .Y(y));
+endmodule
+EOT
+check
+
+equiv_opt opt_expr
+design -load postopt
+select -assert-count 1 t:$shiftx r:A_WIDTH=3 %i
+
+###########
+
+design -reset
+read_verilog -icells <<EOT
+module opt_expr_shiftx_3bit(input [9:0] a, input [3:0] b, output [2:0] y);
+    \$shiftx #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(14), .B_WIDTH(4), .Y_WIDTH(3)) shiftx (.A({4'bxx00,a}), .B(b), .Y(y));
+endmodule
+EOT
+check
+
+equiv_opt opt_expr
+design -load postopt
+select -assert-count 1 t:$shiftx r:A_WIDTH=12 %i
+
+###########
+
+design -reset
+read_verilog -icells <<EOT
+module opt_expr_shift_1bit(input [2:0] a, input [1:0] b, output y);
+    \$shift #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(4), .B_WIDTH(2), .Y_WIDTH(1)) shift (.A({1'b0,a}), .B(b), .Y(y));
+endmodule
+EOT
+check
+
+equiv_opt opt_expr
+design -load postopt
+select -assert-count 1 t:$shift r:A_WIDTH=3 %i
+
+###########
+
+design -reset
+read_verilog -icells <<EOT
+module opt_expr_shift_3bit(input [9:0] a, input [3:0] b, output [2:0] y);
+    \$shift #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(14), .B_WIDTH(4), .Y_WIDTH(3)) shift (.A({4'b0x0x,a}), .B(b), .Y(y));
+endmodule
+EOT
+check
+
+equiv_opt opt_expr
+design -load postopt
+select -assert-count 1 t:$shift r:A_WIDTH=10 %i
+
+###########
+
+design -reset
+read_verilog -icells <<EOT
+module opt_expr_shift_3bit_keepdc(input [9:0] a, input [3:0] b, output [2:0] y);
+    \$shift #(.A_SIGNED(0), .B_SIGNED(0), .A_WIDTH(14), .B_WIDTH(4), .Y_WIDTH(3)) shift (.A({4'b0x0x,a}), .B(b), .Y(y));
+endmodule
+EOT
+check
+
+equiv_opt opt_expr -keepdc
+design -load postopt
+select -assert-count 1 t:$shift r:A_WIDTH=13 %i
diff --git a/tests/sat/initval.v b/tests/sat/initval.v
index 5b661f8d6..81f71b5ba 100644
--- a/tests/sat/initval.v
+++ b/tests/sat/initval.v
@@ -1,6 +1,7 @@
-module test(input clk, input [3:0] bar, output [3:0] foo);
+module test(input clk, input [3:0] bar, output [3:0] foo, asdf);
   reg [3:0] foo = 0;
   reg [3:0] last_bar = 0;
+  reg [3:0] asdf = 4'b1xxx;
 
   always @*
     foo[1:0] <= bar[1:0];
@@ -11,5 +12,10 @@ module test(input clk, input [3:0] bar, output [3:0] foo);
   always @(posedge clk)
     last_bar <= bar;
 
+  always @(posedge clk)
+    asdf[3] <= bar[3];
+  always @*
+    asdf[2:0] = 3'b111;
+
   assert property (foo == {last_bar[3:2], bar[1:0]});
 endmodule
diff --git a/tests/simple/realexpr.v b/tests/simple/realexpr.v
index 5b756e6be..74ed8faa5 100644
--- a/tests/simple/realexpr.v
+++ b/tests/simple/realexpr.v
@@ -1,4 +1,3 @@
-
 module demo_001(y1, y2, y3, y4);
 	output [7:0] y1, y2, y3, y4;
 
@@ -22,3 +21,13 @@ module demo_002(y0, y1, y2, y3);
 	assign y3 = 1 ? -1 : 'd0;
 endmodule
 
+module demo_003(output A, B);
+	parameter real p = 0;
+	assign A = (p==1.0);
+	assign B = (p!="1.000000");
+endmodule
+
+module demo_004(output A, B, C, D);
+	demo_003 #(1.0) demo_real (A, B);
+	demo_003 #(1) demo_int (C, D);
+endmodule
diff --git a/tests/techmap/.gitignore b/tests/techmap/.gitignore
index 397b4a762..cfed22fc5 100644
--- a/tests/techmap/.gitignore
+++ b/tests/techmap/.gitignore
@@ -1 +1,2 @@
 *.log
+/*.mk
diff --git a/tests/techmap/clkbufmap.ys b/tests/techmap/clkbufmap.ys
new file mode 100644
index 000000000..f1277864e
--- /dev/null
+++ b/tests/techmap/clkbufmap.ys
@@ -0,0 +1,96 @@
+read_verilog <<EOT
+module clkbuf (input i, (* clkbuf_driver *) output o); endmodule
+module dff ((* clkbuf_sink *) input clk, input d, output q); endmodule
+module dffe ((* clkbuf_sink *) input c, input d, e, output q); endmodule
+module latch (input e, d, output q); endmodule
+module clkgen (output o); endmodule
+
+module top(input clk1, clk2, clk3, d, e, output [4:0] q);
+wire clk4, clk5, clk6;
+dff s0 (.clk(clk1), .d(d), .q(q[0]));
+dffe s1 (.c(clk2), .d(d), .e(e), .q(q[1]));
+latch s2 (.e(clk3), .d(d), .q(q[2]));
+sub s3 (.sclk4(clk4), .sclk5(clk5), .sclk6(clk6), .sd(d), .sq(q[3]));
+dff s4 (.clk(clk4), .d(d), .q(q[4]));
+dff s5 (.clk(clk5), .d(d), .q(q[4]));
+dff s6 (.clk(clk6), .d(d), .q(q[4]));
+endmodule
+
+module sub(output sclk4, output sclk5, output sclk6, input sd, output sq);
+wire tmp;
+clkgen s7(.o(sclk4));
+clkgen s8(.o(sclk5));
+clkgen s9(.o(tmp));
+clkbuf s10(.i(tmp), .o(sclk6));
+dff s11(.clk(sclk4), .d(sd), .q(sq));
+endmodule
+EOT
+
+hierarchy -auto-top
+design -save ref
+
+# ----------------------
+
+design -load ref
+clkbufmap -buf clkbuf o:i
+select -assert-count 3 top/t:clkbuf
+select -assert-count 2 sub/t:clkbuf
+select -set clk1 w:clk1 %a %co t:clkbuf %i          # Find 'clk1' fanouts that are 'clkbuf'
+select -assert-count 1 @clk1                        # Check there is one such fanout
+select -assert-count 1 @clk1 %x:+[o] %co c:s* %i    # Check that the 'o' of that clkbuf drives one fanout
+select -assert-count 1 @clk1 %x:+[o] %co c:s0 %i    # And that one fanout is 's0'
+select -set clk2 w:clk2 %a %co t:clkbuf %i
+select -assert-count 1 @clk2
+select -assert-count 1 @clk2 %x:+[o] %co c:s* %i
+select -assert-count 1 @clk2 %x:+[o] %co c:s1 %i
+select -set clk5 w:clk5 %a %ci t:clkbuf %i
+select -assert-count 1 @clk5
+select -assert-count 1 @clk5 %x:+[o] %co c:s5 %i
+select -assert-count 1 @clk5 %x:+[i] %ci c:s3 %i
+select -set sclk4 w:sclk4 %a %ci t:clkbuf %i
+select -assert-count 1 @sclk4
+select -assert-count 1 @sclk4 %x:+[o] %co c:s11 %i
+select -assert-count 1 @sclk4 %x:+[i] %ci c:s7 %i
+
+# ----------------------
+
+design -load ref
+setattr -set clkbuf_inhibit 0 w:clk1
+setattr -set clkbuf_inhibit 1 w:clk2
+clkbufmap -buf clkbuf o:i
+select -assert-count 2 top/t:clkbuf
+select -set clk1 w:clk1 %a %co t:clkbuf %i          # Find 'clk1' fanouts that are 'clkbuf'
+select -assert-count 1 @clk1                        # Check there is one such fanout
+select -assert-count 1 @clk1 %x:+[o] %co c:s* %i    # Check that the 'o' of that clkbuf drives one fanout
+select -assert-count 1 @clk1 %x:+[o] %co c:s0 %i    # And that one fanout is 's0'
+select -assert-count 0 w:clk2 %a %co t:clkbuf %i
+
+# ----------------------
+
+design -load ref
+setattr -set clkbuf_inhibit 1 w:clk1
+setattr -set buffer_type "bufg" w:clk2
+clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d
+select -assert-count 3 top/t:clkbuf
+select -assert-count 2 sub/t:clkbuf
+select -set clk1 w:clk1 %a %co t:clkbuf %i          # Find 'clk1' fanouts that are 'clkbuf'
+select -assert-count 1 @clk1                        # Check there is one such fanout
+select -assert-count 1 @clk1 %x:+[o] %co c:s* %i    # Check that the 'o' of that clkbuf drives one fanout
+select -assert-count 1 @clk1 %x:+[o] %co c:s0 %i    # And that one fanout is 's0'
+select -set clk2 w:clk2 %a %co t:clkbuf %i          # Find 'clk1' fanouts that are 'clkbuf'
+select -assert-count 1 @clk2                        # Check there is one such fanout
+select -assert-count 1 @clk2 %x:+[o] %co c:s* %i    # Check that the 'o' of that clkbuf drives one fanout
+select -assert-count 1 @clk2 %x:+[o] %co c:s1 %i    # And that one fanout is 's0'
+
+# ----------------------
+
+design -load ref
+setattr -set buffer_type "none" w:clk1
+setattr -set buffer_type "bufr" w:clk2
+setattr -set buffer_type "bufr" w:sclk4
+setattr -set buffer_type "bufr" w:sclk5
+clkbufmap -buf clkbuf o:i w:* a:buffer_type=none a:buffer_type=bufr %u %d
+select -assert-count 0 w:clk1 %a %co t:clkbuf %i
+select -assert-count 0 w:clk2 %a %co t:clkbuf %i
+select -assert-count 0 top/t:clkbuf
+select -assert-count 1 sub/t:clkbuf
diff --git a/tests/techmap/recursive.v b/tests/techmap/recursive.v
new file mode 100644
index 000000000..d281b21d8
--- /dev/null
+++ b/tests/techmap/recursive.v
@@ -0,0 +1,8 @@
+module top;
+sub s0();
+foo f0();
+endmodule
+
+module foo;
+sub s0();
+endmodule
diff --git a/tests/techmap/recursive_map.v b/tests/techmap/recursive_map.v
new file mode 100644
index 000000000..934256552
--- /dev/null
+++ b/tests/techmap/recursive_map.v
@@ -0,0 +1,4 @@
+module sub;
+    sub _TECHMAP_REPLACE_ ();
+    bar f0();
+endmodule
diff --git a/tests/techmap/recursive_runtest.sh b/tests/techmap/recursive_runtest.sh
new file mode 100644
index 000000000..30c79bf03
--- /dev/null
+++ b/tests/techmap/recursive_runtest.sh
@@ -0,0 +1,3 @@
+set -ev
+
+../../yosys -p 'hierarchy -top top; techmap -map recursive_map.v -max_iter 1; select -assert-count 2 t:sub; select -assert-count 2 t:bar' recursive.v
diff --git a/tests/techmap/run-test.sh b/tests/techmap/run-test.sh
index e2fc11e52..96489ff15 100755
--- a/tests/techmap/run-test.sh
+++ b/tests/techmap/run-test.sh
@@ -1,10 +1,20 @@
-#!/bin/bash
+#!/usr/bin/env bash
 set -e
-for x in *_runtest.sh; do
-	echo "Running $x.."
-	if ! bash $x &> ${x%.sh}.log; then
-		tail ${x%.sh}.log
-		echo ERROR
-		exit 1
+{
+echo "all::"
+for x in *.ys; do
+	echo "all:: run-$x"
+	echo "run-$x:"
+	echo "	@echo 'Running $x..'"
+	echo "	@../../yosys -ql ${x%.ys}.log $x"
+done
+for s in *.sh; do
+	if [ "$s" != "run-test.sh" ]; then
+		echo "all:: run-$s"
+		echo "run-$s:"
+		echo "	@echo 'Running $s..'"
+		echo "	@bash $s > ${s%.sh}.log 2>&1"
 	fi
 done
+} > run-test.mk
+exec ${MAKE:-make} -f run-test.mk
diff --git a/tests/various/mem2reg.ys b/tests/various/mem2reg.ys
new file mode 100644
index 000000000..85d6267c5
--- /dev/null
+++ b/tests/various/mem2reg.ys
@@ -0,0 +1,14 @@
+read_verilog <<EOT
+module top;
+parameter DATADEPTH=2;
+parameter DATAWIDTH=1;
+(* keep, nomem2reg *) reg [DATAWIDTH-1:0] data1 [DATADEPTH-1:0];
+(* keep, mem2reg *) reg [DATAWIDTH-1:0] data2 [DATADEPTH-1:0];
+endmodule
+EOT
+
+proc
+cd top
+select -assert-count 1 m:data1 a:src=<<EOT:4 %i
+select -assert-count 2 w:data2[*] a:src=<<EOT:5 %i
+select -assert-none a:mem2reg
diff --git a/tests/various/pmgen_reduce.ys b/tests/various/pmgen_reduce.ys
new file mode 100644
index 000000000..c214d3f25
--- /dev/null
+++ b/tests/various/pmgen_reduce.ys
@@ -0,0 +1,21 @@
+test_pmgen -generate reduce
+hierarchy -top pmtest_test_pmgen_pm_reduce
+flatten; opt_clean
+
+design -save gold
+test_pmgen -reduce_chain
+design -stash gate
+
+design -copy-from gold -as gold pmtest_test_pmgen_pm_reduce
+design -copy-from gate -as gate pmtest_test_pmgen_pm_reduce
+miter -equiv -flatten -make_assert gold gate miter
+sat -verify -prove-asserts miter
+
+design -load gold
+test_pmgen -reduce_tree
+design -stash gate
+
+design -copy-from gold -as gold pmtest_test_pmgen_pm_reduce
+design -copy-from gate -as gate pmtest_test_pmgen_pm_reduce
+miter -equiv -flatten -make_assert gold gate miter
+sat -verify -prove-asserts miter