From 6331fa5b022b9e16f9392d9604a545f86dc13385 Mon Sep 17 00:00:00 2001
From: SergeyDegtyar <sndegtyar@gmail.com>
Date: Tue, 10 Sep 2019 08:11:56 +0300
Subject: [PATCH] Remove xilinx_ug901 tests (will be moved to yosys-tests)

---
 Makefile                                      |   1 -
 tests/xilinx_ug901/asym_ram_sdp_read_wider.v  |  74 -----------
 tests/xilinx_ug901/asym_ram_sdp_read_wider.ys |  22 ----
 tests/xilinx_ug901/asym_ram_sdp_write_wider.v |  75 -----------
 .../xilinx_ug901/asym_ram_sdp_write_wider.ys  |  31 -----
 tests/xilinx_ug901/asym_ram_tdp_read_first.v  |  85 ------------
 tests/xilinx_ug901/asym_ram_tdp_read_first.ys |  21 ---
 tests/xilinx_ug901/asym_ram_tdp_write_first.v |  92 -------------
 .../xilinx_ug901/asym_ram_tdp_write_first.ys  |  29 -----
 tests/xilinx_ug901/black_box_1.v              |  19 ---
 tests/xilinx_ug901/black_box_1.ys             |  15 ---
 tests/xilinx_ug901/bytewrite_ram_1b.v         |  42 ------
 tests/xilinx_ug901/bytewrite_ram_1b.ys        |  22 ----
 tests/xilinx_ug901/bytewrite_tdp_ram_nc.v     |  78 -----------
 tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys    |  22 ----
 .../bytewrite_tdp_ram_readfirst2.v            |  71 ----------
 .../bytewrite_tdp_ram_readfirst2.ys           |  21 ---
 tests/xilinx_ug901/bytewrite_tdp_ram_rf.v     |  61 ---------
 tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys    |  21 ---
 tests/xilinx_ug901/bytewrite_tdp_ram_wf.v     |  68 ----------
 tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys    |  23 ----
 tests/xilinx_ug901/cmacc.v                    | 122 ------------------
 tests/xilinx_ug901/cmacc.ys                   |  25 ----
 tests/xilinx_ug901/cmult.v                    |  71 ----------
 tests/xilinx_ug901/cmult.ys                   |  31 -----
 .../xilinx_ug901/dynamic_shift_registers_1.v  |  21 ---
 .../xilinx_ug901/dynamic_shift_registers_1.ys |  15 ---
 tests/xilinx_ug901/dynpreaddmultadd.v         |  47 -------
 tests/xilinx_ug901/dynpreaddmultadd.ys        |  31 -----
 tests/xilinx_ug901/fsm_1.v                    |  42 ------
 tests/xilinx_ug901/fsm_1.ys                   |  16 ---
 tests/xilinx_ug901/latches.v                  |  17 ---
 tests/xilinx_ug901/latches.ys                 |  10 --
 tests/xilinx_ug901/macc.v                     |  47 -------
 tests/xilinx_ug901/macc.ys                    |  23 ----
 tests/xilinx_ug901/mult_unsigned.v            |  33 -----
 tests/xilinx_ug901/mult_unsigned.ys           |  29 -----
 tests/xilinx_ug901/presubmult.v               |  43 ------
 tests/xilinx_ug901/presubmult.ys              |  23 ----
 .../xilinx_ug901/ram_simple_dual_one_clock.v  |  25 ----
 .../xilinx_ug901/ram_simple_dual_one_clock.ys |  20 ---
 .../xilinx_ug901/ram_simple_dual_two_clocks.v |  30 -----
 .../ram_simple_dual_two_clocks.ys             |  20 ---
 tests/xilinx_ug901/rams_dist.v                |  24 ----
 tests/xilinx_ug901/rams_dist.ys               |  21 ---
 tests/xilinx_ug901/rams_init_file.data        |  64 ---------
 tests/xilinx_ug901/rams_init_file.v           |  24 ----
 tests/xilinx_ug901/rams_init_file.ys          |  22 ----
 tests/xilinx_ug901/rams_pipeline.v            |  42 ------
 tests/xilinx_ug901/rams_pipeline.ys           |  22 ----
 tests/xilinx_ug901/rams_sp_nc.v               |  26 ----
 tests/xilinx_ug901/rams_sp_nc.ys              |  22 ----
 tests/xilinx_ug901/rams_sp_rf.v               |  26 ----
 tests/xilinx_ug901/rams_sp_rf.ys              |  22 ----
 tests/xilinx_ug901/rams_sp_rf_rst.v           |  29 -----
 tests/xilinx_ug901/rams_sp_rf_rst.ys          |  28 ----
 tests/xilinx_ug901/rams_sp_rom.v              |  46 -------
 tests/xilinx_ug901/rams_sp_rom.ys             |  22 ----
 tests/xilinx_ug901/rams_sp_rom_1.v            |  53 --------
 tests/xilinx_ug901/rams_sp_rom_1.ys           |  22 ----
 tests/xilinx_ug901/rams_sp_wf.v               |  26 ----
 tests/xilinx_ug901/rams_sp_wf.ys              |  26 ----
 tests/xilinx_ug901/rams_tdp_rf_rf.v           |  33 -----
 tests/xilinx_ug901/rams_tdp_rf_rf.ys          |  21 ---
 tests/xilinx_ug901/registers_1.v              |  25 ----
 tests/xilinx_ug901/registers_1.ys             |  12 --
 tests/xilinx_ug901/run-test.sh                |  20 ---
 tests/xilinx_ug901/sfir_shifter.v             |  19 ---
 tests/xilinx_ug901/sfir_shifter.ys            |  16 ---
 tests/xilinx_ug901/shift_registers_0.v        |  22 ----
 tests/xilinx_ug901/shift_registers_0.ys       |  14 --
 tests/xilinx_ug901/shift_registers_1.v        |  24 ----
 tests/xilinx_ug901/shift_registers_1.ys       |  14 --
 tests/xilinx_ug901/squarediffmacc.v           |  52 --------
 tests/xilinx_ug901/squarediffmacc.ys          |  23 ----
 tests/xilinx_ug901/squarediffmult.v           |  42 ------
 tests/xilinx_ug901/squarediffmult.ys          |  30 -----
 tests/xilinx_ug901/top_mux.v                  |  18 ---
 tests/xilinx_ug901/top_mux.ys                 |  13 --
 tests/xilinx_ug901/tristates_1.v              |  17 ---
 tests/xilinx_ug901/tristates_1.ys             |  13 --
 tests/xilinx_ug901/tristates_2.v              |  10 --
 tests/xilinx_ug901/tristates_2.ys             |  13 --
 .../xilinx_ultraram_single_port_no_change.v   |  78 -----------
 .../xilinx_ultraram_single_port_no_change.ys  |  25 ----
 .../xilinx_ultraram_single_port_read_first.v  |  78 -----------
 .../xilinx_ultraram_single_port_read_first.ys |  24 ----
 .../xilinx_ultraram_single_port_write_first.v |  82 ------------
 ...xilinx_ultraram_single_port_write_first.ys |  24 ----
 89 files changed, 2963 deletions(-)
 delete mode 100644 tests/xilinx_ug901/asym_ram_sdp_read_wider.v
 delete mode 100644 tests/xilinx_ug901/asym_ram_sdp_read_wider.ys
 delete mode 100644 tests/xilinx_ug901/asym_ram_sdp_write_wider.v
 delete mode 100644 tests/xilinx_ug901/asym_ram_sdp_write_wider.ys
 delete mode 100644 tests/xilinx_ug901/asym_ram_tdp_read_first.v
 delete mode 100644 tests/xilinx_ug901/asym_ram_tdp_read_first.ys
 delete mode 100644 tests/xilinx_ug901/asym_ram_tdp_write_first.v
 delete mode 100644 tests/xilinx_ug901/asym_ram_tdp_write_first.ys
 delete mode 100644 tests/xilinx_ug901/black_box_1.v
 delete mode 100644 tests/xilinx_ug901/black_box_1.ys
 delete mode 100644 tests/xilinx_ug901/bytewrite_ram_1b.v
 delete mode 100644 tests/xilinx_ug901/bytewrite_ram_1b.ys
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_nc.v
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_rf.v
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_wf.v
 delete mode 100644 tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys
 delete mode 100644 tests/xilinx_ug901/cmacc.v
 delete mode 100644 tests/xilinx_ug901/cmacc.ys
 delete mode 100644 tests/xilinx_ug901/cmult.v
 delete mode 100644 tests/xilinx_ug901/cmult.ys
 delete mode 100644 tests/xilinx_ug901/dynamic_shift_registers_1.v
 delete mode 100644 tests/xilinx_ug901/dynamic_shift_registers_1.ys
 delete mode 100644 tests/xilinx_ug901/dynpreaddmultadd.v
 delete mode 100644 tests/xilinx_ug901/dynpreaddmultadd.ys
 delete mode 100644 tests/xilinx_ug901/fsm_1.v
 delete mode 100644 tests/xilinx_ug901/fsm_1.ys
 delete mode 100644 tests/xilinx_ug901/latches.v
 delete mode 100644 tests/xilinx_ug901/latches.ys
 delete mode 100644 tests/xilinx_ug901/macc.v
 delete mode 100644 tests/xilinx_ug901/macc.ys
 delete mode 100644 tests/xilinx_ug901/mult_unsigned.v
 delete mode 100644 tests/xilinx_ug901/mult_unsigned.ys
 delete mode 100644 tests/xilinx_ug901/presubmult.v
 delete mode 100644 tests/xilinx_ug901/presubmult.ys
 delete mode 100644 tests/xilinx_ug901/ram_simple_dual_one_clock.v
 delete mode 100644 tests/xilinx_ug901/ram_simple_dual_one_clock.ys
 delete mode 100644 tests/xilinx_ug901/ram_simple_dual_two_clocks.v
 delete mode 100644 tests/xilinx_ug901/ram_simple_dual_two_clocks.ys
 delete mode 100644 tests/xilinx_ug901/rams_dist.v
 delete mode 100644 tests/xilinx_ug901/rams_dist.ys
 delete mode 100644 tests/xilinx_ug901/rams_init_file.data
 delete mode 100644 tests/xilinx_ug901/rams_init_file.v
 delete mode 100644 tests/xilinx_ug901/rams_init_file.ys
 delete mode 100644 tests/xilinx_ug901/rams_pipeline.v
 delete mode 100644 tests/xilinx_ug901/rams_pipeline.ys
 delete mode 100644 tests/xilinx_ug901/rams_sp_nc.v
 delete mode 100644 tests/xilinx_ug901/rams_sp_nc.ys
 delete mode 100644 tests/xilinx_ug901/rams_sp_rf.v
 delete mode 100644 tests/xilinx_ug901/rams_sp_rf.ys
 delete mode 100644 tests/xilinx_ug901/rams_sp_rf_rst.v
 delete mode 100644 tests/xilinx_ug901/rams_sp_rf_rst.ys
 delete mode 100644 tests/xilinx_ug901/rams_sp_rom.v
 delete mode 100644 tests/xilinx_ug901/rams_sp_rom.ys
 delete mode 100644 tests/xilinx_ug901/rams_sp_rom_1.v
 delete mode 100644 tests/xilinx_ug901/rams_sp_rom_1.ys
 delete mode 100644 tests/xilinx_ug901/rams_sp_wf.v
 delete mode 100644 tests/xilinx_ug901/rams_sp_wf.ys
 delete mode 100644 tests/xilinx_ug901/rams_tdp_rf_rf.v
 delete mode 100644 tests/xilinx_ug901/rams_tdp_rf_rf.ys
 delete mode 100644 tests/xilinx_ug901/registers_1.v
 delete mode 100644 tests/xilinx_ug901/registers_1.ys
 delete mode 100755 tests/xilinx_ug901/run-test.sh
 delete mode 100644 tests/xilinx_ug901/sfir_shifter.v
 delete mode 100644 tests/xilinx_ug901/sfir_shifter.ys
 delete mode 100644 tests/xilinx_ug901/shift_registers_0.v
 delete mode 100644 tests/xilinx_ug901/shift_registers_0.ys
 delete mode 100644 tests/xilinx_ug901/shift_registers_1.v
 delete mode 100644 tests/xilinx_ug901/shift_registers_1.ys
 delete mode 100644 tests/xilinx_ug901/squarediffmacc.v
 delete mode 100644 tests/xilinx_ug901/squarediffmacc.ys
 delete mode 100644 tests/xilinx_ug901/squarediffmult.v
 delete mode 100644 tests/xilinx_ug901/squarediffmult.ys
 delete mode 100644 tests/xilinx_ug901/top_mux.v
 delete mode 100644 tests/xilinx_ug901/top_mux.ys
 delete mode 100644 tests/xilinx_ug901/tristates_1.v
 delete mode 100644 tests/xilinx_ug901/tristates_1.ys
 delete mode 100644 tests/xilinx_ug901/tristates_2.v
 delete mode 100644 tests/xilinx_ug901/tristates_2.ys
 delete mode 100644 tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v
 delete mode 100644 tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys
 delete mode 100644 tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v
 delete mode 100644 tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys
 delete mode 100644 tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v
 delete mode 100644 tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys

diff --git a/Makefile b/Makefile
index 82af448da..6f5184596 100644
--- a/Makefile
+++ b/Makefile
@@ -716,7 +716,6 @@ test: $(TARGETS) $(EXTRA_TARGETS)
 	+cd tests/ice40 && bash run-test.sh $(SEEDOPT)
 	+cd tests/rpc && bash run-test.sh
 	+cd tests/xilinx && bash run-test.sh $(SEEDOPT)
-	+cd tests/xilinx_ug901 && bash run-test.sh $(SEEDOPT)
 	@echo ""
 	@echo "  Passed \"make test\"."
 	@echo ""
