16 files changed, 182 insertions, 10 deletions
diff --git a/tests/arch/fabulous/.gitignore b/tests/arch/fabulous/.gitignore
new file mode 100644
index 000000000..9a71dca69
--- /dev/null
+++ b/tests/arch/fabulous/.gitignore
@@ -0,0 +1,4 @@
+*.log
+/run-test.mk
++*_synth.v
++*_testbench
diff --git a/tests/arch/fabulous/complexflop.ys b/tests/arch/fabulous/complexflop.ys
new file mode 100644
index 000000000..13f4522b9
--- /dev/null
+++ b/tests/arch/fabulous/complexflop.ys
@@ -0,0 +1,37 @@
+read_verilog <<EOT
+module top ( input d0, d1, d2, d3, ce, sr, clk, output reg q0, q1, q2, q3 );
+    always @(posedge clk)
+      begin
+        if (sr) begin
+            q0 <= 1'b0;
+            q1 <= 1'b1;
+        end else begin
+            q0 <= d0;
+            q1 <= d1;
+        end
+        if (ce) begin
+          if (sr) begin
+              q2 <= 1'b0;
+              q3 <= 1'b1;
+          end else begin
+              q2 <= d2;
+              q3 <= d3;
+          end
+        end
+      end
+endmodule
+EOT
+
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/fabulous/prims.v synth_fabulous -complex-dff # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:LUTFF_SR
+select -assert-count 1 t:LUTFF_SS
+select -assert-count 1 t:LUTFF_ESR
+select -assert-count 1 t:LUTFF_ESS
+
+select -assert-none t:LUTFF_SR t:LUTFF_SS t:LUTFF_ESR t:LUTFF_ESS %% t:* %D
diff --git a/tests/arch/fabulous/counter.ys b/tests/arch/fabulous/counter.ys
new file mode 100644
index 000000000..d79b378a6
--- /dev/null
+++ b/tests/arch/fabulous/counter.ys
@@ -0,0 +1,26 @@
+read_verilog <<EOT
+module top ( out, clk, reset );
+    output [7:0] out;
+    input clk, reset;
+    reg [7:0] out;
+
+    always @(posedge clk)
+      if (reset)
+          out <= 8'b0;
+      else
+          out <= out + 1;
+endmodule
+EOT
+
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:LUT2
+select -assert-count 7 t:LUT3
+select -assert-count 4 t:LUT4
+select -assert-count 8 t:LUTFF
+select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D
diff --git a/tests/arch/fabulous/custom_map.v b/tests/arch/fabulous/custom_map.v
new file mode 100644
index 000000000..1538e837b
--- /dev/null
+++ b/tests/arch/fabulous/custom_map.v
@@ -0,0 +1,3 @@
+module AND(input [7:0] A, B, output [7:0] Y);
+	ALU #(.MODE("AND")) _TECHMAP_REPLACE_ (.A(A), .B(B), .Y(Y));
+endmodule
diff --git a/tests/arch/fabulous/custom_prims.v b/tests/arch/fabulous/custom_prims.v
new file mode 100644
index 000000000..4989188e2
--- /dev/null
+++ b/tests/arch/fabulous/custom_prims.v
@@ -0,0 +1,8 @@
+(* blackbox *)
+module AND(input [7:0] A, B, output [7:0] Y);
+endmodule
+
+(* blackbox *)
+module ALU(input [7:0] A, B, output [7:0] Y);
+parameter MODE = "";
+endmodule
diff --git a/tests/arch/fabulous/customisation.ys b/tests/arch/fabulous/customisation.ys
new file mode 100644
index 000000000..0e78d2e56
--- /dev/null
+++ b/tests/arch/fabulous/customisation.ys
@@ -0,0 +1,10 @@
+read_verilog <<EOT
+module prim_test(input [7:0] a, b, output [7:0] q);
+	AND and_i (.A(a), .B(b), .Y(q));
+endmodule
+EOT
+
+# Test adding custom primitives and techmap rules
+synth_fabulous -top prim_test -extra-plib custom_prims.v -extra-map custom_map.v
+cd prim_test
+select -assert-count 1 t:ALU
diff --git a/tests/arch/fabulous/fsm.ys b/tests/arch/fabulous/fsm.ys
new file mode 100644
index 000000000..9c3831682
--- /dev/null
+++ b/tests/arch/fabulous/fsm.ys
@@ -0,0 +1,19 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/fabulous/prims.v synth_fabulous
+async2sync
+miter -equiv -make_assert -flatten gold gate miter
+stat
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd fsm # Constrain all select calls below inside the top module
+
+select -assert-count 6 t:LUTFF
+select -assert-max 4 t:LUT2
+select -assert-max 2 t:LUT3
+select -assert-max 9 t:LUT4
+select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D
diff --git a/tests/arch/fabulous/logic.ys b/tests/arch/fabulous/logic.ys
new file mode 100644
index 000000000..730d9ab54
--- /dev/null
+++ b/tests/arch/fabulous/logic.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-max 1 t:LUT1
+select -assert-max 6 t:LUT2
+select -assert-max 2 t:LUT4
+select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D
diff --git a/tests/arch/fabulous/regfile.ys b/tests/arch/fabulous/regfile.ys
new file mode 100644
index 000000000..8d1eedef0
--- /dev/null
+++ b/tests/arch/fabulous/regfile.ys
@@ -0,0 +1,33 @@
+read_verilog <<EOT
+module sync_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb);
+	reg [3:0] mem[0:31];
+	always @(posedge clk)
+		if (we) mem[aw] <= wd;
+	always @(posedge clk)
+		ra <= mem[aa];
+	always @(posedge clk)
+		rb <= mem[ab];
+endmodule
+EOT
+
+synth_fabulous -top sync_sync
+cd sync_sync
+select -assert-count 1 t:RegFile_32x4
+
+design -reset
+
+read_verilog <<EOT
+module async_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb);
+	reg [3:0] mem[0:31];
+	always @(posedge clk)
+		if (we) mem[aw] <= wd;
+	always @(posedge clk)
+		ra <= mem[aa];
+	always @(*)
+		rb <= mem[ab];
+endmodule
+EOT
+
+synth_fabulous -top async_sync
+cd async_sync
+select -assert-count 1 t:RegFile_32x4
diff --git a/tests/arch/fabulous/tribuf.ys b/tests/arch/fabulous/tribuf.ys
new file mode 100644
index 000000000..0dcf1cbab
--- /dev/null
+++ b/tests/arch/fabulous/tribuf.ys
@@ -0,0 +1,12 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/fabulous/prims.v -map +/simcells.v synth_fabulous -iopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd tristate # Constrain all select calls below inside the top module
+select -assert-count 3 t:IO_1_bidirectional_frame_config_pass
+select -assert-max 1 t:LUT1
+select -assert-none t:IO_1_bidirectional_frame_config_pass t:LUT1 %% t:* %D
diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys
index b7983cfa4..c1509cabc 100644
--- a/tests/arch/ice40/bug1597.ys
+++ b/tests/arch/ice40/bug1597.ys
@@ -3,7 +3,7 @@ module top (
     input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5,
         PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25,
     output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18,
-        PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24,
+        PIN_19,
 );
     assign USBPU = 0;
 
