Merge remote-tracking branch 'origin/master' into xaig_dff

21 files changed, 189 insertions, 54 deletions

diff --git a/tests/arch/xilinx/add_sub.ys b/tests/arch/xilinx/add_sub.ys
index 9dbddce47..313948cc5 100644
--- a/tests/arch/xilinx/add_sub.ys
+++ b/tests/arch/xilinx/add_sub.ys
@@ -1,7 +1,7 @@
 read_verilog ../common/add_sub.v
 hierarchy -top top
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # 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 14 t:LUT2
diff --git a/tests/arch/xilinx/adffs.ys b/tests/arch/xilinx/adffs.ys
index c0ff6a2e2..3328f9edc 100644
--- a/tests/arch/xilinx/adffs.ys
+++ b/tests/arch/xilinx/adffs.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top adff
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd adff # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDCE %% t:* %D
 design -load read
 hierarchy -top adffn
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd adffn # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -28,7 +28,7 @@ select -assert-none t:BUFG t:FDCE t:INV %% t:* %D
 design -load read
 hierarchy -top dffs
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd dffs # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -40,7 +40,7 @@ select -assert-none t:BUFG t:FDSE %% t:* %D
 design -load read
 hierarchy -top ndffnr
 proc
-equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync  -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd ndffnr # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
diff --git a/tests/arch/xilinx/attributes_test.ys b/tests/arch/xilinx/attributes_test.ys
index 4c881b280..7bdd94a63 100644
--- a/tests/arch/xilinx/attributes_test.ys
+++ b/tests/arch/xilinx/attributes_test.ys
@@ -1,7 +1,7 @@
 # Check that blockram memory without parameters is not modified
 read_verilog ../common/memory_attributes/attributes_test.v
 hierarchy -top block_ram
-synth_xilinx -top block_ram
+synth_xilinx -top block_ram -noiopad
 cd block_ram # Constrain all select calls below inside the top module
 select -assert-count 1 t:RAMB18E1
  
@@ -9,7 +9,7 @@ select -assert-count 1 t:RAMB18E1
 design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
 hierarchy -top distributed_ram
-synth_xilinx -top distributed_ram
+synth_xilinx -top distributed_ram -noiopad
 cd distributed_ram # Constrain all select calls below inside the top module
 select -assert-count 8 t:RAM32X1D
  
@@ -18,7 +18,7 @@ design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
 prep
 setattr -mod -set ram_style "distributed" block_ram
-synth_xilinx -top block_ram
+synth_xilinx -top block_ram -noiopad
 cd block_ram # Constrain all select calls below inside the top module
 select -assert-count 32 t:RAM128X1D
  
@@ -27,7 +27,7 @@ design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
 prep
 setattr -mod -set logic_block 1 block_ram
-synth_xilinx -top block_ram
+synth_xilinx -top block_ram -noiopad
 cd block_ram # Constrain all select calls below inside the top module
 select -assert-count 0 t:RAMB18E1
 select -assert-count 32 t:RAM128X1D
@@ -35,13 +35,13 @@ select -assert-count 32 t:RAM128X1D
 # Set ram_style block to a distributed memory; will be implemented as blockram
 design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
-synth_xilinx -top distributed_ram_manual
+synth_xilinx -top distributed_ram_manual -noiopad
 cd distributed_ram_manual # Constrain all select calls below inside the top module
 select -assert-count 1 t:RAMB18E1
  
 # Set synthesis, ram_block block to a distributed memory; will be implemented as blockram
 design -reset
 read_verilog ../common/memory_attributes/attributes_test.v
-synth_xilinx -top distributed_ram_manual_syn
+synth_xilinx -top distributed_ram_manual_syn -noiopad
 cd distributed_ram_manual_syn # Constrain all select calls below inside the top module
 select -assert-count 1 t:RAMB18E1