diff --git a/tests/xilinx_ug901/asym_ram_sdp_read_wider.v b/tests/xilinx_ug901/asym_ram_sdp_read_wider.v
deleted file mode 100644
index 0716dffdc..000000000
--- a/tests/xilinx_ug901/asym_ram_sdp_read_wider.v
+++ /dev/null
@@ -1,74 +0,0 @@
-// Asymmetric port RAM
-// Read Wider than Write. Read Statement in loop
-//asym_ram_sdp_read_wider.v
-
-module asym_ram_sdp_read_wider (clkA, clkB, enaA, weA, enaB, addrA, addrB, diA, doB);
-parameter WIDTHA = 4;
-parameter SIZEA = 1024;
-parameter ADDRWIDTHA = 10;
-
-parameter WIDTHB = 16;
-parameter SIZEB = 256;
-parameter ADDRWIDTHB = 8;
-input clkA;
-input clkB;
-input weA;
-input enaA, enaB;
-input [ADDRWIDTHA-1:0] addrA;
-input [ADDRWIDTHB-1:0] addrB;
-input [WIDTHA-1:0] diA;
-output [WIDTHB-1:0] doB;
-`define max(a,b) {(a) > (b) ? (a) : (b)}
-`define min(a,b) {(a) < (b) ? (a) : (b)}
-
-function integer log2;
-input integer value;
-reg [31:0] shifted;
-integer res;
-begin
- if (value < 2)
-  log2 = value;
- else
- begin
-  shifted = value-1;
-  for (res=0; shifted>0; res=res+1)
-   shifted = shifted>>1;
-  log2 = res;
- end
-end
-endfunction
-
-localparam maxSIZE = `max(SIZEA, SIZEB);
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);
-localparam minWIDTH = `min(WIDTHA, WIDTHB);
-
-localparam RATIO = maxWIDTH / minWIDTH;
-localparam log2RATIO = log2(RATIO);
-
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
-reg [WIDTHB-1:0] readB;
-
-always @(posedge clkA)
-begin
- if (enaA) begin 
-  if (weA)
-   RAM[addrA] <= diA;
- end  
-end
-
-
-always @(posedge clkB)
-begin : ramread
- integer i;
- reg [log2RATIO-1:0] lsbaddr;
- if (enaB) begin
-  for (i = 0; i < RATIO; i = i+1) begin 
-   lsbaddr = i;
-   readB[(i+1)*minWIDTH-1 -: minWIDTH] <= RAM[{addrB, lsbaddr}];
-  end
- end
-end
-assign doB = readB;
-
-endmodule
-
diff --git a/tests/xilinx_ug901/asym_ram_sdp_read_wider.ys b/tests/xilinx_ug901/asym_ram_sdp_read_wider.ys
deleted file mode 100644
index c63157cdf..000000000
--- a/tests/xilinx_ug901/asym_ram_sdp_read_wider.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog asym_ram_sdp_read_wider.v
-hierarchy -top asym_ram_sdp_read_wider
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd asym_ram_sdp_read_wider
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 4 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
diff --git a/tests/xilinx_ug901/asym_ram_sdp_write_wider.v b/tests/xilinx_ug901/asym_ram_sdp_write_wider.v
deleted file mode 100644
index 22d12d2ce..000000000
--- a/tests/xilinx_ug901/asym_ram_sdp_write_wider.v
+++ /dev/null
@@ -1,75 +0,0 @@
-// Asymmetric port RAM
-// Write wider than Read. Write Statement in a loop.
-// asym_ram_sdp_write_wider.v
-
-module asym_ram_sdp_write_wider (clkA, clkB, weA, enaA, enaB, addrA, addrB, diA, doB);
-parameter WIDTHB = 4;
-//Default parameters were changed because of slow test
-//parameter SIZEB = 1024;
-//parameter ADDRWIDTHB = 10;
-parameter SIZEB = 256;
-parameter ADDRWIDTHB = 8;
-
-//parameter WIDTHA = 16;
-parameter WIDTHA = 8;
-parameter SIZEA = 256;
-parameter ADDRWIDTHA = 8;
-input clkA;
-input clkB;
-input weA;
-input enaA, enaB;
-input [ADDRWIDTHA-1:0] addrA;
-input [ADDRWIDTHB-1:0] addrB;
-input [WIDTHA-1:0] diA;
-output [WIDTHB-1:0] doB;
-`define max(a,b) {(a) > (b) ? (a) : (b)}
-`define min(a,b) {(a) < (b) ? (a) : (b)}
-
-function integer log2;
-input integer value;
-reg [31:0] shifted;
-integer res;
-begin
- if (value < 2)
-  log2 = value;
- else
- begin
-  shifted = value-1;
-  for (res=0; shifted>0; res=res+1)
-   shifted = shifted>>1;
-  log2 = res;
- end
-end
-endfunction
-
-localparam maxSIZE = `max(SIZEA, SIZEB);
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);
-localparam minWIDTH = `min(WIDTHA, WIDTHB);
-
-localparam RATIO = maxWIDTH / minWIDTH;
-localparam log2RATIO = log2(RATIO);
-
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
-reg [WIDTHB-1:0] readB;
-
-always @(posedge clkB) begin
- if (enaB) begin
-  readB <= RAM[addrB];
- end
-end
-assign doB = readB;
-
-always @(posedge clkA)
-begin : ramwrite
- integer i;
- reg [log2RATIO-1:0] lsbaddr;
- for (i=0; i< RATIO; i= i+ 1) begin : write1
-  lsbaddr = i;
-  if (enaA) begin
-   if (weA)
-    RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH];
-  end
- end
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/asym_ram_sdp_write_wider.ys b/tests/xilinx_ug901/asym_ram_sdp_write_wider.ys
deleted file mode 100644
index 229d98df6..000000000
--- a/tests/xilinx_ug901/asym_ram_sdp_write_wider.ys
+++ /dev/null
@@ -1,31 +0,0 @@
-read_verilog asym_ram_sdp_write_wider.v
-hierarchy -top asym_ram_sdp_write_wider
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd asym_ram_sdp_write_wider
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 1028 t:FDRE
-select -assert-count 170 t:LUT2
-select -assert-count 6 t:LUT3
-select -assert-count 518 t:LUT4
-select -assert-count 10 t:LUT5
-select -assert-count 484 t:LUT6
-select -assert-count 157 t:MUXF7
-select -assert-count 3 t:MUXF8
-
-#RRAM128X1D will be synthesized in case when the parameter WIDTHA=4
-#select -assert-count 8 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
diff --git a/tests/xilinx_ug901/asym_ram_tdp_read_first.v b/tests/xilinx_ug901/asym_ram_tdp_read_first.v
deleted file mode 100644
index 2b807a382..000000000
--- a/tests/xilinx_ug901/asym_ram_tdp_read_first.v
+++ /dev/null
@@ -1,85 +0,0 @@
-// Asymetric RAM - TDP  
-// READ_FIRST MODE.
-// asym_ram_tdp_read_first.v
-
-
-module asym_ram_tdp_read_first (clkA, clkB, enaA, weA, enaB, weB, addrA, addrB, diA, doA, diB, doB);
-parameter WIDTHB = 4;
-parameter SIZEB = 1024;
-parameter ADDRWIDTHB = 10;
-parameter WIDTHA = 16;
-parameter SIZEA = 256;
-parameter ADDRWIDTHA = 8;
-input clkA;
-input clkB;
-input weA, weB;
-input enaA, enaB;
-
-input [ADDRWIDTHA-1:0] addrA;
-input [ADDRWIDTHB-1:0] addrB;
-input [WIDTHA-1:0] diA;
-input [WIDTHB-1:0] diB;
-
-output [WIDTHA-1:0] doA;
-output [WIDTHB-1:0] doB;
-
-`define max(a,b) {(a) > (b) ? (a) : (b)}
-`define min(a,b) {(a) < (b) ? (a) : (b)}
-
-function integer log2;
-input integer value;
-reg [31:0] shifted;
-integer res;
-begin
- if (value < 2)
-  log2 = value;
- else
- begin
-  shifted = value-1;
-  for (res=0; shifted>0; res=res+1)
-   shifted = shifted>>1;
-  log2 = res;
- end
-end
-endfunction
-
-localparam maxSIZE = `max(SIZEA, SIZEB);
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);
-localparam minWIDTH = `min(WIDTHA, WIDTHB);
-
-localparam RATIO = maxWIDTH / minWIDTH;
-localparam log2RATIO = log2(RATIO);
-
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
-reg [WIDTHA-1:0] readA;
-reg [WIDTHB-1:0] readB;
-
-always @(posedge clkB)
-begin
- if (enaB) begin
-  readB <= RAM[addrB] ;
-  if (weB)
-   RAM[addrB] <= diB;
- end  
-end
-
-
-always @(posedge clkA)
-begin : portA
- integer i;
- reg [log2RATIO-1:0] lsbaddr ;
-  for (i=0; i< RATIO; i= i+ 1) begin 
-   lsbaddr = i;
-  if (enaA) begin
-   readA[(i+1)*minWIDTH -1 -: minWIDTH] <= RAM[{addrA, lsbaddr}];
-
-   if (weA)
-    RAM[{addrA, lsbaddr}] <= diA[(i+1)*minWIDTH-1 -: minWIDTH];
-  end
- end
-end
-
-assign doA = readA;
-assign doB = readB;
-
-endmodule
diff --git a/tests/xilinx_ug901/asym_ram_tdp_read_first.ys b/tests/xilinx_ug901/asym_ram_tdp_read_first.ys
deleted file mode 100644
index 5f96b800c..000000000
--- a/tests/xilinx_ug901/asym_ram_tdp_read_first.ys
+++ /dev/null
@@ -1,21 +0,0 @@
-read_verilog asym_ram_tdp_read_first.v
-hierarchy -top asym_ram_tdp_read_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd asym_ram_tdp_read_first
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:$mem
-select -assert-count 2 t:LUT2
-
-select -assert-none t:$mem t:LUT2 %% t:* %D
diff --git a/tests/xilinx_ug901/asym_ram_tdp_write_first.v b/tests/xilinx_ug901/asym_ram_tdp_write_first.v
deleted file mode 100644
index 90187ea26..000000000
--- a/tests/xilinx_ug901/asym_ram_tdp_write_first.v
+++ /dev/null
@@ -1,92 +0,0 @@
-// Asymmetric port RAM - TDP
-// WRITE_FIRST MODE.
-// asym_ram_tdp_write_first.v
-
-
-module asym_ram_tdp_write_first (clkA, clkB, enaA, weA, enaB, weB, addrA, addrB, diA, doA, diB, doB);
-parameter WIDTHB = 4;
-//Default parameters were changed because of slow test
-//parameter SIZEB = 1024;
-//parameter ADDRWIDTHB = 10;
-parameter SIZEB = 32;
-parameter ADDRWIDTHB = 8;
-
-//parameter WIDTHA = 16;
-parameter WIDTHA = 4;
-//parameter SIZEA = 256;
-parameter SIZEA = 32;
-parameter ADDRWIDTHA = 8;
-input clkA;
-input clkB;
-input weA, weB;
-input enaA, enaB;
-
-input [ADDRWIDTHA-1:0] addrA;
-input [ADDRWIDTHB-1:0] addrB;
-input [WIDTHA-1:0] diA;
-input [WIDTHB-1:0] diB;
-
-output [WIDTHA-1:0] doA;
-output [WIDTHB-1:0] doB;
-
-`define max(a,b) {(a) > (b) ? (a) : (b)}
-`define min(a,b) {(a) < (b) ? (a) : (b)}
-
-function integer log2;
-input integer value;
-reg [31:0] shifted;
-integer res;
-begin
- if (value < 2)
-  log2 = value;
- else
- begin
-  shifted = value-1;
-  for (res=0; shifted>0; res=res+1)
-   shifted = shifted>>1;
-  log2 = res;
- end
-end
-endfunction
-
-localparam maxSIZE = `max(SIZEA, SIZEB);
-localparam maxWIDTH = `max(WIDTHA, WIDTHB);
-localparam minWIDTH = `min(WIDTHA, WIDTHB);
-
-localparam RATIO = maxWIDTH / minWIDTH;
-localparam log2RATIO = log2(RATIO);
-
-reg [minWIDTH-1:0] RAM [0:maxSIZE-1];
-reg [WIDTHA-1:0] readA;
-reg [WIDTHB-1:0] readB;
-
-always @(posedge clkB)
-begin
- if (enaB) begin
-  if (weB)
-   RAM[addrB] = diB;
-  readB = RAM[addrB] ;
- end
-end
-
-
-always @(posedge clkA)
-begin : portA
- integer i;
- reg [log2RATIO-1:0] lsbaddr ;
-  for (i=0; i< RATIO; i= i+ 1) begin
-   lsbaddr = i;
-   if (enaA) begin
-
-   if (weA)
-    RAM[{addrA, lsbaddr}] = diA[(i+1)*minWIDTH-1 -: minWIDTH];
-
-   readA[(i+1)*minWIDTH -1 -: minWIDTH] = RAM[{addrA, lsbaddr}];
-  end
- end
-end
-
-assign doA = readA;
-assign doB = readB;
-
-endmodule
diff --git a/tests/xilinx_ug901/asym_ram_tdp_write_first.ys b/tests/xilinx_ug901/asym_ram_tdp_write_first.ys
deleted file mode 100644
index bbe3cc849..000000000
--- a/tests/xilinx_ug901/asym_ram_tdp_write_first.ys
+++ /dev/null
@@ -1,29 +0,0 @@
-read_verilog asym_ram_tdp_write_first.v
-hierarchy -top asym_ram_tdp_write_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd asym_ram_tdp_write_first
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 200 t:FDRE
-select -assert-count 10 t:LUT2
-select -assert-count 44 t:LUT3
-select -assert-count 81 t:LUT4
-select -assert-count 104 t:LUT5
-select -assert-count 560 t:LUT6
-select -assert-count 261 t:MUXF7
-select -assert-count 127 t:MUXF8
-
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXF7 t:MUXF8 %% t:* %D
diff --git a/tests/xilinx_ug901/black_box_1.v b/tests/xilinx_ug901/black_box_1.v
deleted file mode 100644
index 40caa1b10..000000000
--- a/tests/xilinx_ug901/black_box_1.v
+++ /dev/null
@@ -1,19 +0,0 @@
-// Black Box
-// black_box_1.v
-// 
-(* black_box *) module black_box1 (in1, in2, dout);
-input in1, in2;
-output dout;
-endmodule
-
-module black_box_1 (DI_1, DI_2, DOUT);
-input DI_1, DI_2;
-output DOUT;
-
-black_box1 U1 (
-                .in1(DI_1),
-                .in2(DI_2),
-                .dout(DOUT)
-              );
-
-endmodule
diff --git a/tests/xilinx_ug901/black_box_1.ys b/tests/xilinx_ug901/black_box_1.ys
deleted file mode 100644
index acf0b5761..000000000
--- a/tests/xilinx_ug901/black_box_1.ys
+++ /dev/null
@@ -1,15 +0,0 @@
-read_verilog black_box_1.v
-hierarchy -top black_box_1
-proc
-tribuf
-flatten
-synth
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd black_box_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 black box.
-#stat
-#select -assert-count 0 t:LUT1
-#select -assert-count 1 t:$_TBUF_
-#select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D
diff --git a/tests/xilinx_ug901/bytewrite_ram_1b.v b/tests/xilinx_ug901/bytewrite_ram_1b.v
deleted file mode 100644
index 46d86c297..000000000
--- a/tests/xilinx_ug901/bytewrite_ram_1b.v
+++ /dev/null
@@ -1,42 +0,0 @@
-// Single-Port BRAM with Byte-wide Write Enable
-// Read-First mode
-// Single-process description
-// Compact description of the write with a generate-for 
-//   statement
-// Column width and number of columns easily configurable
-//
-// bytewrite_ram_1b.v
-//
-
-module bytewrite_ram_1b (clk, we, addr, di, do);
-
-parameter SIZE = 1024; 
-parameter ADDR_WIDTH = 10; 
-parameter COL_WIDTH = 8; 
-parameter NB_COL = 4;
-
-input clk;
-input [NB_COL-1:0] we;
-input [ADDR_WIDTH-1:0] addr;
-input [NB_COL*COL_WIDTH-1:0] di;
-output reg [NB_COL*COL_WIDTH-1:0] do;
-
-reg [NB_COL*COL_WIDTH-1:0] RAM [SIZE-1:0];
-
-always @(posedge clk)
-begin
-    do <= RAM[addr];
-end
-
-generate genvar i;
-for (i = 0; i < NB_COL; i = i+1)
-begin
-always @(posedge clk)
-begin
-    if (we[i])
-        RAM[addr][(i+1)*COL_WIDTH-1:i*COL_WIDTH] <= di[(i+1)*COL_WIDTH-1:i*COL_WIDTH];
-    end 
-end
-endgenerate
-
-endmodule
diff --git a/tests/xilinx_ug901/bytewrite_ram_1b.ys b/tests/xilinx_ug901/bytewrite_ram_1b.ys
deleted file mode 100644
index 4f0967801..000000000
--- a/tests/xilinx_ug901/bytewrite_ram_1b.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog bytewrite_ram_1b.v
-hierarchy -top bytewrite_ram_1b
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd bytewrite_ram_1b
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:BUFG
-select -assert-count 32 t:LUT2
-select -assert-count 8 t:RAMB36E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB36E1 %% t:* %D
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.v b/tests/xilinx_ug901/bytewrite_tdp_ram_nc.v
deleted file mode 100644
index 1093b0838..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.v
+++ /dev/null
@@ -1,78 +0,0 @@
-//
-// True-Dual-Port BRAM with Byte-wide Write Enable
-//      No-Change mode
-//
-// bytewrite_tdp_ram_nc.v
-//
-// ByteWide Write Enable, - NO_CHANGE mode template - Vivado recomended
-module bytewrite_tdp_ram_nc
-  #(
-    //---------------------------------------------------------------
-    parameter   NUM_COL                 =   4,
-    parameter   COL_WIDTH               =   8,
-    parameter   ADDR_WIDTH              =  10, // Addr  Width in bits : 2**ADDR_WIDTH = RAM Depth
-    parameter   DATA_WIDTH              =  NUM_COL*COL_WIDTH  // Data  Width in bits
-    //---------------------------------------------------------------
-    ) (
-       input clkA,
-       input enaA, 
-       input [NUM_COL-1:0] weA,
-       input [ADDR_WIDTH-1:0] addrA,
-       input [DATA_WIDTH-1:0] dinA,
-       output reg [DATA_WIDTH-1:0] doutA,
-       
-       input clkB,
-       input enaB,
-       input [NUM_COL-1:0] weB,
-       input [ADDR_WIDTH-1:0] addrB,
-       input [DATA_WIDTH-1:0] dinB,
-       output reg [DATA_WIDTH-1:0] doutB
-       );
-
-   
-   // Core Memory  
-   reg [DATA_WIDTH-1:0]            ram_block [(2**ADDR_WIDTH)-1:0];
-   
-   // Port-A Operation
-   generate
-      genvar                       i;
-      for(i=0;i<NUM_COL;i=i+1) begin
-         always @ (posedge clkA) begin
-            if(enaA) begin
-               if(weA[i]) begin
-                  ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
-               end
-            end
-         end
-      end
-   endgenerate
-   
-   always @ (posedge clkA) begin
-      if(enaA) begin
-         if (~|weA)
-           doutA <= ram_block[addrA];
-      end
-   end
-   
-   
-   // Port-B Operation:
-   generate
-      for(i=0;i<NUM_COL;i=i+1) begin
-         always @ (posedge clkB) begin
-            if(enaB) begin
-               if(weB[i]) begin
-                  ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
-               end
-            end
-         end
-      end
-   endgenerate
-   
-   always @ (posedge clkB) begin
-      if(enaB) begin
-         if (~|weB)
-           doutB <= ram_block[addrB];
-      end
-   end
-   
-endmodule // bytewrite_tdp_ram_nc
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys
deleted file mode 100644
index b6818e322..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_nc.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog bytewrite_tdp_ram_nc.v
-hierarchy -top bytewrite_tdp_ram_nc
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd bytewrite_tdp_ram_nc
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 8 t:LUT2
-select -assert-count 64 t:LUT3
-select -assert-count 2 t:LUT5
-select -assert-none t:LUT2 t:LUT3 t:LUT5 t:$mem %% t:* %D
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v b/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v
deleted file mode 100644
index 349aa2aec..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.v
+++ /dev/null
@@ -1,71 +0,0 @@
-// ByteWide Write Enable, - Alternate READ_FIRST mode template - Vivado recomended
-// bytewrite_tdp_ram_readfirst2.v
-module bytewrite_tdp_ram_readfirst2
-  #(
-    //-------------------------------------------------------------------------
-    parameter   NUM_COL                 =   4,
-    parameter   COL_WIDTH               =   8,
-    parameter   ADDR_WIDTH              =  10, // Addr  Width in bits : 2**ADDR_WIDTH = RAM Depth
-    parameter   DATA_WIDTH              =  NUM_COL*COL_WIDTH  // Data  Width in bits
-    //-------------------------------------------------------------------------
-    ) (
-       input clkA,
-       input enaA, 
-       input [NUM_COL-1:0] weA,
-       input [ADDR_WIDTH-1:0] addrA,
-       input [DATA_WIDTH-1:0] dinA,
-       output reg [DATA_WIDTH-1:0] doutA,
-       
-       input clkB,
-       input enaB,
-       input [NUM_COL-1:0] weB,
-       input [ADDR_WIDTH-1:0] addrB,
-       input [DATA_WIDTH-1:0] dinB,
-       output reg [DATA_WIDTH-1:0] doutB
-       );
-   
-   
-   // Core Memory  
-   reg [DATA_WIDTH-1:0]            ram_block [(2**ADDR_WIDTH)-1:0];
-   
-   // Port-A Operation
-   generate
-      genvar                       i;
-      for(i=0;i<NUM_COL;i=i+1) begin
-         always @ (posedge clkA) begin
-            if(enaA) begin
-               if(weA[i]) begin
-                  ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
-               end
-            end
-         end
-      end
-   endgenerate
-   
-   always @ (posedge clkA) begin
-      if(enaA) begin
-         doutA <= ram_block[addrA];
-      end
-   end
-   
-   
-   // Port-B Operation:
-   generate
-      for(i=0;i<NUM_COL;i=i+1) begin
-         always @ (posedge clkB) begin
-            if(enaB) begin
-               if(weB[i]) begin
-                  ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
-               end
-            end
-         end
-      end
-   endgenerate
-   
-   always @ (posedge clkB) begin
-      if(enaB) begin
-         doutB <= ram_block[addrB];
-      end
-   end
-
-endmodule // bytewrite_tdp_ram_readfirst2
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys
deleted file mode 100644
index 3273d0d43..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_readfirst2.ys
+++ /dev/null
@@ -1,21 +0,0 @@
-read_verilog bytewrite_tdp_ram_readfirst2.v
-hierarchy -top bytewrite_tdp_ram_readfirst2
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd bytewrite_tdp_ram_readfirst2
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 8 t:LUT2
-select -assert-count 64 t:LUT3
-select -assert-none t:LUT2 t:LUT3 t:$mem %% t:* %D
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.v b/tests/xilinx_ug901/bytewrite_tdp_ram_rf.v
deleted file mode 100644
index 72dad9d8f..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.v
+++ /dev/null
@@ -1,61 +0,0 @@
-// True-Dual-Port BRAM with Byte-wide Write Enable
-//      Read-First mode 
-// bytewrite_tdp_ram_rf.v
-//
-
-module bytewrite_tdp_ram_rf
- #(
-//--------------------------------------------------------------------------
-parameter   NUM_COL             =   4,
-parameter   COL_WIDTH           =   8,
-parameter   ADDR_WIDTH          =  10, 
-// Addr  Width in bits : 2 *ADDR_WIDTH = RAM Depth
-parameter   DATA_WIDTH      =  NUM_COL*COL_WIDTH  // Data  Width in bits
-    //----------------------------------------------------------------------
-  ) (
-     input clkA,
-     input enaA, 
-     input [NUM_COL-1:0] weA,
-     input [ADDR_WIDTH-1:0] addrA,
-     input [DATA_WIDTH-1:0] dinA,
-     output reg [DATA_WIDTH-1:0] doutA,
-
-     input clkB,
-     input enaB,
-     input [NUM_COL-1:0] weB,
-     input [ADDR_WIDTH-1:0] addrB,
-     input [DATA_WIDTH-1:0] dinB,
-     output reg [DATA_WIDTH-1:0] doutB
-     );
-
-
-   // Core Memory  
-   reg [DATA_WIDTH-1:0]   ram_block [(2**ADDR_WIDTH)-1:0];
-
-   integer                i;
-   // Port-A Operation
-   always @ (posedge clkA) begin
-      if(enaA) begin
-         for(i=0;i<NUM_COL;i=i+1) begin
-            if(weA[i]) begin
-               ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
-            end
-         end
-         doutA <= ram_block[addrA];  
-      end
-   end
-
-   // Port-B Operation:
-   always @ (posedge clkB) begin
-      if(enaB) begin
-         for(i=0;i<NUM_COL;i=i+1) begin
-            if(weB[i]) begin
-               ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
-            end
-         end     
-         
-         doutB <= ram_block[addrB];  
-      end
-   end
-
-endmodule // bytewrite_tdp_ram_rf
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys
deleted file mode 100644
index 2a34d9abe..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_rf.ys
+++ /dev/null
@@ -1,21 +0,0 @@
-read_verilog bytewrite_tdp_ram_rf.v
-hierarchy -top bytewrite_tdp_ram_rf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd bytewrite_tdp_ram_rf
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 8 t:LUT2
-select -assert-count 64 t:LUT3
-select -assert-none t:LUT2 t:LUT3 t:$mem %% t:* %D
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.v b/tests/xilinx_ug901/bytewrite_tdp_ram_wf.v
deleted file mode 100644
index d39565e52..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.v
+++ /dev/null
@@ -1,68 +0,0 @@
-// True-Dual-Port BRAM with Byte-wide Write Enable
-//      Write-First mode
-// File: HDL_Coding_Techniques/rams/bytewrite_tdp_ram_wf.v
-//
-// ByteWide Write Enable, - WRITE_FIRST mode template - Vivado recomended
-module bytewrite_tdp_ram_wf
-  #(
-    //----------------------------------------------------------------------
-parameter   NUM_COL         =   4,
-parameter   COL_WIDTH       =   8,
-parameter   ADDR_WIDTH      =  10, 
-// Addr  Width in bits : 2**ADDR_WIDTH = RAM Depth
-parameter   DATA_WIDTH      =  NUM_COL*COL_WIDTH  // Data  Width in bits
-    //----------------------------------------------------------------------
-    ) (
-       input clkA,
-       input enaA, 
-       input [NUM_COL-1:0] weA,
-       input [ADDR_WIDTH-1:0] addrA,
-       input [DATA_WIDTH-1:0] dinA,
-       output reg [DATA_WIDTH-1:0] doutA,
-       
-       input clkB,
-       input enaB,
-       input [NUM_COL-1:0] weB,
-       input [ADDR_WIDTH-1:0] addrB,
-       input [DATA_WIDTH-1:0] dinB,
-       output reg [DATA_WIDTH-1:0] doutB
-       );
-   
-   
-   // Core Memory  
-   reg [DATA_WIDTH-1:0]            ram_block [(2**ADDR_WIDTH)-1:0];
-   
-   // Port-A Operation
-   generate
-      genvar                       i;
-      for(i=0;i<NUM_COL;i=i+1) begin
-         always @ (posedge clkA) begin
-            if(enaA) begin
-               if(weA[i]) begin
-                  ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] <= dinA[i*COL_WIDTH +: COL_WIDTH];
-                  doutA[i*COL_WIDTH +: COL_WIDTH]  <= dinA[i*COL_WIDTH +: COL_WIDTH] ;
-               end else begin
-                  doutA[i*COL_WIDTH +: COL_WIDTH]  <= ram_block[addrA][i*COL_WIDTH +: COL_WIDTH] ;
-               end
-            end
-         end
-      end
-   endgenerate
-   
-   // Port-B Operation:
-   generate
-      for(i=0;i<NUM_COL;i=i+1) begin
-         always @ (posedge clkB) begin
-            if(enaB) begin
-               if(weB[i]) begin
-                  ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] <= dinB[i*COL_WIDTH +: COL_WIDTH];
-                  doutB[i*COL_WIDTH +: COL_WIDTH]  <= dinB[i*COL_WIDTH +: COL_WIDTH] ;
-               end else begin 
-                  doutB[i*COL_WIDTH +: COL_WIDTH]  <= ram_block[addrB][i*COL_WIDTH +: COL_WIDTH] ;
-               end
-            end     
-         end
-      end
-   endgenerate
-   
-endmodule // bytewrite_tdp_ram_wf
diff --git a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys b/tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys
deleted file mode 100644
index b681d0c2b..000000000
--- a/tests/xilinx_ug901/bytewrite_tdp_ram_wf.ys
+++ /dev/null
@@ -1,23 +0,0 @@
-read_verilog bytewrite_tdp_ram_wf.v
-hierarchy -top bytewrite_tdp_ram_wf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd bytewrite_tdp_ram_wf
-stat
-#Vivado synthesizes 1 RAMB36E1.
-select -assert-count 1 t:$mem
-select -assert-count 2 t:BUFG
-select -assert-count 64 t:FDRE
-select -assert-count 8 t:LUT2
-select -assert-count 128 t:LUT3
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:$mem %% t:* %D
diff --git a/tests/xilinx_ug901/cmacc.v b/tests/xilinx_ug901/cmacc.v
deleted file mode 100644
index 038402daf..000000000
--- a/tests/xilinx_ug901/cmacc.v
+++ /dev/null
@@ -1,122 +0,0 @@
-// Complex Multiplier with accumulation (pr+i.pi) = (ar+i.ai)*(br+i.bi)
-// File: cmacc.v
-// The RTL below describes a complex multiplier with accumulation
-// which can be packed into 3 DSP blocks (Ultrascale architecture)
-//Default parameters were changed because of slow test
-//module cmacc # (parameter AWIDTH = 16, BWIDTH = 18, SIZEOUT = 40)
-module cmacc # (parameter AWIDTH = 4, BWIDTH = 5, SIZEOUT = 9)
-  (
-   input clk,
-   input sload,
-   input signed [AWIDTH-1:0] ar,
-   input signed [AWIDTH-1:0] ai,
-  input signed [BWIDTH-1:0]   br,
-  input signed [BWIDTH-1:0]   bi,
-  output signed [SIZEOUT-1:0] pr,
-  output signed [SIZEOUT-1:0] pi);
-
-  reg signed [AWIDTH-1:0]  ai_d, ai_dd, ai_ddd, ai_dddd;
-  reg signed [AWIDTH-1:0] ar_d, ar_dd, ar_ddd, ar_dddd;
-  reg signed [BWIDTH-1:0] bi_d, bi_dd, bi_ddd, br_d, br_dd, br_ddd;
-  reg signed [AWIDTH:0] addcommon;
-  reg signed [BWIDTH:0] addr, addi;
-  reg signed [AWIDTH+BWIDTH:0] mult0, multr, multi;
-  reg signed [SIZEOUT-1:0] pr_int, pi_int, old_result_real, old_result_im;
-  reg signed [AWIDTH+BWIDTH:0] common, commonr1, commonr2;
-
-  reg sload_reg;
-
- `ifdef SIM
-  initial
-  begin
-    ai_d = 0;
-    ai_dd = 0;
-    ai_ddd = 0;
-    ai_dddd = 0;
-    ar_d = 0;
-    ar_dd = 0;
-    ar_ddd = 0;
-    ar_dddd = 0;
-    bi_d = 0;
-    bi_dd = 0;
-    bi_ddd = 0;
-    br_d = 0;
-    br_dd = 0;
-    br_ddd = 0;
-  end
- `endif
-
-  always @(posedge clk)
-  begin
-    ar_d      <= ar;
-    ar_dd     <= ar_d;
-    ai_d      <= ai;
-    ai_dd     <= ai_d;
-    br_d      <= br;
-    br_dd     <= br_d;
-    br_ddd    <= br_dd;
-    bi_d      <= bi;
-    bi_dd     <= bi_d;
-    bi_ddd    <= bi_dd;
-    sload_reg <= sload;
-  end
-
-  // Common factor (ar ai) x bi, shared for the calculations of the real and imaginary final products
-  //
-  always @(posedge clk)
-  begin
-    addcommon <= ar_d - ai_d;
-    mult0     <= addcommon * bi_dd;
-    common    <= mult0;
-  end
-
-  // Accumulation loop (combinatorial) for *Real*
-  //
-  always @(sload_reg or pr_int)
-  if (sload_reg)
-  old_result_real <= 0;
-  else
-  // 'sload' is now and opens the accumulation loop.
-  // The accumulator takes the next multiplier output
-  // in the same cycle.
-  old_result_real <= pr_int;
-
-  // Real product
-  //
-  always @(posedge clk)
-  begin
-    ar_ddd   <= ar_dd;
-    ar_dddd  <= ar_ddd;
-    addr     <= br_ddd - bi_ddd;
-    multr    <= addr * ar_dddd;
-    commonr1 <= common;
-    pr_int   <= multr + commonr1 + old_result_real;
-  end
-
-  // Accumulation loop (combinatorial) for *Imaginary*
-  //
-  always @(sload_reg or pi_int)
-  if (sload_reg)
-  old_result_im <= 0;
-  else
-  // 'sload' is now and opens the accumulation loop.
-  // The accumulator takes the next multiplier output
-  // in the same cycle.
-  old_result_im <= pi_int;
-
-  // Imaginary product
-  //
-  always @(posedge clk)
-  begin
-    ai_ddd   <= ai_dd;
-    ai_dddd  <= ai_ddd;
-    addi     <= br_ddd + bi_ddd;
-    multi    <= addi * ai_dddd;
-    commonr2 <= common;
-    pi_int   <= multi + commonr2 + old_result_im;
-  end
-
-  assign pr = pr_int;
-  assign pi = pi_int;
-
-endmodule // cmacc
diff --git a/tests/xilinx_ug901/cmacc.ys b/tests/xilinx_ug901/cmacc.ys
deleted file mode 100644
index c1ac931c8..000000000
--- a/tests/xilinx_ug901/cmacc.ys
+++ /dev/null
@@ -1,25 +0,0 @@
-read_verilog cmacc.v
-hierarchy -top cmacc
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd cmacc
-#Vivado synthesizes 5 DSP48E1, 32 FDRE, 18 LUT.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 77 t:FDRE
-select -assert-count 5 t:LUT1
-select -assert-count 46 t:LUT2
-select -assert-count 25 t:LUT3
-select -assert-count 8 t:LUT4
-select -assert-count 16 t:LUT5
-select -assert-count 85 t:LUT6
-select -assert-count 54 t:MUXCY
-select -assert-count 8 t:MUXF7
-select -assert-count 2 t:MUXF8
-select -assert-count 22 t:SRL16E
-select -assert-count 62 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:SRL16E t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/cmult.v b/tests/xilinx_ug901/cmult.v
deleted file mode 100644
index d5d85a28c..000000000
--- a/tests/xilinx_ug901/cmult.v
+++ /dev/null
@@ -1,71 +0,0 @@
-//
-// Complex Multiplier (pr+i.pi) = (ar+i.ai)*(br+i.bi)
-// file: cmult.v
-
-module cmult # (parameter AWIDTH = 16, BWIDTH = 18)
-   (
-    input clk,
-    input signed [AWIDTH-1:0]      ar, ai,
-    input signed [BWIDTH-1:0]      br, bi,
-    output signed [AWIDTH+BWIDTH:0] pr, pi
-   );
-
-reg signed [AWIDTH-1:0] ai_d, ai_dd, ai_ddd, ai_dddd   ; 
-reg signed [AWIDTH-1:0] ar_d, ar_dd, ar_ddd, ar_dddd   ; 
-reg signed [BWIDTH-1:0] bi_d, bi_dd, bi_ddd, br_d, br_dd, br_ddd ; 
-reg signed [AWIDTH:0]  addcommon     ; 
-reg signed [BWIDTH:0]  addr, addi     ; 
-reg signed [AWIDTH+BWIDTH:0] mult0, multr, multi, pr_int, pi_int  ; 
-reg signed [AWIDTH+BWIDTH:0] common, commonr1, commonr2   ; 
-  
-always @(posedge clk)
- begin
-  ar_d   <= ar;
-  ar_dd  <= ar_d;
-  ai_d   <= ai;
-  ai_dd  <= ai_d;
-  br_d   <= br;
-  br_dd  <= br_d;
-  br_ddd <= br_dd;
-  bi_d   <= bi;
-  bi_dd  <= bi_d;
-  bi_ddd <= bi_dd;
- end
- 
-// Common factor (ar ai) x bi, shared for the calculations of the real and imaginary final products
-// 
-always @(posedge clk)
- begin
-  addcommon <= ar_d - ai_d;
-  mult0     <= addcommon * bi_dd;
-  common    <= mult0;
- end
-
-// Real product
-//
-always @(posedge clk)
- begin
-   ar_ddd   <= ar_dd;
-   ar_dddd  <= ar_ddd;
-   addr     <= br_ddd - bi_ddd;
-   multr    <= addr * ar_dddd;
-   commonr1 <= common;
-   pr_int   <= multr + commonr1;
- end
-
-// Imaginary product
-//
-always @(posedge clk)
- begin
-  ai_ddd   <= ai_dd;
-  ai_dddd  <= ai_ddd;
-  addi     <= br_ddd + bi_ddd;
-  multi    <= addi * ai_dddd;
-  commonr2 <= common;
-  pi_int   <= multi + commonr2;
- end
-
-assign pr = pr_int;
-assign pi = pi_int;
-   
-endmodule // cmult
diff --git a/tests/xilinx_ug901/cmult.ys b/tests/xilinx_ug901/cmult.ys
deleted file mode 100644
index 605f00983..000000000
--- a/tests/xilinx_ug901/cmult.ys
+++ /dev/null
@@ -1,31 +0,0 @@
-read_verilog cmult.v
-hierarchy -top cmult
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd cmult
-#Vivado synthesizes 3 DSP48E1, 68 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 281 t:FDRE
-select -assert-count 18 t:LUT1
-select -assert-count 467 t:LUT2
-select -assert-count 187 t:LUT3
-select -assert-count 98 t:LUT4
-select -assert-count 165 t:LUT5
-select -assert-count 1596 t:LUT6
-select -assert-count 222 t:MUXCY
-select -assert-count 393 t:MUXF7
-select -assert-count 121 t:MUXF8
-select -assert-count 85 t:SRL16E
-select -assert-count 230 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:SRL16E t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/dynamic_shift_registers_1.v b/tests/xilinx_ug901/dynamic_shift_registers_1.v
deleted file mode 100644
index b69c022cd..000000000
--- a/tests/xilinx_ug901/dynamic_shift_registers_1.v
+++ /dev/null
@@ -1,21 +0,0 @@
-// 32-bit dynamic shift register.
-// Download: 
-// File: dynamic_shift_registers_1.v
-
-module dynamic_shift_register_1 (CLK, CE, SEL, SI, DO);
-parameter SELWIDTH = 5;
-input CLK, CE, SI;
-input [SELWIDTH-1:0] SEL;
-output DO;
-
-localparam DATAWIDTH = 2**SELWIDTH;
-reg [DATAWIDTH-1:0] data;
-
-assign DO = data[SEL];
-
-always @(posedge CLK)
- begin
-  if (CE == 1'b1)
-    data <= {data[DATAWIDTH-2:0], SI};
-  end 
-endmodule
diff --git a/tests/xilinx_ug901/dynamic_shift_registers_1.ys b/tests/xilinx_ug901/dynamic_shift_registers_1.ys
deleted file mode 100644
index f70c84f2f..000000000
--- a/tests/xilinx_ug901/dynamic_shift_registers_1.ys
+++ /dev/null
@@ -1,15 +0,0 @@
-read_verilog dynamic_shift_registers_1.v
-hierarchy -top dynamic_shift_register_1
-proc
-flatten
-#ERROR: Found 1 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd dynamic_shift_register_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 3 SRLC32E.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:SRLC32E
-select -assert-none t:BUFG t:SRLC32E %% t:* %D
diff --git a/tests/xilinx_ug901/dynpreaddmultadd.v b/tests/xilinx_ug901/dynpreaddmultadd.v
deleted file mode 100644
index e3bb3a86c..000000000
--- a/tests/xilinx_ug901/dynpreaddmultadd.v
+++ /dev/null
@@ -1,47 +0,0 @@
-// Pre-add/subtract select with Dynamic control
-// dynpreaddmultadd.v
-//Default parameters were changed because of slow test.
-//module dynpreaddmultadd  # (parameter SIZEIN = 16)
-module dynpreaddmultadd  # (parameter SIZEIN = 8)
-        (
-          input clk, ce, rst, subadd,
-          input  signed [SIZEIN-1:0] a, b, c, d,
-          output signed [2*SIZEIN:0] dynpreaddmultadd_out
-        );
-
-// Declare registers for intermediate values
-reg signed [SIZEIN-1:0] a_reg, b_reg, c_reg;
-reg signed [SIZEIN:0]   add_reg;
-reg signed [2*SIZEIN:0] d_reg, m_reg, p_reg;
-
-always @(posedge clk)
-begin
- if (rst)
-  begin
-   a_reg   <= 0;
-   b_reg   <= 0;
-   c_reg   <= 0;
-   d_reg   <= 0;
-   add_reg <= 0;
-   m_reg   <= 0;
-   p_reg   <= 0;
-  end
- else if (ce)
-  begin
-   a_reg   <= a;
-   b_reg   <= b;
-   c_reg   <= c;
-   d_reg   <= d;
-   if (subadd)
-    add_reg <= a_reg - b_reg;
-   else
-    add_reg <= a_reg + b_reg;
-   m_reg   <= add_reg * c_reg;
-   p_reg   <= m_reg + d_reg;
-  end
-end
-
-// Output accumulation result
-assign dynpreaddmultadd_out = p_reg;
-
-endmodule // dynpreaddmultadd
diff --git a/tests/xilinx_ug901/dynpreaddmultadd.ys b/tests/xilinx_ug901/dynpreaddmultadd.ys
deleted file mode 100644
index f74128dae..000000000
--- a/tests/xilinx_ug901/dynpreaddmultadd.ys
+++ /dev/null
@@ -1,31 +0,0 @@
-read_verilog dynpreaddmultadd.v
-hierarchy -top dynpreaddmultadd
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd dynpreaddmultadd
-
-#Vivado synthesizes 1 DSP48E1.
-select -assert-count 1 t:BUFG
-select -assert-count 75 t:FDRE
-select -assert-count 8 t:LUT1
-select -assert-count 131 t:LUT2
-select -assert-count 19 t:LUT3
-select -assert-count 26 t:LUT4
-select -assert-count 12 t:LUT5
-select -assert-count 142 t:LUT6
-select -assert-count 48 t:MUXCY
-select -assert-count 50 t:MUXF7
-select -assert-count 15 t:MUXF8
-select -assert-count 52 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/fsm_1.v b/tests/xilinx_ug901/fsm_1.v
deleted file mode 100644
index ee3571d0d..000000000
--- a/tests/xilinx_ug901/fsm_1.v
+++ /dev/null
@@ -1,42 +0,0 @@
-// State Machine with single sequential block
-//fsm_1.v
-module fsm_1(clk,reset,flag,sm_out);
-input clk,reset,flag;
-output reg sm_out;
-
-parameter s1 = 3'b000;
-parameter s2 = 3'b001;
-parameter s3 = 3'b010;
-parameter s4 = 3'b011;
-parameter s5 = 3'b111;
-
-reg [2:0] state;
-
-always@(posedge clk)
-  begin
-    if(reset)
-      begin
-        state <= s1;
-        sm_out  <= 1'b1;
-      end
-  else
-    begin
-     case(state)
-       s1: if(flag) 
-            begin 
-              state <= s2; 
-              sm_out <= 1'b1; 
-            end
-           else
-            begin
-              state <= s3;
-              sm_out <= 1'b0;
-            end
-       s2: begin state <= s4; sm_out <= 1'b0; end
-       s3: begin state <= s4; sm_out <= 1'b0; end
-       s4: begin state <= s5; sm_out <= 1'b1; end
-       s5: begin state <= s1; sm_out <= 1'b1; end
-     endcase
-    end
- end
-endmodule
diff --git a/tests/xilinx_ug901/fsm_1.ys b/tests/xilinx_ug901/fsm_1.ys
deleted file mode 100644
index 192966163..000000000
--- a/tests/xilinx_ug901/fsm_1.ys
+++ /dev/null
@@ -1,16 +0,0 @@
-read_verilog fsm_1.v
-hierarchy -top fsm_1
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd fsm_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 2 LUT5, 2 LUT4, 1 LUT3, 4 FDRE.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 4 t:FDRE
-select -assert-count 2 t:LUT4
-select -assert-count 2 t:LUT5
-select -assert-count 1 t:LUT6
-
-select -assert-none t:BUFG t:FDRE t:LUT4 t:LUT5 t:LUT6 %% t:* %D
diff --git a/tests/xilinx_ug901/latches.v b/tests/xilinx_ug901/latches.v
deleted file mode 100644
index 09d0f9f73..000000000
--- a/tests/xilinx_ug901/latches.v
+++ /dev/null
@@ -1,17 +0,0 @@
-// Latch with Positive Gate and Asynchronous Reset
-// File: latches.v
-module latches (
-                input G,
-                input D,
-                input CLR,
-                output reg Q
-               );
-always @ *
-begin
- if(CLR)
-  Q = 0;
- else if(G)
-  Q = D;
-end
-
-endmodule               
diff --git a/tests/xilinx_ug901/latches.ys b/tests/xilinx_ug901/latches.ys
deleted file mode 100644
index be4a8de94..000000000
--- a/tests/xilinx_ug901/latches.ys
+++ /dev/null
@@ -1,10 +0,0 @@
-read_verilog latches.v
-proc
-hierarchy -top latches
-flatten
-synth_xilinx
-#Vivado synthesizes 1 BUFG, 8 LDCE.
-select -assert-count 2 t:LUT2
-select -assert-count 1 t:$_DLATCH_P_
-#ERROR: Assertion failed: selection is not empty: t:LUT2 t:$_DLATCH_P_ %% t:* %D
-#select -assert-none t:LUT2 t:$_DLATCH_P_ %% t:* %D
diff --git a/tests/xilinx_ug901/macc.v b/tests/xilinx_ug901/macc.v
deleted file mode 100644
index 9db8ea2c9..000000000
--- a/tests/xilinx_ug901/macc.v
+++ /dev/null
@@ -1,47 +0,0 @@
-// Signed 40-bit streaming accumulator with 16-bit inputs
-// File: macc.v
-//
-module macc  # (
-				//Default parameters were changed because of slow test
-               // parameter SIZEIN = 16, SIZEOUT = 40
-               // parameter SIZEIN = 12, SIZEOUT = 30
-                parameter SIZEIN = 8, SIZEOUT = 20
-               )
-               (
-                input clk, ce, sload,
-                input signed  [SIZEIN-1:0]  a, b,
-                output signed [SIZEOUT-1:0] accum_out
-               );
-
-   // Declare registers for intermediate values
-reg signed [SIZEIN-1:0]  a_reg, b_reg;
-reg                      sload_reg;
-reg signed [2*SIZEIN:0]  mult_reg;
-reg signed [SIZEOUT-1:0] adder_out, old_result;
-
-always @(adder_out or sload_reg)
-begin
-  if (sload_reg)
-    old_result <= 0;
-  else
-   // 'sload' is now active (=low) and opens the accumulation loop.
-   // The accumulator takes the next multiplier output in
-   // the same cycle.
-    old_result <= adder_out;
-end
-
-always @(posedge clk)
- if (ce)
-   begin
-      a_reg <= a;
-      b_reg <= b;
-      mult_reg <= a_reg * b_reg;
-      sload_reg <= sload;
-      // Store accumulation result into a register
-      adder_out <= old_result + mult_reg;
-   end
-
-// Output accumulation result
-assign accum_out = adder_out;
-
-endmodule // macc
diff --git a/tests/xilinx_ug901/macc.ys b/tests/xilinx_ug901/macc.ys
deleted file mode 100644
index 5a78a352c..000000000
--- a/tests/xilinx_ug901/macc.ys
+++ /dev/null
@@ -1,23 +0,0 @@
-read_verilog macc.v
-hierarchy -top macc
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd macc
-#Vivado synthesizes 1 DSP48E1, 1 FDRE. (When SIZEIN = 12, SIZEOUT = 30)
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 53 t:FDRE
-select -assert-count 64 t:LUT2
-select -assert-count 10 t:LUT3
-select -assert-count 22 t:LUT4
-select -assert-count 14 t:LUT5
-select -assert-count 123 t:LUT6
-select -assert-count 34 t:MUXCY
-select -assert-count 41 t:MUXF7
-select -assert-count 14 t:MUXF8
-select -assert-count 36 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/mult_unsigned.v b/tests/xilinx_ug901/mult_unsigned.v
deleted file mode 100644
index 466c16cf8..000000000
--- a/tests/xilinx_ug901/mult_unsigned.v
+++ /dev/null
@@ -1,33 +0,0 @@
-// Unsigned 16x24-bit Multiplier
-// 1 latency stage on operands
-// 3 latency stage after the multiplication
-// File: multipliers2.v
-//
-module mult_unsigned (clk, A, B, RES);
-//Default parameters were changed because of slow test
-//parameter WIDTHA = 16;
-//parameter WIDTHB = 24;
-parameter WIDTHA = 8;
-parameter WIDTHB = 12;
-input clk;
-input [WIDTHA-1:0] A;
-input [WIDTHB-1:0] B;
-output [WIDTHA+WIDTHB-1:0] RES;
-
-reg [WIDTHA-1:0] rA;
-reg [WIDTHB-1:0] rB;
-reg [WIDTHA+WIDTHB-1:0] M [3:0];
-
-integer i;
-always @(posedge clk)
- begin
-  rA <= A;
-  rB <= B;
-  M[0] <= rA * rB;
-  for (i = 0; i < 3; i = i+1)
-    M[i+1] <= M[i];
- end
-
-assign RES = M[3];
-
-endmodule
diff --git a/tests/xilinx_ug901/mult_unsigned.ys b/tests/xilinx_ug901/mult_unsigned.ys
deleted file mode 100644
index a929ca3ad..000000000
--- a/tests/xilinx_ug901/mult_unsigned.ys
+++ /dev/null
@@ -1,29 +0,0 @@
-read_verilog mult_unsigned.v
-hierarchy -top mult_unsigned
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd mult_unsigned
-
-#Vivado synthesizes 1 DSP48E1, 40 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 20 t:FDRE
-select -assert-count 33 t:LUT2
-select -assert-count 1 t:LUT3
-select -assert-count 11 t:LUT4
-select -assert-count 4 t:LUT5
-select -assert-count 139 t:LUT6
-select -assert-count 19 t:MUXCY
-select -assert-count 35 t:MUXF7
-select -assert-count 20 t:SRL16E
-select -assert-count 20 t:XORCY
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:SRL16E t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/presubmult.v b/tests/xilinx_ug901/presubmult.v
deleted file mode 100644
index 30e6133ff..000000000
--- a/tests/xilinx_ug901/presubmult.v
+++ /dev/null
@@ -1,43 +0,0 @@
-//
-// Pre-adder support in subtract mode for DSP block
-// File: presubmult.v
-
-module presubmult  # (//Default parameters were changed because of slow test
-					// parameter SIZEIN = 16
-                      parameter SIZEIN = 8
-                     )
-                     (
-                      input clk, ce, rst,
-                      input  signed [SIZEIN-1:0] a, b, c,
-                      output signed [2*SIZEIN:0] presubmult_out
-                     );
-
-// Declare registers for intermediate values
-reg signed [SIZEIN-1:0] a_reg, b_reg, c_reg;
-reg signed [SIZEIN:0]   add_reg;
-reg signed [2*SIZEIN:0] m_reg, p_reg;
-
-always @(posedge clk)
- if (rst)
-  begin
-     a_reg   <= 0;
-     b_reg   <= 0;
-     c_reg   <= 0;
-     add_reg <= 0;
-     m_reg   <= 0;
-     p_reg   <= 0;
-  end
- else if (ce)
-  begin
-     a_reg   <= a;
-     b_reg   <= b;
-     c_reg   <= c;
-     add_reg <= a - b;
-     m_reg   <= add_reg * c_reg;
-     p_reg   <= m_reg;
-  end
-
-// Output accumulation result
-assign presubmult_out = p_reg;
-
-endmodule // presubmult
diff --git a/tests/xilinx_ug901/presubmult.ys b/tests/xilinx_ug901/presubmult.ys
deleted file mode 100644
index 831458dec..000000000
--- a/tests/xilinx_ug901/presubmult.ys
+++ /dev/null
@@ -1,23 +0,0 @@
-read_verilog presubmult.v
-hierarchy -top presubmult
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd presubmult
-#Vivado synthesizes 1 DSP48E1. (When SIZEIN = 8)
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 51 t:FDRE
-select -assert-count 75 t:LUT2
-select -assert-count 10 t:LUT3
-select -assert-count 24 t:LUT4
-select -assert-count 15 t:LUT5
-select -assert-count 136 t:LUT6
-select -assert-count 24 t:MUXCY
-select -assert-count 46 t:MUXF7
-select -assert-count 14 t:MUXF8
-select -assert-count 26 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/ram_simple_dual_one_clock.v b/tests/xilinx_ug901/ram_simple_dual_one_clock.v
deleted file mode 100644
index 3390e2da5..000000000
--- a/tests/xilinx_ug901/ram_simple_dual_one_clock.v
+++ /dev/null
@@ -1,25 +0,0 @@
-// Simple Dual-Port Block RAM with One Clock
-// File: simple_dual_one_clock.v
-
-module simple_dual_one_clock (clk,ena,enb,wea,addra,addrb,dia,dob);
-
-input clk,ena,enb,wea;
-input [9:0] addra,addrb;
-input [15:0] dia;
-output [15:0] dob;
-reg [15:0] ram [1023:0];
-reg [15:0] doa,dob;
-
-always @(posedge clk) begin 
- if (ena) begin
-    if (wea)
-        ram[addra] <= dia;
- end
-end
-
-always @(posedge clk) begin 
-  if (enb)
-    dob <= ram[addrb];
-end
-
-endmodule
\ No newline at end of file
diff --git a/tests/xilinx_ug901/ram_simple_dual_one_clock.ys b/tests/xilinx_ug901/ram_simple_dual_one_clock.ys
deleted file mode 100644
index c1bde951e..000000000
--- a/tests/xilinx_ug901/ram_simple_dual_one_clock.ys
+++ /dev/null
@@ -1,20 +0,0 @@
-read_verilog ram_simple_dual_one_clock.v
-hierarchy -top simple_dual_one_clock
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-design -load postopt
-cd simple_dual_one_clock
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
diff --git a/tests/xilinx_ug901/ram_simple_dual_two_clocks.v b/tests/xilinx_ug901/ram_simple_dual_two_clocks.v
deleted file mode 100644
index 1113b928e..000000000
--- a/tests/xilinx_ug901/ram_simple_dual_two_clocks.v
+++ /dev/null
@@ -1,30 +0,0 @@
-// Simple Dual-Port Block RAM with Two Clocks
-// File: simple_dual_two_clocks.v
-
-module simple_dual_two_clocks (clka,clkb,ena,enb,wea,addra,addrb,dia,dob);
-
-input clka,clkb,ena,enb,wea;
-input [9:0] addra,addrb;
-input [15:0] dia;
-output [15:0] dob;
-reg [15:0] ram [1023:0];
-reg [15:0] dob;
-
-always @(posedge clka) 
-begin 
-  if (ena)
-    begin
-      if (wea)
-        ram[addra] <= dia;
-    end
-end
-
-always @(posedge clkb) 
-begin
-  if (enb)
-    begin
-      dob <= ram[addrb];
-    end
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/ram_simple_dual_two_clocks.ys b/tests/xilinx_ug901/ram_simple_dual_two_clocks.ys
deleted file mode 100644
index db0d789e9..000000000
--- a/tests/xilinx_ug901/ram_simple_dual_two_clocks.ys
+++ /dev/null
@@ -1,20 +0,0 @@
-read_verilog ram_simple_dual_two_clocks.v
-hierarchy -top simple_dual_two_clocks
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-design -load postopt
-cd simple_dual_two_clocks
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
diff --git a/tests/xilinx_ug901/rams_dist.v b/tests/xilinx_ug901/rams_dist.v
deleted file mode 100644
index 405283b69..000000000
--- a/tests/xilinx_ug901/rams_dist.v
+++ /dev/null
@@ -1,24 +0,0 @@
-// Dual-Port RAM with Asynchronous Read (Distributed RAM)
-// File: rams_dist.v
-
-module rams_dist (clk, we, a, dpra, di, spo, dpo);
-
-input clk;
-input we;
-input [5:0] a;
-input [5:0] dpra;
-input [15:0] di;
-output [15:0] spo;
-output [15:0] dpo;
-reg [15:0] ram [63:0];
-
-always @(posedge clk) 
-begin 
- if (we)
-   ram[a] <= di;
-end
-
-assign spo = ram[a];
-assign dpo = ram[dpra];
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_dist.ys b/tests/xilinx_ug901/rams_dist.ys
deleted file mode 100644
index 0aa1a8309..000000000
--- a/tests/xilinx_ug901/rams_dist.ys
+++ /dev/null
@@ -1,21 +0,0 @@
-read_verilog rams_dist.v
-hierarchy -top rams_dist
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_dist
-stat
-#Vivado synthesizes 32 RAM64X1D.
-select -assert-count 1 t:BUFG
-select -assert-count 32 t:RAM64X1D
-
-select -assert-none t:BUFG t:RAM64X1D %% t:* %D
diff --git a/tests/xilinx_ug901/rams_init_file.data b/tests/xilinx_ug901/rams_init_file.data
deleted file mode 100644
index f14f0b324..000000000
--- a/tests/xilinx_ug901/rams_init_file.data
+++ /dev/null
@@ -1,64 +0,0 @@
-00001110110000011001111011000110
-00101011001011010101001000100011
-01110100010100011000011100001111
-01000001010000100101001110010100
-00001001101001111111101000101011
-00101101001011111110101010100111
-11101111000100111000111101101101
-10001111010010011001000011101111
-00000001100011100011110010011111
-11011111001110101011111001001010
-11100111010100111110110011001010
-11000100001001101100111100101001
-10001011100101011111111111100001
-11110101110110010000010110111010
-01001011000000111001010110101110
-11100001111111001010111010011110
-01101111011010010100001101110001
-01010100011011111000011000100100
-11110000111101101111001100001011
-10101101001111010100100100011100
-01011100001010111111101110101110
-01011101000100100111010010110101
-11110111000100000101011101101101
-11100111110001111010101100001101
-01110100000011101111111000011111
-00010011110101111000111001011101
-01101110001111100011010101101111
-10111100000000010011101011011011
-11000001001101001101111100010000
-00011111110010110110011111010101
-01100100100000011100100101110000
-10001000000100111011001010001111
-11001000100011101001010001100001
-10000000100111010011100111100011
-11011111010010100010101010000111
-10000000110111101000111110111011
-10110011010111101111000110011001
-00010111100001001010110111011100
-10011100101110101111011010110011
-01010011101101010001110110011010
-01111011011100010101000101000001
-10001000000110010110111001101010
-11101000001101010000111001010110
-11100011111100000111110101110101
-01001010000000001111111101101111
-00100011000011001000000010001111
-10011000111010110001001011100100
-11111111111011110101000101000111
-11000011000101000011100110100000
-01101101001011111010100011101001
-10000111101100101001110011010111
-11010110100100101110110010100100
-01001111111001101101011111001011
-11011001001101110110000100110111
-10110110110111100101110011100110
-10011100111001000010111111010110
-00000000001011011111001010110010
-10100110011010000010001000011011
-11001010111111001001110001110101
-00100001100010000111000101001000
-00111100101111110001101101111010
-11000010001010000000010100100001
-11000001000110001101000101001110
-10010011010100010001100100100111
diff --git a/tests/xilinx_ug901/rams_init_file.v b/tests/xilinx_ug901/rams_init_file.v
deleted file mode 100644
index 046779af9..000000000
--- a/tests/xilinx_ug901/rams_init_file.v
+++ /dev/null
@@ -1,24 +0,0 @@
-// Initializing Block RAM from external data file
-// Binary data
-// File: rams_init_file.v 
-
-module rams_init_file (clk, we, addr, din, dout);
-input clk;
-input we;
-input [5:0] addr;
-input [31:0] din;
-output [31:0] dout;
-
-reg [31:0] ram [0:63];
-reg [31:0] dout;
-
-initial begin
-$readmemb("rams_init_file.data",ram);
-end
-
-always @(posedge clk)
-begin
-  if (we)
-     ram[addr] <= din;
-  dout <= ram[addr];
-end endmodule
diff --git a/tests/xilinx_ug901/rams_init_file.ys b/tests/xilinx_ug901/rams_init_file.ys
deleted file mode 100644
index d22a0f52c..000000000
--- a/tests/xilinx_ug901/rams_init_file.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog rams_init_file.v
-hierarchy -top rams_init_file
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_init_file
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 32 t:FDRE
-select -assert-count 32 t:RAM64X1D
-
-select -assert-none t:BUFG t:FDRE t:RAM64X1D %% t:* %D
diff --git a/tests/xilinx_ug901/rams_pipeline.v b/tests/xilinx_ug901/rams_pipeline.v
deleted file mode 100644
index e86d417f5..000000000
--- a/tests/xilinx_ug901/rams_pipeline.v
+++ /dev/null
@@ -1,42 +0,0 @@
-// Block RAM with Optional Output Registers
-// File: rams_pipeline
-
-module rams_pipeline (clk1, clk2, we, en1, en2, addr1, addr2, di, res1, res2);
-input clk1;
-input clk2;
-input we, en1, en2;
-input [9:0] addr1;
-input [9:0] addr2;
-input [15:0] di;
-output [15:0] res1;
-output [15:0] res2;
-reg [15:0] res1;
-reg [15:0] res2;
-reg [15:0] RAM [1023:0];
-reg [15:0] do1;
-reg [15:0] do2;
-
-always @(posedge clk1)
-begin
-    if (we == 1'b1)
-        RAM[addr1] <= di;
-    do1 <= RAM[addr1];
-end
-
-always @(posedge clk2)
-begin
-    do2 <= RAM[addr2];
-end
-
-always @(posedge clk1)
-begin
-    if (en1 == 1'b1)
-        res1 <= do1;
-end
-
-always @(posedge clk2)
-begin
-    if (en2 == 1'b1)
-        res2 <= do2;
-end 
-endmodule
diff --git a/tests/xilinx_ug901/rams_pipeline.ys b/tests/xilinx_ug901/rams_pipeline.ys
deleted file mode 100644
index 7fd7c76e4..000000000
--- a/tests/xilinx_ug901/rams_pipeline.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog rams_pipeline.v
-hierarchy -top rams_pipeline
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_pipeline
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 2 t:BUFG
-select -assert-count 32 t:FDRE
-select -assert-count 2 t:RAMB18E1
-
-select -assert-none t:BUFG t:FDRE t:RAMB18E1 %% t:* %D
diff --git a/tests/xilinx_ug901/rams_sp_nc.v b/tests/xilinx_ug901/rams_sp_nc.v
deleted file mode 100644
index 08abc0d2c..000000000
--- a/tests/xilinx_ug901/rams_sp_nc.v
+++ /dev/null
@@ -1,26 +0,0 @@
-// Single-Port Block RAM No-Change Mode
-// File: rams_sp_nc.v
-
-module rams_sp_nc (clk, we, en, addr, di, dout);
-
-input clk; 
-input we; 
-input en;
-input [9:0] addr; 
-input [15:0] di; 
-output [15:0] dout;
-
-reg [15:0] RAM [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
-  if (en)
-  begin
-    if (we)
-      RAM[addr] <= di;
-    else
-      dout <= RAM[addr];
-  end
-end
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_nc.ys b/tests/xilinx_ug901/rams_sp_nc.ys
deleted file mode 100644
index 9b7d6386f..000000000
--- a/tests/xilinx_ug901/rams_sp_nc.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog rams_sp_nc.v
-hierarchy -top rams_sp_nc
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_sp_nc
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 2 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
diff --git a/tests/xilinx_ug901/rams_sp_rf.v b/tests/xilinx_ug901/rams_sp_rf.v
deleted file mode 100644
index 5e0adf88b..000000000
--- a/tests/xilinx_ug901/rams_sp_rf.v
+++ /dev/null
@@ -1,26 +0,0 @@
-// Single-Port Block RAM Read-First Mode
-// rams_sp_rf.v
-module rams_sp_rf (clk, en, we, addr, di, dout);
-
-input clk; 
-input we; 
-input en;
-input [9:0] addr; 
-input [15:0] di; 
-output [15:0] dout;
-
-reg [15:0] RAM [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
-  if (en)
-    begin
-      if (we)
-        RAM[addr]<=di;
-      dout <= RAM[addr];
-    end
-end
-
-endmodule
-
diff --git a/tests/xilinx_ug901/rams_sp_rf.ys b/tests/xilinx_ug901/rams_sp_rf.ys
deleted file mode 100644
index 56f345c63..000000000
--- a/tests/xilinx_ug901/rams_sp_rf.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog rams_sp_rf.v
-hierarchy -top rams_sp_rf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_sp_rf
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:LUT2
-select -assert-count 1 t:RAMB18E1
-
-select -assert-none t:BUFG t:LUT2 t:RAMB18E1 %% t:* %D
diff --git a/tests/xilinx_ug901/rams_sp_rf_rst.v b/tests/xilinx_ug901/rams_sp_rf_rst.v
deleted file mode 100644
index cb8d50c4c..000000000
--- a/tests/xilinx_ug901/rams_sp_rf_rst.v
+++ /dev/null
@@ -1,29 +0,0 @@
-// Block RAM with Resettable Data Output
-// File: rams_sp_rf_rst.v
-
-module rams_sp_rf_rst (clk, en, we, rst, addr, di, dout);
-input clk; 
-input en; 
-input we; 
-input rst;
-input [9:0] addr; 
-input [15:0] di; 
-output [15:0] dout;
-
-reg [15:0] ram [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
-  if (en) //optional enable
-    begin
-      if (we) //write enable
-        ram[addr] <= di;
-      if (rst) //optional reset
-        dout <= 0;
-      else
-        dout <= ram[addr];
-    end
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_rf_rst.ys b/tests/xilinx_ug901/rams_sp_rf_rst.ys
deleted file mode 100644
index 57e4df9f5..000000000
--- a/tests/xilinx_ug901/rams_sp_rf_rst.ys
+++ /dev/null
@@ -1,28 +0,0 @@
-read_verilog rams_sp_rf_rst.v
-hierarchy -top rams_sp_rf_rst
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_sp_rf_rst
-stat
-#Vivado synthesizes 1 RAMB18E1.
-
-select -assert-count 1 t:BUFG
-select -assert-count 16 t:FDRE
-select -assert-count 5 t:LUT2
-select -assert-count 4 t:LUT3
-select -assert-count 13 t:LUT4
-select -assert-count 23 t:LUT5
-select -assert-count 32 t:LUT6
-select -assert-count 128 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:RAM128X1D %% t:* %D
diff --git a/tests/xilinx_ug901/rams_sp_rom.v b/tests/xilinx_ug901/rams_sp_rom.v
deleted file mode 100644
index b6e05f6c8..000000000
--- a/tests/xilinx_ug901/rams_sp_rom.v
+++ /dev/null
@@ -1,46 +0,0 @@
-// Initializing Block RAM (Single-Port Block RAM)
-// File: rams_sp_rom 
-module rams_sp_rom (clk, we, addr, di, dout);
-input clk;
-input we;
-input [5:0] addr;
-input [19:0] di;
-output [19:0] dout;
-
-reg [19:0] ram [63:0];
-reg [19:0] dout;
-
-initial 
-begin
-  ram[63] = 20'h0200A; ram[62] = 20'h00300; ram[61] = 20'h08101;
-  ram[60] = 20'h04000; ram[59] = 20'h08601; ram[58] = 20'h0233A;
-  ram[57] = 20'h00300; ram[56] = 20'h08602; ram[55] = 20'h02310;
-  ram[54] = 20'h0203B; ram[53] = 20'h08300; ram[52] = 20'h04002;
-  ram[51] = 20'h08201; ram[50] = 20'h00500; ram[49] = 20'h04001;
-  ram[48] = 20'h02500; ram[47] = 20'h00340; ram[46] = 20'h00241;
-  ram[45] = 20'h04002; ram[44] = 20'h08300; ram[43] = 20'h08201;
-  ram[42] = 20'h00500; ram[41] = 20'h08101; ram[40] = 20'h00602;
-  ram[39] = 20'h04003; ram[38] = 20'h0241E; ram[37] = 20'h00301;
-  ram[36] = 20'h00102; ram[35] = 20'h02122; ram[34] = 20'h02021;
-  ram[33] = 20'h00301; ram[32] = 20'h00102; ram[31] = 20'h02222;
-  ram[30] = 20'h04001; ram[29] = 20'h00342; ram[28] = 20'h0232B; 
-  ram[27] = 20'h00900; ram[26] = 20'h00302; ram[25] = 20'h00102; 
-  ram[24] = 20'h04002; ram[23] = 20'h00900; ram[22] = 20'h08201; 
-  ram[21] = 20'h02023; ram[20] = 20'h00303; ram[19] = 20'h02433; 
-  ram[18] = 20'h00301; ram[17] = 20'h04004; ram[16] = 20'h00301; 
-  ram[15] = 20'h00102; ram[14] = 20'h02137; ram[13] = 20'h02036; 
-  ram[12] = 20'h00301; ram[11] = 20'h00102; ram[10] = 20'h02237; 
-  ram[9]  = 20'h04004; ram[8]  = 20'h00304; ram[7] = 20'h04040; 
-  ram[6]  = 20'h02500; ram[5]  = 20'h02500; ram[4] = 20'h02500; 
-  ram[3]  = 20'h0030D; ram[2]  = 20'h02341; ram[1] = 20'h08201; 
-  ram[0]  = 20'h0400D;
-end
- 
-always @(posedge clk)
-begin
-  if (we)
-    ram[addr] <= di;
-  dout <= ram[addr];
-end 
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_rom.ys b/tests/xilinx_ug901/rams_sp_rom.ys
deleted file mode 100644
index bb8680df0..000000000
--- a/tests/xilinx_ug901/rams_sp_rom.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog rams_sp_rom.v
-hierarchy -top rams_sp_rom
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_sp_rom
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 20 t:RAM64X1D
-select -assert-count 20 t:FDRE
-
-select -assert-none t:BUFG t:RAM64X1D t:FDRE %% t:* %D
diff --git a/tests/xilinx_ug901/rams_sp_rom_1.v b/tests/xilinx_ug901/rams_sp_rom_1.v
deleted file mode 100644
index b3b8e89fe..000000000
--- a/tests/xilinx_ug901/rams_sp_rom_1.v
+++ /dev/null
@@ -1,53 +0,0 @@
-// ROMs Using Block RAM Resources.
-// File: rams_sp_rom_1.v
-//
-module rams_sp_rom_1 (clk, en, addr, dout);
-input clk;
-input en;
-input [5:0] addr;
-output  [19:0] dout;
-
-(*rom_style = "block" *) reg [19:0] data;
-
-always @(posedge clk) 
-begin 
-  if (en)
-    case(addr)
-      6'b000000: data <= 20'h0200A; 6'b100000: data <= 20'h02222;
-      6'b000001: data <= 20'h00300; 6'b100001: data <= 20'h04001;
-      6'b000010: data <= 20'h08101; 6'b100010: data <= 20'h00342;
-      6'b000011: data <= 20'h04000; 6'b100011: data <= 20'h0232B;
-      6'b000100: data <= 20'h08601; 6'b100100: data <= 20'h00900;
-      6'b000101: data <= 20'h0233A; 6'b100101: data <= 20'h00302;
-      6'b000110: data <= 20'h00300; 6'b100110: data <= 20'h00102;
-      6'b000111: data <= 20'h08602; 6'b100111: data <= 20'h04002;
-      6'b001000: data <= 20'h02310; 6'b101000: data <= 20'h00900;
-      6'b001001: data <= 20'h0203B; 6'b101001: data <= 20'h08201;
-      6'b001010: data <= 20'h08300; 6'b101010: data <= 20'h02023;
-      6'b001011: data <= 20'h04002; 6'b101011: data <= 20'h00303;
-      6'b001100: data <= 20'h08201; 6'b101100: data <= 20'h02433;
-      6'b001101: data <= 20'h00500; 6'b101101: data <= 20'h00301;
-      6'b001110: data <= 20'h04001; 6'b101110: data <= 20'h04004;
-      6'b001111: data <= 20'h02500; 6'b101111: data <= 20'h00301;
-      6'b010000: data <= 20'h00340; 6'b110000: data <= 20'h00102;
-      6'b010001: data <= 20'h00241; 6'b110001: data <= 20'h02137;
-      6'b010010: data <= 20'h04002; 6'b110010: data <= 20'h02036;
-      6'b010011: data <= 20'h08300; 6'b110011: data <= 20'h00301;
-      6'b010100: data <= 20'h08201; 6'b110100: data <= 20'h00102;
-      6'b010101: data <= 20'h00500; 6'b110101: data <= 20'h02237;
-      6'b010110: data <= 20'h08101; 6'b110110: data <= 20'h04004;
-      6'b010111: data <= 20'h00602; 6'b110111: data <= 20'h00304;
-      6'b011000: data <= 20'h04003; 6'b111000: data <= 20'h04040;
-      6'b011001: data <= 20'h0241E; 6'b111001: data <= 20'h02500;
-      6'b011010: data <= 20'h00301; 6'b111010: data <= 20'h02500;
-      6'b011011: data <= 20'h00102; 6'b111011: data <= 20'h02500;
-      6'b011100: data <= 20'h02122; 6'b111100: data <= 20'h0030D;
-      6'b011101: data <= 20'h02021; 6'b111101: data <= 20'h02341;
-      6'b011110: data <= 20'h00301; 6'b111110: data <= 20'h08201;
-      6'b011111: data <= 20'h00102; 6'b111111: data <= 20'h0400D;
-    endcase
-end 
-
-assign dout = data;
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_rom_1.ys b/tests/xilinx_ug901/rams_sp_rom_1.ys
deleted file mode 100644
index 4285df1f8..000000000
--- a/tests/xilinx_ug901/rams_sp_rom_1.ys
+++ /dev/null
@@ -1,22 +0,0 @@
-read_verilog rams_sp_rom_1.v
-hierarchy -top rams_sp_rom_1
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_sp_rom_1
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:BUFG
-select -assert-count 14 t:LUT6
-select -assert-count 14 t:FDRE
-
-select -assert-none t:BUFG t:LUT6 t:FDRE %% t:* %D
diff --git a/tests/xilinx_ug901/rams_sp_wf.v b/tests/xilinx_ug901/rams_sp_wf.v
deleted file mode 100644
index 55ed6bd54..000000000
--- a/tests/xilinx_ug901/rams_sp_wf.v
+++ /dev/null
@@ -1,26 +0,0 @@
-// Single-Port Block RAM Write-First Mode (recommended template)
-// File: rams_sp_wf.v
-module rams_sp_wf (clk, we, en, addr, di, dout);
-input clk; 
-input we; 
-input en;
-input [9:0] addr; 
-input [15:0] di; 
-output [15:0] dout;
-reg [15:0] RAM [1023:0];
-reg [15:0] dout;
-
-always @(posedge clk)
-begin
-  if (en)
-  begin
-    if (we)
-      begin
-        RAM[addr] <= di;
-        dout <= di;
-      end
-   else
-    dout <= RAM[addr];
-  end
-end
-endmodule
diff --git a/tests/xilinx_ug901/rams_sp_wf.ys b/tests/xilinx_ug901/rams_sp_wf.ys
deleted file mode 100644
index 4d9a9cfea..000000000
--- a/tests/xilinx_ug901/rams_sp_wf.ys
+++ /dev/null
@@ -1,26 +0,0 @@
-read_verilog rams_sp_wf.v
-hierarchy -top rams_sp_wf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_sp_wf
-stat
-#Vivado synthesizes 1 RAMB18E1.
-
-select -assert-count 1 t:BUFG
-select -assert-count 16 t:FDRE
-select -assert-count 44 t:LUT5
-select -assert-count 38 t:LUT6
-select -assert-count 10 t:MUXF7
-select -assert-count 128 t:RAM128X1D
-
-select -assert-none t:BUFG t:LUT2 t:FDRE t:LUT5 t:LUT6 t:MUXF7 t:RAM128X1D %% t:* %D
diff --git a/tests/xilinx_ug901/rams_tdp_rf_rf.v b/tests/xilinx_ug901/rams_tdp_rf_rf.v
deleted file mode 100644
index 63899226f..000000000
--- a/tests/xilinx_ug901/rams_tdp_rf_rf.v
+++ /dev/null
@@ -1,33 +0,0 @@
-// Dual-Port Block RAM with Two Write Ports
-// File: rams_tdp_rf_rf.v
-
-module rams_tdp_rf_rf (clka,clkb,ena,enb,wea,web,addra,addrb,dia,dib,doa,dob);
-
-input clka,clkb,ena,enb,wea,web;
-input [9:0] addra,addrb;
-input [15:0] dia,dib;
-output [15:0] doa,dob;
-reg [15:0] ram [1023:0];
-reg [15:0] doa,dob;
-
-always @(posedge clka)
-begin 
-  if (ena)
-    begin
-      if (wea)
-        ram[addra] <= dia;
-      doa <= ram[addra];
-    end
-end
-
-always @(posedge clkb) 
-begin 
-  if (enb)
-    begin
-      if (web)
-        ram[addrb] <= dib;
-      dob <= ram[addrb];
-    end
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/rams_tdp_rf_rf.ys b/tests/xilinx_ug901/rams_tdp_rf_rf.ys
deleted file mode 100644
index 20cf4fdcc..000000000
--- a/tests/xilinx_ug901/rams_tdp_rf_rf.ys
+++ /dev/null
@@ -1,21 +0,0 @@
-read_verilog rams_tdp_rf_rf.v
-hierarchy -top rams_tdp_rf_rf
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd rams_tdp_rf_rf
-stat
-#Vivado synthesizes 1 RAMB18E1.
-select -assert-count 1 t:$mem
-select -assert-count 2 t:LUT2
-
-select -assert-none t:$mem t:LUT2 %% t:* %D
diff --git a/tests/xilinx_ug901/registers_1.v b/tests/xilinx_ug901/registers_1.v
deleted file mode 100644
index beea6e666..000000000
--- a/tests/xilinx_ug901/registers_1.v
+++ /dev/null
@@ -1,25 +0,0 @@
-// 8-bit Register with
-// Rising-edge Clock
-// Active-high Synchronous Clear
-// Active-high Clock Enable
-// File: registers_1.v
-
-module registers_1(d_in,ce,clk,clr,dout);
-input [7:0] d_in;
-input ce;
-input clk;
-input clr;
-output [7:0] dout;
-reg [7:0] d_reg;
-
-always @ (posedge clk)
-begin
- if(clr)
-  d_reg <= 8'b0;
- else if(ce)
-  d_reg <= d_in;
-end
-
-assign dout = d_reg;
-endmodule
-
diff --git a/tests/xilinx_ug901/registers_1.ys b/tests/xilinx_ug901/registers_1.ys
deleted file mode 100644
index 39ca894a2..000000000
--- a/tests/xilinx_ug901/registers_1.ys
+++ /dev/null
@@ -1,12 +0,0 @@
-read_verilog registers_1.v
-hierarchy -top registers_1
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd registers_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 8 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 8 t:FDRE
-select -assert-count 9 t:LUT2
-select -assert-none t:BUFG t:FDRE t:LUT2 %% t:* %D
diff --git a/tests/xilinx_ug901/run-test.sh b/tests/xilinx_ug901/run-test.sh
deleted file mode 100755
index ea56b70f0..000000000
--- a/tests/xilinx_ug901/run-test.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/usr/bin/env bash
-set -e
-{
-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"
-	fi
-done
-} > run-test.mk
-exec ${MAKE:-make} -f run-test.mk
diff --git a/tests/xilinx_ug901/sfir_shifter.v b/tests/xilinx_ug901/sfir_shifter.v
deleted file mode 100644
index a8b144bcd..000000000
--- a/tests/xilinx_ug901/sfir_shifter.v
+++ /dev/null
@@ -1,19 +0,0 @@
-//sfir_shifter.v
-(* dont_touch = "yes" *)
-module sfir_shifter #(parameter dsize = 16, nbtap = 4)
-                     (input clk,input [dsize-1:0] datain, output [dsize-1:0] dataout);
-
-   (* srl_style = "srl_register" *) reg [dsize-1:0] tmp [0:2*nbtap-1];
-   integer i;
-
-   always @(posedge clk)
-     begin
-        tmp[0] <= datain;
-        for (i=0; i<=2*nbtap-2; i=i+1)
-          tmp[i+1] <= tmp[i];
-     end
-
-   assign dataout = tmp[2*nbtap-1];
-
-endmodule
-// sfir_shifter
diff --git a/tests/xilinx_ug901/sfir_shifter.ys b/tests/xilinx_ug901/sfir_shifter.ys
deleted file mode 100644
index b9fbeb8cb..000000000
--- a/tests/xilinx_ug901/sfir_shifter.ys
+++ /dev/null
@@ -1,16 +0,0 @@
-read_verilog sfir_shifter.v
-hierarchy -top sfir_shifter
-proc
-flatten
-#ERROR: Found 32 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd sfir_shifter
-#Vivado synthesizes 32 FDRE, 16 SRL16E.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 16 t:SRL16E
-
-select -assert-none t:BUFG t:SRL16E %% t:* %D
diff --git a/tests/xilinx_ug901/shift_registers_0.v b/tests/xilinx_ug901/shift_registers_0.v
deleted file mode 100644
index 77a3ec893..000000000
--- a/tests/xilinx_ug901/shift_registers_0.v
+++ /dev/null
@@ -1,22 +0,0 @@
-//  8-bit Shift Register
-//  Rising edge clock
-//  Active high clock enable
-//  Concatenation-based template
-//  File: shift_registers_0.v
-
-module shift_registers_0 (clk, clken, SI, SO);
-parameter WIDTH = 32; 
-input clk, clken, SI; 
-output SO;
-
-reg [WIDTH-1:0] shreg;
-
-always @(posedge clk)
-  begin
-    if (clken)
-      shreg = {shreg[WIDTH-2:0], SI};
-  end
-
-assign SO = shreg[WIDTH-1];
-
-endmodule
diff --git a/tests/xilinx_ug901/shift_registers_0.ys b/tests/xilinx_ug901/shift_registers_0.ys
deleted file mode 100644
index 89da1d7cc..000000000
--- a/tests/xilinx_ug901/shift_registers_0.ys
+++ /dev/null
@@ -1,14 +0,0 @@
-read_verilog shift_registers_0.v
-hierarchy -top shift_registers_0
-proc
-flatten
-#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd shift_registers_0 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:SRLC32E
-select -assert-none t:BUFG t:SRLC32E %% t:* %D
diff --git a/tests/xilinx_ug901/shift_registers_1.v b/tests/xilinx_ug901/shift_registers_1.v
deleted file mode 100644
index d50820e7b..000000000
--- a/tests/xilinx_ug901/shift_registers_1.v
+++ /dev/null
@@ -1,24 +0,0 @@
-// 32-bit Shift Register
-// Rising edge clock
-// Active high clock enable
-// For-loop based template
-// File: shift_registers_1.v
-
-module shift_registers_1 (clk, clken, SI, SO);
-parameter WIDTH = 32; 
-input clk, clken, SI; 
-output SO;
-reg [WIDTH-1:0] shreg;
-
-integer i;
-always @(posedge clk)
-begin
-  if (clken)
-    begin
-      for (i = 0; i < WIDTH-1; i = i+1)
-        shreg[i+1] <= shreg[i];
-      shreg[0] <= SI; 
-    end
-end
-assign SO = shreg[WIDTH-1];
-endmodule
diff --git a/tests/xilinx_ug901/shift_registers_1.ys b/tests/xilinx_ug901/shift_registers_1.ys
deleted file mode 100644
index b53b6cb25..000000000
--- a/tests/xilinx_ug901/shift_registers_1.ys
+++ /dev/null
@@ -1,14 +0,0 @@
-read_verilog shift_registers_1.v
-hierarchy -top shift_registers_1
-proc
-flatten
-#ERROR: Found 2 unproven $equiv cells in 'equiv_status -assert'.
-#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-equiv_opt -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-cd shift_registers_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 1 BUFG, 2 FDRE, 3 SRLC32E.
-select -assert-count 1 t:BUFG
-select -assert-count 1 t:SRLC32E
-select -assert-none t:BUFG t:SRLC32E %% t:* %D
diff --git a/tests/xilinx_ug901/squarediffmacc.v b/tests/xilinx_ug901/squarediffmacc.v
deleted file mode 100644
index 6535b24c4..000000000
--- a/tests/xilinx_ug901/squarediffmacc.v
+++ /dev/null
@@ -1,52 +0,0 @@
-// This module performs subtraction of two inputs, squaring on the diff
-// and then accumulation
-// This can be implemented in 1 DSP Block (Ultrascale architecture)
-// File : squarediffmacc.v
-module squarediffmacc  # (
-						//Default parameters were changed because of slow test
-                          //parameter SIZEIN = 16,
-                                    //SIZEOUT = 40
-						  parameter SIZEIN = 8,
-                          SIZEOUT = 20
-                         )
-                        (
-                         input clk,
-                         input ce,
-                         input sload,
-                         input signed [SIZEIN-1:0]   a,
-                         input signed [SIZEIN-1:0]   b,
-                         output signed [SIZEOUT+1:0] accum_out
-                        );
-
-// Declare registers for intermediate values
-reg signed [SIZEIN-1:0]  a_reg, b_reg;
-reg signed [SIZEIN:0]  diff_reg;
-reg                       sload_reg;
-reg signed [2*SIZEIN+1:0] m_reg;
-reg signed [SIZEOUT-1:0]  adder_out, old_result;
-
-  always @(sload_reg or adder_out)
-  if (sload_reg)
-    old_result <= 0;
-  else
-    // 'sload' is now and opens the accumulation loop.
-    // The accumulator takes the next multiplier output
-    // in the same cycle.
-    old_result <= adder_out;
-
-  always @(posedge clk)
-  if (ce)
-  begin
-    a_reg     <= a;
-    b_reg     <= b;
-    diff_reg  <= a_reg - b_reg;
-    m_reg  <= diff_reg * diff_reg;
-    sload_reg <= sload;
-    // Store accumulation result into a register
-    adder_out <= old_result + m_reg;
-  end
-
-  // Output accumulation result
-  assign accum_out = adder_out;
-
-endmodule // squarediffmacc
diff --git a/tests/xilinx_ug901/squarediffmacc.ys b/tests/xilinx_ug901/squarediffmacc.ys
deleted file mode 100644
index 92474bea3..000000000
--- a/tests/xilinx_ug901/squarediffmacc.ys
+++ /dev/null
@@ -1,23 +0,0 @@
-read_verilog squarediffmacc.v
-hierarchy -top squarediffmacc
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd squarediffmacc
-#Vivado synthesizes 1 DSP48E1, 33 FDRE, 16 LUT.
-stat
-select -assert-count 1 t:BUFG
-select -assert-count 64 t:FDRE
-select -assert-count 78 t:LUT2
-select -assert-count 7 t:LUT3
-select -assert-count 11 t:LUT4
-select -assert-count 8 t:LUT5
-select -assert-count 125 t:LUT6
-select -assert-count 44 t:MUXCY
-select -assert-count 50 t:MUXF7
-select -assert-count 17 t:MUXF8
-select -assert-count 47 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/squarediffmult.v b/tests/xilinx_ug901/squarediffmult.v
deleted file mode 100644
index 0f41b67bc..000000000
--- a/tests/xilinx_ug901/squarediffmult.v
+++ /dev/null
@@ -1,42 +0,0 @@
-// Squarer support for DSP block (DSP48E2) with 
-// pre-adder configured
-// as subtractor
-// File: squarediffmult.v
-
-module squarediffmult # (parameter SIZEIN = 16)
-                        (
-                          input clk, ce, rst,
-                          input  signed [SIZEIN-1:0]   a, b,
-                          output signed [2*SIZEIN+1:0] square_out
-                        );
-
-   // Declare registers for intermediate values
-reg signed [SIZEIN-1:0]   a_reg, b_reg;
-reg signed [SIZEIN:0]     diff_reg;
-reg signed [2*SIZEIN+1:0] m_reg, p_reg;
-
-always @(posedge clk)
-begin
- if (rst)
-  begin
-   a_reg    <= 0;
-   b_reg    <= 0;
-   diff_reg <= 0;   
-   m_reg    <= 0;
-   p_reg    <= 0;
-  end
- else
-  if (ce)
-  begin
-    a_reg     <= a;
-    b_reg     <= b;
-    diff_reg <= a_reg - b_reg;
-    m_reg  <= diff_reg * diff_reg;
-    p_reg  <= m_reg;     
- end
-end
-
-// Output result
-assign square_out = p_reg;
-   
-endmodule // squarediffmult
diff --git a/tests/xilinx_ug901/squarediffmult.ys b/tests/xilinx_ug901/squarediffmult.ys
deleted file mode 100644
index 3468e5bb4..000000000
--- a/tests/xilinx_ug901/squarediffmult.ys
+++ /dev/null
@@ -1,30 +0,0 @@
-read_verilog squarediffmult.v
-hierarchy -top squarediffmult
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd squarediffmult
-stat
-#Vivado synthesizes 16 FDRE, 1 DSP48E1.
-select -assert-count 1 t:BUFG
-select -assert-count 117 t:FDRE
-select -assert-count 223 t:LUT2
-select -assert-count 50 t:LUT3
-select -assert-count 38 t:LUT4
-select -assert-count 56 t:LUT5
-select -assert-count 372 t:LUT6
-select -assert-count 49 t:MUXCY
-select -assert-count 99 t:MUXF7
-select -assert-count 26 t:MUXF8
-select -assert-count 51 t:XORCY
-
-select -assert-none t:BUFG t:FDRE t:LUT2 t:LUT3 t:LUT4 t:LUT5 t:LUT6 t:MUXCY t:MUXF7 t:MUXF8 t:XORCY %% t:* %D
diff --git a/tests/xilinx_ug901/top_mux.v b/tests/xilinx_ug901/top_mux.v
deleted file mode 100644
index c23c7491c..000000000
--- a/tests/xilinx_ug901/top_mux.v
+++ /dev/null
@@ -1,18 +0,0 @@
-// Multiplexer using case statement 
-module mux4 (sel, a, b, c, d, outmux);
-input [1:0] sel;
-input [1:0] a, b, c, d;
-output [1:0] outmux;
-reg [1:0] outmux;
-
-always @ *
-   begin 
-	   case(sel)
-		  2'b00 : outmux = a;
-      2'b01 : outmux = b;
-      2'b10 : outmux = c;
-      2'b11 : outmux = d;
-     endcase
-   end 
-endmodule
-
diff --git a/tests/xilinx_ug901/top_mux.ys b/tests/xilinx_ug901/top_mux.ys
deleted file mode 100644
index 0245f3bbc..000000000
--- a/tests/xilinx_ug901/top_mux.ys
+++ /dev/null
@@ -1,13 +0,0 @@
-read_verilog top_mux.v
-hierarchy -top mux4
-proc
-flatten
-equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check
-design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
-
-cd mux4
-#Vivado synthesizes 2 LUT.
-stat
-select -assert-count 2 t:LUT6
-
-select -assert-none t:LUT6 %% t:* %D
diff --git a/tests/xilinx_ug901/tristates_1.v b/tests/xilinx_ug901/tristates_1.v
deleted file mode 100644
index 0038a9989..000000000
--- a/tests/xilinx_ug901/tristates_1.v
+++ /dev/null
@@ -1,17 +0,0 @@
-// Tristate Description Using Combinatorial Always Block
-// File: tristates_1.v
-//
-module tristates_1 (T, I, O);
-input  T, I;
-output O;
-reg    O;
-
-always @(T or I)
-begin
-  if (~T)
-    O = I;
-  else
-   O = 1'bZ;
-end
-
-endmodule
diff --git a/tests/xilinx_ug901/tristates_1.ys b/tests/xilinx_ug901/tristates_1.ys
deleted file mode 100644
index 7c13dc227..000000000
--- a/tests/xilinx_ug901/tristates_1.ys
+++ /dev/null
@@ -1,13 +0,0 @@
-read_verilog tristates_1.v
-hierarchy -top tristates_1
-proc
-tribuf
-flatten
-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 tristates_1 # Constrain all select calls below inside the top module
-#Vivado synthesizes 3 IBUF, 1 OBUFT.
-select -assert-count 1 t:LUT1
-select -assert-count 1 t:$_TBUF_
-select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D
diff --git a/tests/xilinx_ug901/tristates_2.v b/tests/xilinx_ug901/tristates_2.v
deleted file mode 100644
index 0c70a1257..000000000
--- a/tests/xilinx_ug901/tristates_2.v
+++ /dev/null
@@ -1,10 +0,0 @@
-// Tristate Description Using Concurrent Assignment
-// File: tristates_2.v
-//
-module tristates_2 (T, I, O);
-input  T, I;
-output O;
-
-assign O = (~T) ? I: 1'bZ;
-
-endmodule
diff --git a/tests/xilinx_ug901/tristates_2.ys b/tests/xilinx_ug901/tristates_2.ys
deleted file mode 100644
index ba2e1d855..000000000
--- a/tests/xilinx_ug901/tristates_2.ys
+++ /dev/null
@@ -1,13 +0,0 @@
-read_verilog tristates_2.v
-hierarchy -top tristates_2
-proc
-tribuf
-flatten
-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 tristates_2 # Constrain all select calls below inside the top module
-#Vivado synthesizes 3 IBUF, 1 OBUFT.
-select -assert-count 1 t:LUT1
-select -assert-count 1 t:$_TBUF_
-select -assert-none t:LUT1 t:$_TBUF_ %% t:* %D
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v b/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v
deleted file mode 100644
index f5e843dc9..000000000
--- a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.v
+++ /dev/null
@@ -1,78 +0,0 @@
-//  Xilinx UltraRAM Single Port No Change Mode.  This code implements
-//  a parameterizable UltraRAM block in No Change mode. The behavior of this RAM is
-//  when data is written, the output of RAM is unchanged. Only when write is
-//  inactive data corresponding to the address is presented on the output port.
-//
-module xilinx_ultraram_single_port_no_change #(
-//Default parameters were changed because of slow test
-  //parameter AWIDTH = 12,  // Address Width
-  //parameter DWIDTH = 72,  // Data Width
-  //parameter NBPIPE = 3    // Number of pipeline Registers
-  parameter AWIDTH = 8,  // Address Width
-  parameter DWIDTH = 8,  // Data Width
-  parameter NBPIPE = 3    // Number of pipeline Registers
- ) (
-    input clk,                    // Clock
-    input rst,                    // Reset
-    input we,                     // Write Enable
-    input regce,                  // Output Register Enable
-    input mem_en,                 // Memory Enable
-    input [DWIDTH-1:0] din,       // Data Input
-    input [AWIDTH-1:0] addr,      // Address Input
-    output reg [DWIDTH-1:0] dout  // Data Output
-   );
-
-(* ram_style = "ultra" *)
-reg [DWIDTH-1:0] mem[(1<<AWIDTH)-1:0];        // Memory Declaration
-reg [DWIDTH-1:0] memreg;
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0];    // Pipelines for memory
-reg mem_en_pipe_reg[NBPIPE:0];                // Pipelines for memory enable
-
-integer          i;
-
-// RAM : Read has one latency, Write has one latency as well.
-always @ (posedge clk)
-begin
- if(mem_en)
-  begin
-  if(we)
-    mem[addr] <= din;
-  else
-   memreg <= mem[addr];
-  end
-end
-// The enable of the RAM goes through a pipeline to produce a
-// series of pipelined enable signals required to control the data
-// pipeline.
-always @ (posedge clk)
-begin
-mem_en_pipe_reg[0] <= mem_en;
- for (i=0; i<NBPIPE; i=i+1)
-  mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];
-end
-
-// RAM output data goes through a pipeline.
-always @ (posedge clk)
-begin
- if (mem_en_pipe_reg[0])
-  mem_pipe_reg[0] <= memreg;
-end
-
-always @ (posedge clk)
-begin
- for (i = 0; i < NBPIPE-1; i = i+1)
-  if (mem_en_pipe_reg[i+1])
-    mem_pipe_reg[i+1] <= mem_pipe_reg[i];
-end
-
-// Final output register gives user the option to add a reset and
-// an additional enable signal just for the data ouptut
-always @ (posedge clk)
-begin
- if (rst)
-  dout <= 0;
- else if (mem_en_pipe_reg[NBPIPE] && regce)
-  dout <= mem_pipe_reg[NBPIPE-1];
-end
-endmodule
-
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys b/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys
deleted file mode 100644
index df3126e67..000000000
--- a/tests/xilinx_ug901/xilinx_ultraram_single_port_no_change.ys
+++ /dev/null
@@ -1,25 +0,0 @@
-read_verilog xilinx_ultraram_single_port_no_change.v
-hierarchy -top xilinx_ultraram_single_port_no_change
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd xilinx_ultraram_single_port_no_change
-stat
-#Vivado synthesizes 1 RAMB36E1, 28 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 53 t:FDRE
-select -assert-count 1 t:LUT1
-select -assert-count 9 t:LUT2
-select -assert-count 11 t:LUT3
-select -assert-count 16 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v b/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v
deleted file mode 100644
index d36c38fe1..000000000
--- a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.v
+++ /dev/null
@@ -1,78 +0,0 @@
-//  Xilinx UltraRAM Single Port Read First Mode.  This code implements
-//  a parameterizable UltraRAM block in read first mode. The behavior of this RAM is
-//  when data is written, the old memory contents at the write address are
-//  presented on the output port.
-//
-module xilinx_ultraram_single_port_read_first #(
-
-//Default parameters were changed because of slow test
-  //parameter AWIDTH = 12,  // Address Width
-  //parameter DWIDTH = 72,  // Data Width
-  //parameter NBPIPE = 3    // Number of pipeline Registers
-  parameter AWIDTH = 8,  // Address Width
-  parameter DWIDTH = 8,  // Data Width
-  parameter NBPIPE = 3    // Number of pipeline Registers
- ) (
-    input clk,                    // Clock
-    input rst,                    // Reset
-    input we,                     // Write Enable
-    input regce,                  // Output Register Enable
-    input mem_en,                 // Memory Enable
-    input [DWIDTH-1:0] din,       // Data Input
-    input [AWIDTH-1:0] addr,      // Address Input
-    output reg [DWIDTH-1:0] dout  // Data Output
-   );
-
-(* ram_style = "ultra" *)
-reg [DWIDTH-1:0] mem[(1<<AWIDTH)-1:0];        // Memory Declaration
-reg [DWIDTH-1:0] memreg;
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0];    // Pipelines for memory
-reg mem_en_pipe_reg[NBPIPE:0];                // Pipelines for memory enable
-
-integer          i;
-
-// RAM : Both READ and WRITE have a latency of one
-always @ (posedge clk)
-begin
- if(mem_en)
-  begin
-   if(we)
-    mem[addr] <= din;
-   memreg <= mem[addr];
-  end
-end
-
-// The enable of the RAM goes through a pipeline to produce a
-// series of pipelined enable signals required to control the data
-// pipeline.
-always @ (posedge clk)
-begin
- mem_en_pipe_reg[0] <= mem_en;
- for (i=0; i<NBPIPE; i=i+1)
-   mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];
-end
-
-// RAM output data goes through a pipeline.
-always @ (posedge clk)
-begin
- if (mem_en_pipe_reg[0])
-  mem_pipe_reg[0] <= memreg;
-end
-
-always @ (posedge clk)
-begin
- for (i = 0; i < NBPIPE-1; i = i+1)
-  if (mem_en_pipe_reg[i+1])
-   mem_pipe_reg[i+1] <= mem_pipe_reg[i];
-end
-
-// Final output register gives user the option to add a reset and
-// an additional enable signal just for the data ouptut
-always @ (posedge clk)
-begin
- if (rst)
-   dout <= 0;
- else if (mem_en_pipe_reg[NBPIPE] && regce)
-   dout <= mem_pipe_reg[NBPIPE-1];
-end
-endmodule
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys b/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys
deleted file mode 100644
index 4907d042d..000000000
--- a/tests/xilinx_ug901/xilinx_ultraram_single_port_read_first.ys
+++ /dev/null
@@ -1,24 +0,0 @@
-read_verilog xilinx_ultraram_single_port_read_first.v
-hierarchy -top xilinx_ultraram_single_port_read_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd xilinx_ultraram_single_port_read_first
-#Vivado synthesizes 1 RAMB18E1, 28 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 53 t:FDRE
-select -assert-count 1 t:LUT1
-select -assert-count 8 t:LUT2
-select -assert-count 11 t:LUT3
-select -assert-count 16 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT1 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v b/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v
deleted file mode 100644
index 7985d3d4a..000000000
--- a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.v
+++ /dev/null
@@ -1,82 +0,0 @@
-//  Xilinx UltraRAM Single Port Write First Mode.  This code implements
-//  a parameterizable UltraRAM block in write first mode. The behavior of this RAM is
-//  when data is written, the new memory contents at the write address are
-//  presented on the output port.
-//
-module xilinx_ultraram_single_port_write_first #(
-
-//Default parameters were changed because of slow test
-  //parameter AWIDTH = 12,  // Address Width
-  //parameter DWIDTH = 72,  // Data Width
-  //parameter NBPIPE = 3    // Number of pipeline Registers
-  parameter AWIDTH = 8,  // Address Width
-  parameter DWIDTH = 8,  // Data Width
-  parameter NBPIPE = 3    // Number of pipeline Registers
- ) (
-    input clk,                    // Clock
-    input rst,                    // Reset
-    input we,                     // Write Enable
-    input regce,                  // Output Register Enable
-    input mem_en,                 // Memory Enable
-    input [DWIDTH-1:0] din,       // Data Input
-    input [AWIDTH-1:0] addr,      // Address Input
-    output reg [DWIDTH-1:0] dout  // Data Output
-   );
-
-(* ram_style = "ultra" *)
-reg [DWIDTH-1:0] mem[(1<<AWIDTH)-1:0];        // Memory Declaration
-reg [DWIDTH-1:0] memreg;
-reg [DWIDTH-1:0] mem_pipe_reg[NBPIPE-1:0];    // Pipelines for memory
-reg mem_en_pipe_reg[NBPIPE:0];                // Pipelines for memory enable
-
-integer          i;
-
-// RAM : Both READ and WRITE have a latency of one
-always @ (posedge clk)
-begin
- if(mem_en)
-  begin
-    if(we)
-    begin
-      mem[addr] <= din;
-     memreg <= din;
-   end
-    else
-     memreg <= mem[addr];
-  end
-end
-
-// The enable of the RAM goes through a pipeline to produce a
-// series of pipelined enable signals required to control the data
-// pipeline.
-always @ (posedge clk)
-begin
- mem_en_pipe_reg[0] <= mem_en;
- for (i=0; i<NBPIPE; i=i+1)
-   mem_en_pipe_reg[i+1] <= mem_en_pipe_reg[i];
-end
-
-// RAM output data goes through a pipeline.
-always @ (posedge clk)
-begin
- if (mem_en_pipe_reg[0])
-  mem_pipe_reg[0] <= memreg;
-end
-
-always @ (posedge clk)
-begin
-  for (i = 0; i < NBPIPE-1; i = i+1)
-   if (mem_en_pipe_reg[i+1])
-     mem_pipe_reg[i+1] <= mem_pipe_reg[i];
-end
-
-// Final output register gives user the option to add a reset and
-// an additional enable signal just for the data ouptut
-always @ (posedge clk)
-begin
- if (rst)
-  dout <= 0;
- else if (mem_en_pipe_reg[NBPIPE] && regce)
-  dout <= mem_pipe_reg[NBPIPE-1];
-end
-endmodule
diff --git a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys b/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys
deleted file mode 100644
index 9ca6b4d89..000000000
--- a/tests/xilinx_ug901/xilinx_ultraram_single_port_write_first.ys
+++ /dev/null
@@ -1,24 +0,0 @@
-read_verilog xilinx_ultraram_single_port_write_first.v
-hierarchy -top xilinx_ultraram_single_port_write_first
-proc
-memory -nomap
-equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx
-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
-
-design -load postopt
-cd xilinx_ultraram_single_port_write_first
-#Vivado synthesizes 1 RAMB18E1, 28 FDRE.
-select -assert-count 1 t:BUFG
-select -assert-count 44 t:FDRE
-select -assert-count 8 t:LUT5
-select -assert-count 8 t:LUT2
-select -assert-count 3 t:LUT3
-select -assert-count 16 t:RAM128X1D
-
-select -assert-none t:BUFG t:FDRE t:LUT5 t:LUT2 t:LUT3 t:RAM128X1D %% t:* %D
-- 
2.30.2