aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/arch/efinix/mux.ys2
-rw-r--r--tests/arch/ice40/bug1597.ys72
-rw-r--r--tests/arch/ice40/ice40_opt.ys57
-rw-r--r--tests/arch/xilinx/tribuf.sh5
-rw-r--r--tests/sat/initval.ys11
-rw-r--r--tests/simple_abc9/abc9.v18
-rwxr-xr-xtests/simple_abc9/run-test.sh3
-rw-r--r--tests/techmap/abc9.ys29
-rw-r--r--tests/various/abc9.ys15
-rw-r--r--tests/various/help.ys2
10 files changed, 188 insertions, 26 deletions
diff --git a/tests/arch/efinix/mux.ys b/tests/arch/efinix/mux.ys
index b46f641e1..a5ab80d8b 100644
--- a/tests/arch/efinix/mux.ys
+++ b/tests/arch/efinix/mux.ys
@@ -36,6 +36,6 @@ proc
equiv_opt -assert -map +/efinix/cells_sim.v synth_efinix # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mux16 # Constrain all select calls below inside the top module
-select -assert-count 12 t:EFX_LUT4
+select -assert-max 12 t:EFX_LUT4
select -assert-none t:EFX_LUT4 %% t:* %D
diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys
new file mode 100644
index 000000000..b7983cfa4
--- /dev/null
+++ b/tests/arch/ice40/bug1597.ys
@@ -0,0 +1,72 @@
+read_verilog <<EOT
+module top (
+ input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5,
+ PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25,
+ output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18,
+ PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24,
+);
+ assign USBPU = 0;
+
+ wire[5:0] parOut;
+ wire[5:0] chrg;
+
+ assign PIN_14 = parOut[0];
+ assign PIN_15 = parOut[1];
+ assign PIN_16 = parOut[2];
+ assign PIN_17 = parOut[3];
+ assign PIN_18 = parOut[4];
+ assign PIN_19 = parOut[5];
+ assign chrg[0] = PIN_3;
+ assign chrg[1] = PIN_4;
+ assign chrg[2] = PIN_5;
+ assign chrg[3] = PIN_6;
+ assign chrg[4] = PIN_7;
+ assign chrg[5] = PIN_8;
+
+ SSCounter6o sc6(PIN_1, CLK, PIN_2, PIN_9, chrg, parOut);
+
+endmodule
+
+module SSCounter6 (input wire rst, clk, adv, jmp, input wire [5:0] in, output reg[5:0] out);
+ always @(posedge clk, posedge rst)
+ if (rst) out <= 0;
+ else if (adv || jmp) out <= jmp ? in : out + 1;
+endmodule
+
+// Optimized 6 bit counter, it should takes 7 cells.
+/* b[5:1] /* b[0]
+1010101010101010 in 1010101010101010 in
+1100110011001100 jmp 1100110011001100 jmp
+1111000011110000 loop 1111000011110000 loop
+1111111100000000 carry 1111111100000000 -
+---------------------- ----------------------
+1000101110111000 out 1000101110001011 out
+ 8 B B 8 8 B 8 B
+*/
+module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output wire[5:0] out);
+ wire[4:0] co;
+ wire[5:0] lo;
+ wire ien;
+ SB_LUT4 #(.LUT_INIT(16'hFFF0)) lien (ien, 0, 0, adv, jmp);
+ SB_CARRY c0 (co[0], jmp, out[0], 1),
+ c1 (co[1], jmp, out[1], co[0]),
+ c2 (co[2], jmp, out[2], co[1]),
+ c3 (co[3], jmp, out[3], co[2]),
+ c4 (co[4], jmp, out[4], co[3]);
+ SB_DFFER d0 (out[0], clk, ien, rst, lo[0]),
+ d1 (out[1], clk, ien, rst, lo[1]),
+ d2 (out[2], clk, ien, rst, lo[2]),
+ d3 (out[3], clk, ien, rst, lo[3]),
+ d4 (out[4], clk, ien, rst, lo[4]),
+ d5 (out[5], clk, ien, rst, lo[5]);
+ SB_LUT4 #(.LUT_INIT(16'h8B8B)) l0 (lo[0], in[0], jmp, out[0], 0);
+ SB_LUT4 #(.LUT_INIT(16'h8BB8)) l1 (lo[1], in[1], jmp, out[1], co[0]);
+ SB_LUT4 #(.LUT_INIT(16'h8BB8)) l2 (lo[2], in[2], jmp, out[2], co[1]);
+ SB_LUT4 #(.LUT_INIT(16'h8BB8)) l3 (lo[3], in[3], jmp, out[3], co[2]);
+ SB_LUT4 #(.LUT_INIT(16'h8BB8)) l4 (lo[4], in[4], jmp, out[4], co[3]);
+ SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]);
+endmodule
+EOT
+hierarchy -top top
+flatten
+equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40
diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys
index 5186d4800..71b68431e 100644
--- a/tests/arch/ice40/ice40_opt.ys
+++ b/tests/arch/ice40/ice40_opt.ys
@@ -1,24 +1,4 @@
read_verilog -icells -formal <<EOT
-module \$__ICE40_CARRY_WRAPPER (output CO, O, input A, B, CI, I0, I3);
- parameter LUT = 0;
- SB_CARRY carry (
- .I0(A),
- .I1(B),
- .CI(CI),
- .CO(CO)
- );
- \$lut #(
- .WIDTH(4),
- .LUT(LUT)
- ) lut (
- .A({I0,A,B,I3}),
- .Y(O)
- );
-endmodule
-EOT
-design -stash unmap
-
-read_verilog -icells -formal <<EOT
module top(input CI, I0, output [1:0] CO, output O);
wire A = 1'b0, B = 1'b0;
\$__ICE40_CARRY_WRAPPER #(
@@ -26,13 +6,14 @@ module top(input CI, I0, output [1:0] CO, output O);
// A[1]: 1100 1100 1100 1100
// A[2]: 1111 0000 1111 0000
// A[3]: 1111 1111 0000 0000
- .LUT(~16'b 0110_1001_1001_0110)
+ .LUT(~16'b 0110_1001_1001_0110),
+ .I3_IS_CI(1'b1)
) u0 (
.A(A),
.B(B),
.CI(CI),
.I0(I0),
- .I3(CI),
+ .I3(1'bx),
.CO(CO[0]),
.O(O)
);
@@ -40,7 +21,7 @@ module top(input CI, I0, output [1:0] CO, output O);
endmodule
EOT
-equiv_opt -assert -map %unmap -map +/ice40/cells_sim.v ice40_opt
+equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt
design -load postopt
select -assert-count 1 t:*
select -assert-count 1 t:$lut
@@ -105,3 +86,33 @@ select -assert-count 1 t:SB_LUT4
select -assert-count 1 t:SB_CARRY
select -assert-count 1 t:SB_CARRY a:keep %i
select -assert-count 1 t:SB_CARRY c:carry %i
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input I3, I2, I1, I0, output O, O2);
+ SB_LUT4 #(
+ .LUT_INIT(8'b 1001_0110)
+ ) u0 (
+ .I0(I0),
+ .I1(I1),
+ .I2(I2),
+ .I3(),
+ .O(O)
+ );
+ wire CO;
+ \$__ICE40_CARRY_WRAPPER #(
+ .LUT(~8'b 1001_0110),
+ .I3_IS_CI(1'b0)
+ ) u1 (
+ .A(1'b0),
+ .B(1'b0),
+ .CI(1'b0),
+ .I0(),
+ .I3(),
+ .CO(CO),
+ .O(O2)
+ );
+endmodule
+EOT
+ice40_opt
diff --git a/tests/arch/xilinx/tribuf.sh b/tests/arch/xilinx/tribuf.sh
new file mode 100644
index 000000000..636aed12a
--- /dev/null
+++ b/tests/arch/xilinx/tribuf.sh
@@ -0,0 +1,5 @@
+! ../../../yosys ../common/tribuf.v -qp "synth_xilinx"
+../../../yosys ../common/tribuf.v -qp "synth_xilinx -iopad; \
+select -assert-count 2 t:IBUF; \
+select -assert-count 1 t:INV; \
+select -assert-count 1 t:OBUFT"
diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys
index 2079d2f34..1436724b0 100644
--- a/tests/sat/initval.ys
+++ b/tests/sat/initval.ys
@@ -2,3 +2,14 @@ read_verilog -sv initval.v
proc;;
sat -seq 10 -prove-asserts
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, output [1:0] o);
+(* init = 2'bx0 *)
+wire [1:0] o;
+assign o[1] = o[0];
+$_DFF_P_ dff (.C(clk), .D(i), .Q(o[0]));
+endmodule
+EOT
+sat -seq 1
diff --git a/tests/simple_abc9/abc9.v b/tests/simple_abc9/abc9.v
index 8afd0ce96..e5837d480 100644
--- a/tests/simple_abc9/abc9.v
+++ b/tests/simple_abc9/abc9.v
@@ -213,7 +213,7 @@ module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encode
input rst;
endmodule
-(* abc_box_id=1 *)
+(* abc9_box_id=1, whitebox *)
module MUXF8(input I0, I1, S, output O);
endmodule
@@ -291,3 +291,19 @@ 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
+
+module abc9_test036(input A, B, S, output [1:0] O);
+ (* keep *)
+ MUXF8 m (
+ .I0(I0),
+ .I1(I1),
+ .O(O[0]),
+ .S(S)
+ );
+ MUXF8 m2 (
+ .I0(I0),
+ .I1(I1),
+ .O(O[1]),
+ .S(S)
+ );
+endmodule
diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh
index bc921daa9..32d7a80ca 100755
--- a/tests/simple_abc9/run-test.sh
+++ b/tests/simple_abc9/run-test.sh
@@ -28,4 +28,5 @@ exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p
abc9 -lut 4 -box ../abc.box; \
clean; \
check -assert; \
- select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'"
+ select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%; \
+ setattr -mod -unset whitebox'"
diff --git a/tests/techmap/abc9.ys b/tests/techmap/abc9.ys
index 62b5dfef6..2140dde26 100644
--- a/tests/techmap/abc9.ys
+++ b/tests/techmap/abc9.ys
@@ -39,6 +39,35 @@ design -load gold
scratchpad -copy abc9.script.flow3 abc9.script
abc9 -lut 4
+design -reset
+read_verilog <<EOT
+module top(input a, b, output o);
+(* keep *) wire w = a & b;
+assign o = ~w;
+endmodule
+EOT
+
+simplemap
+equiv_opt -assert abc9 -lut 4
+design -load postopt
+select -assert-count 2 t:$lut
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input a, b, output o);
+wire w;
+(* keep *) $_AND_ gate (.Y(w), .A(a), .B(b));
+assign o = ~w;
+endmodule
+EOT
+
+simplemap
+equiv_opt -assert abc9 -lut 4
+design -load postopt
+select -assert-count 1 t:$lut
+select -assert-count 1 t:$_AND_
+
design -reset
read_verilog -icells <<EOT
diff --git a/tests/various/abc9.ys b/tests/various/abc9.ys
index 81d0afd1b..0c7695089 100644
--- a/tests/various/abc9.ys
+++ b/tests/various/abc9.ys
@@ -14,6 +14,7 @@ design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
+
design -load read
hierarchy -top abc9_test028
proc
@@ -23,6 +24,7 @@ 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
@@ -38,3 +40,16 @@ design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -seq 10 -verify -prove-asserts -show-ports miter
+
+
+design -reset
+read_verilog -icells <<EOT
+module abc9_test036(input clk, d, output q);
+(* keep *) reg w;
+$__ABC9_FF_ ff(.D(d), .Q(w));
+wire \ff.clock = clk;
+wire \ff.init = 1'b0;
+assign q = w;
+endmodule
+EOT
+abc9 -lut 4 -dff
diff --git a/tests/various/help.ys b/tests/various/help.ys
new file mode 100644
index 000000000..9283ce8f1
--- /dev/null
+++ b/tests/various/help.ys
@@ -0,0 +1,2 @@
+help -all
+help -celltypes
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 06:25:28 +0000