diff --git a/tests/arch/xilinx/blockram.ys b/tests/arch/xilinx/blockram.ys
index bb908cbbf..ed743cf44 100644
--- a/tests/arch/xilinx/blockram.ys
+++ b/tests/arch/xilinx/blockram.ys
@@ -3,28 +3,28 @@
 # Memory bits <= 18K; Data width <= 36; Address width <= 14: -> RAMB18E1
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 1 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 18 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 14 -set DATA_WIDTH 1 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 9 -set DATA_WIDTH 36 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -32,7 +32,7 @@ select -assert-count 1 t:RAMB18E1
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 8 -set DATA_WIDTH 2 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 0 t:RAMB18E1
 select -assert-count 4 t:RAM128X1D
@@ -41,7 +41,7 @@ select -assert-count 4 t:RAM128X1D
 design -reset
 read_verilog ../common/blockram.v
 chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 36 sync_ram_sdp
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB36E1
 
@@ -52,7 +52,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set ram_style "block" m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -60,7 +60,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set ram_block 1 m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -68,7 +68,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set ram_style "dont_infer_a_ram_pretty_please" m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 0 t:RAMB18E1
 
@@ -76,7 +76,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 10 -chparam DATA_WIDTH 1 
 setattr -set logic_block 1 m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 0 t:RAMB18E1
 
@@ -84,7 +84,7 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
 setattr -set ram_style "block" m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
 
@@ -92,6 +92,6 @@ design -reset
 read_verilog ../common/blockram.v
 hierarchy -top sync_ram_sdp -chparam ADDRESS_WIDTH 8 -chparam DATA_WIDTH 1
 setattr -set ram_block 1 m:memory
-synth_xilinx -top sync_ram_sdp
+synth_xilinx -top sync_ram_sdp -noiopad
 cd sync_ram_sdp
 select -assert-count 1 t:RAMB18E1