@@ -67,6 +67,7 @@ module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output w
     SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]);
 endmodule
 EOT
+read_verilog -lib +/ice40/cells_sim.v
 hierarchy -top top
 flatten
-equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40
+equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40
diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys
index 71b68431e..e779ab207 100644
--- a/tests/arch/ice40/ice40_opt.ys
+++ b/tests/arch/ice40/ice40_opt.ys
@@ -21,6 +21,7 @@ module top(input CI, I0, output [1:0] CO, output O);
 endmodule
 EOT
 
+read_verilog -icells -lib +/ice40/abc9_model.v +/ice40/cells_sim.v
 equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt
 design -load postopt
 select -assert-count 1 t:*
diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys
index 56c9cabb3..0a5b9356a 100644
--- a/tests/arch/intel_alm/counter.ys
+++ b/tests/arch/intel_alm/counter.ys
@@ -2,7 +2,7 @@ read_verilog ../common/counter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check
+equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
@@ -17,7 +17,7 @@ read_verilog ../common/counter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check
+equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd top # Constrain all select calls below inside the top module
 
diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys
index 0ba3901f7..79e5a322c 100644
--- a/tests/arch/xilinx/abc9_dff.ys
+++ b/tests/arch/xilinx/abc9_dff.ys
@@ -12,6 +12,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
 FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
 endmodule
 EOT
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 6 t:FD*
@@ -31,6 +32,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
 FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
 endmodule
 EOT
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 4 t:FD*
@@ -54,6 +56,7 @@ logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=.*1' with \(\* abc9_flop
 logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
 logger -expect warning "Whitebox 'FDSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
 logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 8 t:FD*
@@ -75,6 +78,7 @@ always @(posedge clk or posedge pre)
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 1 t:FDCE
@@ -94,6 +98,7 @@ assign q = ~r;
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 1 t:FDRE %co w:r %i
@@ -111,6 +116,7 @@ assign q2 = r;
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-count 1 t:FDRE %co %a w:r %i
@@ -128,6 +134,7 @@ assign o = r1 | r2;
 endmodule
 EOT
 proc
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 
 
diff --git a/tests/arch/xilinx/opt_lut_ins.ys b/tests/arch/xilinx/opt_lut_ins.ys
index a01d02179..2328919a3 100644
--- a/tests/arch/xilinx/opt_lut_ins.ys
+++ b/tests/arch/xilinx/opt_lut_ins.ys
@@ -18,6 +18,7 @@ end
 
 EOF
 
+read_verilog -lib +/xilinx/cells_sim.v
 equiv_opt -assert -map +/xilinx/cells_sim.v opt_lut_ins -tech xilinx
 
 design -load postopt
diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys
index c09699411..9f0b27ced 100644
--- a/tests/arch/xilinx/xilinx_dffopt.ys
+++ b/tests/arch/xilinx/xilinx_dffopt.ys
@@ -5,7 +5,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -52,7 +52,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -100,7 +100,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -137,7 +137,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -183,7 +183,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;
 
@@ -232,7 +232,7 @@ read_verilog << EOT
 module t0 (...);
 input wire clk;
 input wire [7:0] i;
-output wire [7:0] o;
+output wire [0:0] o;
 
 wire [7:0] tmp ;