Merge branch 'master' into eddie/submod_po

7 files changed, 98 insertions, 11 deletions

diff --git a/tests/various/abc9.v b/tests/various/abc9.v
index 30ebd4e26..f0b3f6837 100644
--- a/tests/various/abc9.v
+++ b/tests/various/abc9.v
@@ -9,3 +9,10 @@ wire w;
 unknown u(~i, w);
 unknown2 u2(w, o);
 endmodule
+
+module abc9_test032(input clk, d, r, output reg q);
+initial q = 1'b0;
+always @(negedge clk or negedge r)
+    if (!r) q <= 1'b0;
+    else q <= d;
+endmodule
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
index 5c9a4075d..0c7695089 100644
--- a/tests/various/abc9.ys
+++ b/tests/various/abc9.ys
@@ -14,6 +14,7 @@ design -import gate -as gate
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -show-ports miter
 
+
 design -load read
 hierarchy -top abc9_test028
 proc
@@ -22,3 +23,33 @@ abc9 -lut 4
 select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
 select -assert-count 1 t:unknown
 select -assert-none t:$lut t:unknown %% t: %D
+
+
+design -load read
+hierarchy -top abc9_test032
+proc
+clk2fflogic
+design -save gold
+
+abc9 -lut 4
+check
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 10 -verify -prove-asserts -show-ports miter
+
+
+design -reset
+read_verilog -icells <<EOT
+module abc9_test036(input clk, d, output q);
+(* keep *) reg w;
+$__ABC9_FF_ ff(.D(d), .Q(w));
+wire \ff.clock = clk;
+wire \ff.init = 1'b0;
+assign q = w;
+endmodule
+EOT
+abc9 -lut 4 -dff
diff --git a/tests/various/autoname.ys b/tests/various/autoname.ys
new file mode 100644
index 000000000..830962e81
--- /dev/null
+++ b/tests/various/autoname.ys
@@ -0,0 +1,19 @@
+read_ilang <<EOT
+autoidx 2
+module \top
+  wire output 3 $y
+  wire input 1 \a
+  wire input 2 \b
+  cell $and \b_$and_B
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 1
+    parameter \B_SIGNED 0
+    parameter \B_WIDTH 1
+    parameter \Y_WIDTH 1
+    connect \A \a
+    connect \B \b
+    connect \Y $y
+  end
+end
+EOT
+autoname
diff --git a/tests/various/bug1462.ys b/tests/various/bug1462.ys
deleted file mode 100644
index 15cab5121..000000000
--- a/tests/various/bug1462.ys
+++ /dev/null
@@ -1,11 +0,0 @@
-read_verilog << EOF
-module top(...);
-input wire [31:0] A;
-output wire [31:0] P;
-
-assign P = A * 32'h12300000;
-
-endmodule
-EOF
-
-synth_xilinx
diff --git a/tests/various/bug1531.ys b/tests/various/bug1531.ys
new file mode 100644
index 000000000..542223030
--- /dev/null
+++ b/tests/various/bug1531.ys
@@ -0,0 +1,34 @@
+read_verilog <<EOT
+module top (y, clk, w);
+   output reg y = 1'b0;
+   input clk, w;
+   reg [1:0] i = 2'b00;
+   always @(posedge clk)
+     // If the constant below is set to 2'b00, the correct output is generated.
+     //       vvvv
+     for (i = 1'b0; i < 2'b01; i = i + 2'b01) 
+       y <= w || i[1:1];
+endmodule
+EOT
+
+synth
+design -stash gate
+
+read_verilog <<EOT
+module gold (y, clk, w);
+  input clk;
+  wire [1:0] i;
+  input w;
+  output y;
+  reg y = 1'h0;
+  always @(posedge clk)
+      y <= w;
+  assign i = 2'h0;
+endmodule
+EOT
+proc gold
+
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 10 -verify -prove-asserts -show-ports miter
diff --git a/tests/various/help.ys b/tests/various/help.ys
new file mode 100644
index 000000000..9283ce8f1
--- /dev/null
+++ b/tests/various/help.ys
@@ -0,0 +1,2 @@
+help -all
+help -celltypes
diff --git a/tests/various/scratchpad.ys b/tests/various/scratchpad.ys
new file mode 100644
index 000000000..dc94081ea
--- /dev/null
+++ b/tests/various/scratchpad.ys
@@ -0,0 +1,5 @@
+scratchpad -set foo "bar baz"
+scratchpad -copy foo oof
+scratchpad -unset foo
+scratchpad -assert oof "bar baz"
+scratchpad -assert-unset foo