diff --git a/tests/arch/xilinx/bug1460.ys b/tests/arch/xilinx/bug1460.ys
index 2018071cc..09935ccd8 100644
--- a/tests/arch/xilinx/bug1460.ys
+++ b/tests/arch/xilinx/bug1460.ys
@@ -28,7 +28,7 @@ module register_file(
 endmodule
 EOT
 
-synth_xilinx
+synth_xilinx -noiopad
 cd register_file
 select -assert-count 32 t:RAM32M
 select -assert-none t:* t:BUFG %d t:RAM32M %d
diff --git a/tests/arch/xilinx/bug1598.ys b/tests/arch/xilinx/bug1598.ys
new file mode 100644
index 000000000..1175380b1
--- /dev/null
+++ b/tests/arch/xilinx/bug1598.ys
@@ -0,0 +1,16 @@
+read_verilog <<EOT
+module led_blink (
+        input clk,
+        output ledc
+    );
+ 
+    reg [6:0] led_counter = 0;
+    always @( posedge clk ) begin
+            led_counter <= led_counter + 1;
+    end
+    assign ledc = !led_counter[ 6:3 ];
+ 
+endmodule
+EOT
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -abc9
diff --git a/tests/arch/xilinx/counter.ys b/tests/arch/xilinx/counter.ys
index 604acdbfc..11c29922e 100644
--- a/tests/arch/xilinx/counter.ys
+++ b/tests/arch/xilinx/counter.ys
@@ -2,7 +2,7 @@ read_verilog ../common/counter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # 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/dffs.ys b/tests/arch/xilinx/dffs.ys
index 0bba4858f..dc764b033 100644
--- a/tests/arch/xilinx/dffs.ys
+++ b/tests/arch/xilinx/dffs.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top dff
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd dff # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
@@ -15,7 +15,7 @@ select -assert-none t:BUFG t:FDRE %% t:* %D
 design -load read
 hierarchy -top dffe
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd dffe # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
diff --git a/tests/arch/xilinx/dsp_cascade.ys b/tests/arch/xilinx/dsp_cascade.ys
new file mode 100644
index 000000000..ca6b619b9
--- /dev/null
+++ b/tests/arch/xilinx/dsp_cascade.ys
@@ -0,0 +1,89 @@
+design -reset
+read_verilog <<EOT
+module cascade(input clk, input [4:0] a, input [4:0] b, output reg [9:0] o);
+reg [4:0] ar1, ar2, ar3, br1, br2, br3;
+reg [9:0] m, n;
+always @(posedge clk) begin
+ar1 <= a;
+ar2 <= ar1;
+ar3 <= ar2;
+br1 <= b;
+br2 <= br1;
+br3 <= br2;
+m <= ar1 * br1;
+n <= ar2 * br2 + m;
+o <= ar3 * br3 + n;
+end
+endmodule
+EOT
+proc
+design -save read
+
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+design -load postopt
+cd cascade
+select -assert-count 3 t:DSP48E1
+select -assert-none t:DSP48E1 t:BUFG %% t:* %D
+# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
+# (i.e. Take all DSP48E1s, expand to find all wires connected
+#       to its PCOUT port, then remove all DSP48E1s from this
+#       selection, then expand again to find all cells where
+#       those wires are connected to the PCIN port, then remove
+#       all wires from this selection, and lastly intersect
+#       this selection with all DSP48E1 cells (to check that
+#       the connected cells are indeed DSPs)
+select -assert-count 2 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
+
+design -load read
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
+design -load postopt
+cd cascade
+select -assert-count 3 t:DSP48A1
+select -assert-count 5 t:FDRE # No cascade for A input
+select -assert-none t:DSP48A1 t:BUFG t:FDRE %% t:* %D
+# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
+#   (see above for explanation)
+select -assert-count 2 t:DSP48A1 %co:+[PCOUT] t:DSP48A1 %d %co:+[PCIN] w:* %d t:DSP48A1 %i
+
+design -reset
+read_verilog <<EOT
+module cascade(input clk, input [4:0] a, input [4:0] b, output reg [9:0] o);
+reg [4:0] ar1, ar2, ar3, br1, br2, br3;
+reg [9:0] m;
+always @(posedge clk) begin
+ar1 <= a;
+ar2 <= ar1;
+ar3 <= ar2;
+br1 <= b;
+br2 <= br1;
+br3 <= br2;
+m <= ar2 * br2;
+o <= ar3 * br3 + m;
+end
+endmodule
+EOT
+proc
+design -save read
+
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad
+design -load postopt
+cd cascade
+select -assert-count 2 t:DSP48E1
+select -assert-none t:DSP48E1 t:BUFG %% t:* %D
+# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
+#   (see above for explanation)
+select -assert-count 1 t:DSP48E1 %co:+[PCOUT] t:DSP48E1 %d %co:+[PCIN] w:* %d t:DSP48E1 %i
+
+design -load read
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad
+design -load postopt
+cd cascade
+select -assert-count 2 t:DSP48A1
+select -assert-count 10 t:FDRE # Cannot cascade because first 'm' DSP
+                               # uses both B0REG and B1REG, whereas 'o'
+                               # only requires 1
+select -assert-none t:DSP48A1 t:BUFG t:FDRE %% t:* %D
+# Very crude method of checking that DSP48E1.PCOUT -> DSP48E1.PCIN
+#   (see above for explanation)
+select -assert-count 1 t:DSP48A1 %co:+[PCOUT] t:DSP48A1 %d %co:+[PCIN] w:* %d t:DSP48A1 %i
+
diff --git a/tests/arch/xilinx/dsp_fastfir.ys b/tests/arch/xilinx/dsp_fastfir.ys
index 0067a822b..57fe49bde 100644
--- a/tests/arch/xilinx/dsp_fastfir.ys
+++ b/tests/arch/xilinx/dsp_fastfir.ys
@@ -63,7 +63,7 @@ module fastfir_dynamictaps(i_clk, i_reset, i_tap_wr, i_tap, i_ce, i_sample, o_re
 endmodule
 EOT
 
-synth_xilinx
+synth_xilinx -noiopad
 cd fastfir_dynamictaps
 select -assert-count 2 t:DSP48E1
 select -assert-none t:* t:DSP48E1 %d t:BUFG %d
diff --git a/tests/arch/xilinx/fsm.ys b/tests/arch/xilinx/fsm.ys
index f03400fe7..3235d5af3 100644
--- a/tests/arch/xilinx/fsm.ys
+++ b/tests/arch/xilinx/fsm.ys
@@ -3,7 +3,7 @@ hierarchy -top fsm
 proc
 flatten
 
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 miter -equiv -make_assert -flatten gold gate miter
 sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
 
diff --git a/tests/arch/xilinx/latches.ys b/tests/arch/xilinx/latches.ys
index c87a8e38b..e226c2ec8 100644
--- a/tests/arch/xilinx/latches.ys
+++ b/tests/arch/xilinx/latches.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top latchp
 proc
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd latchp # Constrain all select calls below inside the top module
 select -assert-count 1 t:LDCE
@@ -14,7 +14,7 @@ select -assert-none t:LDCE %% t:* %D
 design -load read
 hierarchy -top latchn
 proc
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd latchn # Constrain all select calls below inside the top module
 select -assert-count 1 t:LDCE
@@ -26,7 +26,7 @@ select -assert-none t:LDCE t:INV %% t:* %D
 design -load read
 hierarchy -top latchsr
 proc
-equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd latchsr # Constrain all select calls below inside the top module
 select -assert-count 1 t:LDCE
diff --git a/tests/arch/xilinx/logic.ys b/tests/arch/xilinx/logic.ys
index d5b5c1a37..61a9314cc 100644
--- a/tests/arch/xilinx/logic.ys
+++ b/tests/arch/xilinx/logic.ys
@@ -1,7 +1,7 @@
 read_verilog ../common/logic.v
 hierarchy -top top
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # 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/lutram.ys b/tests/arch/xilinx/lutram.ys
index 6c9d1eae1..3f127a77e 100644
--- a/tests/arch/xilinx/lutram.ys
+++ b/tests/arch/xilinx/lutram.ys
@@ -2,7 +2,7 @@
 #hierarchy -top lutram_1w1r -chparam A_WIDTH 4
 #proc
 #memory -nomap
-#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+#equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 #memory
 #opt -full
 #
@@ -22,7 +22,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 5
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -42,7 +42,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -62,7 +62,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w3r
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -82,7 +82,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w3r -chparam A_WIDTH 6
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -102,7 +102,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 5 -chparam D_WIDTH 6
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
@@ -122,7 +122,7 @@ read_verilog ../common/lutram.v
 hierarchy -top lutram_1w1r -chparam A_WIDTH 6 -chparam D_WIDTH 6
 proc
 memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 memory
 opt -full
 
diff --git a/tests/arch/xilinx/macc.sh b/tests/arch/xilinx/macc.sh
index 154a29848..58b97b646 100644
--- a/tests/arch/xilinx/macc.sh
+++ b/tests/arch/xilinx/macc.sh
@@ -1,3 +1,6 @@
 ../../../yosys -qp "synth_xilinx -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v
 iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v
 vvp -N ./test_macc
+../../../yosys -qp "synth_xilinx -family xc6s -top macc2; rename -top macc2_uut" -o macc_uut.v macc.v
+iverilog -o test_macc macc_tb.v macc_uut.v macc.v ../../../techlibs/xilinx/cells_sim.v
+vvp -N ./test_macc
diff --git a/tests/arch/xilinx/macc.ys b/tests/arch/xilinx/macc.ys
index 11e959976..bf2b36320 100644
--- a/tests/arch/xilinx/macc.ys
+++ b/tests/arch/xilinx/macc.ys
@@ -3,8 +3,8 @@ design -save read
 
 hierarchy -top macc
 proc
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
@@ -17,8 +17,8 @@ select -assert-none t:BUFG t:FDRE t:DSP48E1 %% t:* %D
 design -load read
 hierarchy -top macc2
 proc
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx ### TODO
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
+#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
+equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
 sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
diff --git a/tests/arch/xilinx/mul.ys b/tests/arch/xilinx/mul.ys
index d76814966..490846ff1 100644
--- a/tests/arch/xilinx/mul.ys
+++ b/tests/arch/xilinx/mul.ys
@@ -1,9 +1,21 @@
 read_verilog ../common/mul.v
 hierarchy -top top
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # 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:DSP48E1
 select -assert-none t:DSP48E1 %% t:* %D
+
+design -reset
+
+read_verilog ../common/mul.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # 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:DSP48A1
+select -assert-none t:DSP48A1 %% t:* %D
diff --git a/tests/arch/xilinx/mul_unsigned.ys b/tests/arch/xilinx/mul_unsigned.ys
index 62495b90c..980263cbd 100644
--- a/tests/arch/xilinx/mul_unsigned.ys
+++ b/tests/arch/xilinx/mul_unsigned.ys
@@ -2,10 +2,24 @@ read_verilog mul_unsigned.v
 hierarchy -top mul_unsigned
 proc
 
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mul_unsigned # Constrain all select calls below inside the top module
 select -assert-count 1 t:BUFG
 select -assert-count 1 t:DSP48E1
 select -assert-count 30 t:FDRE
 select -assert-none t:DSP48E1 t:FDRE t:BUFG %% t:* %D
+
+design -reset
+
+read_verilog mul_unsigned.v
+hierarchy -top mul_unsigned
+proc
+
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -family xc6s -noiopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd mul_unsigned # Constrain all select calls below inside the top module
+select -assert-count 1 t:BUFG
+select -assert-count 1 t:DSP48A1
+select -assert-count 30 t:FDRE
+select -assert-none t:DSP48A1 t:FDRE t:BUFG %% t:* %D
diff --git a/tests/arch/xilinx/mux.ys b/tests/arch/xilinx/mux.ys
index 388272449..99817738d 100644
--- a/tests/arch/xilinx/mux.ys
+++ b/tests/arch/xilinx/mux.ys
@@ -3,7 +3,7 @@ design -save read
 
 hierarchy -top mux2
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux2 # Constrain all select calls below inside the top module
 select -assert-count 1 t:LUT3
@@ -14,7 +14,7 @@ select -assert-none t:LUT3 %% t:* %D
 design -load read
 hierarchy -top mux4
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux4 # Constrain all select calls below inside the top module
 select -assert-count 1 t:LUT6
@@ -25,7 +25,7 @@ select -assert-none t:LUT6 %% t:* %D
 design -load read
 hierarchy -top mux8
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux8 # Constrain all select calls below inside the top module
 select -assert-count 1 t:LUT3
@@ -37,7 +37,7 @@ select -assert-none t:LUT3 t:LUT6 %% t:* %D
 design -load read
 hierarchy -top mux16
 proc
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
 design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
 cd mux16 # Constrain all select calls below inside the top module
 select -assert-min 5 t:LUT6
diff --git a/tests/arch/xilinx/shifter.ys b/tests/arch/xilinx/shifter.ys
index 455437f18..3652319a0 100644
--- a/tests/arch/xilinx/shifter.ys
+++ b/tests/arch/xilinx/shifter.ys
@@ -2,7 +2,7 @@ read_verilog ../common/shifter.v
 hierarchy -top top
 proc
 flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
+equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # 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/tribuf.ys b/tests/arch/xilinx/tribuf.ys
index 4697703ca..eaccab126 100644
--- a/tests/arch/xilinx/tribuf.ys
+++ b/tests/arch/xilinx/tribuf.ys
@@ -7,6 +7,7 @@ synth
 equiv_opt -assert -map +/xilinx/cells_sim.v -map +/simcells.v synth_xilinx # 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
-# TODO :: Tristate logic not yet supported; see https://github.com/YosysHQ/yosys/issues/1225
-select -assert-count 1 t:$_TBUF_
-select -assert-none t:$_TBUF_ %% t:* %D
+select -assert-count 2 t:IBUF
+select -assert-count 1 t:INV
+select -assert-count 1 t:OBUFT
+select -assert-none t:IBUF t:INV t:OBUFT %% t:* %D