From 19bc429482418aa42861ca0f195d86bc9577e320 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 4 Dec 2019 21:36:41 -0800
Subject: abc9_map.v to transform INIT=1 to INIT=0

---
 tests/arch/xilinx/abc9_map.ys | 91 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 91 insertions(+)
 create mode 100644 tests/arch/xilinx/abc9_map.ys

(limited to 'tests/arch')

diff --git a/tests/arch/xilinx/abc9_map.ys b/tests/arch/xilinx/abc9_map.ys
new file mode 100644
index 000000000..6823589f1
--- /dev/null
+++ b/tests/arch/xilinx/abc9_map.ys
@@ -0,0 +1,91 @@
+read_verilog <<EOT
+module top(input C, CE, D, R, output [1:0] Q);
+FDRE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[0]));
+FDRE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDSE
+select -assert-count 1 t:FDSE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, S, output [1:0] Q);
+FDSE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[0]));
+FDSE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDRE
+select -assert-count 1 t:FDRE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, PRE, output [1:0] Q);
+FDPE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[0]));
+FDPE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDCE
+select -assert-count 1 t:FDCE_1
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
+
+design -reset
+read_verilog <<EOT
+module top(input C, CE, D, CLR, output [1:0] Q);
+FDCE   #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[0]));
+FDCE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[1]));
+endmodule
+EOT
+design -save gold
+
+techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_unmap.v
+select -assert-count 1 t:FDPE
+techmap -autoproc -map +/xilinx/cells_sim.v
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+techmap -autoproc -map +/xilinx/cells_sim.v
+clk2fflogic
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
-- 
cgit v1.2.3


From 0c4be94a02a70de495343258ecda19eb20b3616b Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Mon, 30 Dec 2019 20:13:25 -0800
Subject: Add -D DFF_MODE to abc9_map test

---
 tests/arch/xilinx/abc9_map.ys | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'tests/arch')

diff --git a/tests/arch/xilinx/abc9_map.ys b/tests/arch/xilinx/abc9_map.ys
index 6823589f1..4a7b9384a 100644
--- a/tests/arch/xilinx/abc9_map.ys
+++ b/tests/arch/xilinx/abc9_map.ys
@@ -6,7 +6,7 @@ endmodule
 EOT
 design -save gold
 
-techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
 techmap -map +/xilinx/abc9_unmap.v
 select -assert-count 1 t:FDSE
 select -assert-count 1 t:FDSE_1
@@ -29,7 +29,7 @@ endmodule
 EOT
 design -save gold
 
-techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
 techmap -map +/xilinx/abc9_unmap.v
 select -assert-count 1 t:FDRE
 select -assert-count 1 t:FDRE_1
@@ -52,7 +52,7 @@ endmodule
 EOT
 design -save gold
 
-techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
 techmap -map +/xilinx/abc9_unmap.v
 select -assert-count 1 t:FDCE
 select -assert-count 1 t:FDCE_1
@@ -76,7 +76,7 @@ endmodule
 EOT
 design -save gold
 
-techmap -map +/xilinx/abc9_map.v -max_iter 1
+techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
 techmap -map +/xilinx/abc9_unmap.v
 select -assert-count 1 t:FDPE
 techmap -autoproc -map +/xilinx/cells_sim.v
-- 
cgit v1.2.3


From ccc0a740d254e6895b49037681bc484d6572342d Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Tue, 31 Dec 2019 16:16:05 -0800
Subject: Add some abc9 dff tests

---
 tests/arch/xilinx/abc9_dff.ys | 55 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 tests/arch/xilinx/abc9_dff.ys

(limited to 'tests/arch')

diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys
new file mode 100644
index 000000000..6611b4f18
--- /dev/null
+++ b/tests/arch/xilinx/abc9_dff.ys
@@ -0,0 +1,55 @@
+read_verilog <<EOT
+module top(input C, D, output [3:0] Q);
+FDRE   fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
+FDSE   fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
+FDCE   fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
+FDPE   fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
+endmodule
+EOT
+equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
+design -load postopt
+select -assert-none t:FD*
+
+
+design -reset
+read_verilog <<EOT
+module top(input C, D, output [3:0] Q);
+FDRE   fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
+FDSE   fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
+FDCE   fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
+FDPE   fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
+endmodule
+EOT
+equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
+design -load postopt
+select -assert-none t:FD*
+
+
+design -reset
+read_verilog <<EOT
+module top(input C, D, output [3:0] Q);
+FDRE_1 fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
+FDSE_1 fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
+FDCE_1 fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
+FDPE_1 fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
+endmodule
+EOT
+
+equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
+design -load postopt
+select -assert-none t:FD*
+
+
+design -reset
+read_verilog <<EOT
+module top(input C, D, output [3:0] Q);
+FDRE_1 fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
+FDSE_1 fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
+FDCE_1 fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
+FDPE_1 fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
+endmodule
+EOT
+
+equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
+design -load postopt
+select -assert-none t:FD*
-- 
cgit v1.2.3


From 6e866030c286d70f6ccff805e58b1fdd9a1a322b Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 2 Jan 2020 14:38:59 -0800
Subject: Combine tests to check multiple clock domains

---
 tests/arch/xilinx/abc9_dff.ys | 43 ++++++++++---------------------------------
 1 file changed, 10 insertions(+), 33 deletions(-)

(limited to 'tests/arch')

diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys
index 6611b4f18..b457cefce 100644
--- a/tests/arch/xilinx/abc9_dff.ys
+++ b/tests/arch/xilinx/abc9_dff.ys
@@ -1,55 +1,32 @@
 read_verilog <<EOT
-module top(input C, D, output [3:0] Q);
+module top(input C, D, output [7:0] Q);
 FDRE   fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
 FDSE   fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
 FDCE   fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
 FDPE   fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
+FDRE_1 fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
+FDSE_1 fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
+FDCE_1 fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
+FDPE_1 fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
 endmodule
 EOT
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-none t:FD*
 
-
 design -reset
 read_verilog <<EOT
-module top(input C, D, output [3:0] Q);
+module top(input C, D, output [7:0] Q);
 FDRE   fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
 FDSE   fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
 FDCE   fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
 FDPE   fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
+FDRE_1 fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
+FDSE_1 fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
+FDCE_1 fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
+FDPE_1 fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
 endmodule
 EOT
 equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
 design -load postopt
 select -assert-none t:FD*
-
-
-design -reset
-read_verilog <<EOT
-module top(input C, D, output [3:0] Q);
-FDRE_1 fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
-FDSE_1 fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
-FDCE_1 fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
-FDPE_1 fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
-endmodule
-EOT
-
-equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
-design -load postopt
-select -assert-none t:FD*
-
-
-design -reset
-read_verilog <<EOT
-module top(input C, D, output [3:0] Q);
-FDRE_1 fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
-FDSE_1 fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
-FDCE_1 fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
-FDPE_1 fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
-endmodule
-EOT
-
-equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
-design -load postopt
-select -assert-none t:FD*
-- 
cgit v1.2.3