aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/arch/xilinx/abc9_dff.ys55
-rw-r--r--tests/arch/xilinx/abc9_map.ys91
-rw-r--r--tests/simple_abc9/abc9.v27
-rwxr-xr-xtests/simple_abc9/run-test.sh6
-rw-r--r--tests/various/abc9.v7
-rw-r--r--tests/various/abc9.ys16
6 files changed, 200 insertions, 2 deletions
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*
diff --git a/tests/arch/xilinx/abc9_map.ys b/tests/arch/xilinx/abc9_map.ys
new file mode 100644
index 000000000..4a7b9384a
--- /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 -D DFF_MODE
+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 -D DFF_MODE
+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 -D DFF_MODE
+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 -D DFF_MODE
+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
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
index de60619d1..8afd0ce96 100644
--- a/tests/simple_abc9/abc9.v
+++ b/tests/simple_abc9/abc9.v
@@ -264,3 +264,30 @@ always @*
if (en)
q <= d;
endmodule
+
+module abc9_test031(input clk1, clk2, d, output reg q1, q2);
+always @(posedge clk1) q1 <= d;
+always @(negedge clk2) q2 <= q1;
+endmodule
+
+module abc9_test032(input clk, d, r, output reg q);
+always @(posedge clk or posedge r)
+ if (r) q <= 1'b0;
+ else q <= d;
+endmodule
+
+module abc9_test033(input clk, d, r, output reg q);
+always @(negedge clk or posedge r)
+ if (r) q <= 1'b1;
+ else q <= d;
+endmodule
+
+module abc9_test034(input clk, d, output reg q1, q2);
+always @(posedge clk) q1 <= d;
+always @(posedge clk) q2 <= q1;
+endmodule
+
+module abc9_test035(input clk, d, output reg [1:0] q);
+always @(posedge clk) q[0] <= d;
+always @(negedge clk) q[1] <= q[0];
+endmodule
diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh
index 0d4262005..bc921daa9 100755
--- a/tests/simple_abc9/run-test.sh
+++ b/tests/simple_abc9/run-test.sh
@@ -20,10 +20,12 @@ fi
cp ../simple/*.v .
cp ../simple/*.sv .
DOLLAR='?'
-exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p '\
+exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p '\
hierarchy; \
synth -run coarse; \
opt -full; \
- techmap; abc9 -lut 4 -box ../abc.box; \
+ techmap; \
+ abc9 -lut 4 -box ../abc.box; \
+ clean; \
check -assert; \
select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"
diff --git a/tests/various/abc9.v b/tests/various/abc9.v
index 30ebd4e26..f0b3f6837 100644
--- a/tests/various/abc9.v
+++ b/tests/various/abc9.v
@@ -9,3 +9,10 @@ wire w;
unknown u(~i, w);
unknown2 u2(w, o);
endmodule
+
+module abc9_test032(input clk, d, r, output reg q);
+initial q = 1'b0;
+always @(negedge clk or negedge r)
+ if (!r) q <= 1'b0;
+ else q <= d;
+endmodule
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
index 5c9a4075d..81d0afd1b 100644
--- a/tests/various/abc9.ys
+++ b/tests/various/abc9.ys
@@ -22,3 +22,19 @@ abc9 -lut 4
select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
select -assert-count 1 t:unknown
select -assert-none t:$lut t:unknown %% t: %D
+
+design -load read
+hierarchy -top abc9_test032
+proc
+clk2fflogic
+design -save gold
+
+abc9 -lut 4
+check
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 10 -verify -prove-asserts -show-ports miter
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-24 22:04:26 +0000