aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/arch/anlogic/fsm.ys5
-rw-r--r--tests/arch/efinix/fsm.ys5
-rw-r--r--tests/opt/opt_expr_alu.ys63
-rw-r--r--tests/opt/opt_expr_xor.ys52
-rw-r--r--tests/opt/opt_merge_init.ys28
-rw-r--r--tests/opt/opt_merge_keep.ys64
-rw-r--r--tests/simple/dynslice.v12
-rw-r--r--tests/techmap/cmp2lcu.ys52
-rw-r--r--tests/techmap/iopadmap.ys10
9 files changed, 283 insertions, 8 deletions
diff --git a/tests/arch/anlogic/fsm.ys b/tests/arch/anlogic/fsm.ys
index 0bcc4e011..eb94177ad 100644
--- a/tests/arch/anlogic/fsm.ys
+++ b/tests/arch/anlogic/fsm.ys
@@ -10,9 +10,6 @@ sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
-select -assert-count 1 t:AL_MAP_LUT2
-select -assert-count 5 t:AL_MAP_LUT5
-select -assert-count 1 t:AL_MAP_LUT6
select -assert-count 6 t:AL_MAP_SEQ
-select -assert-none t:AL_MAP_LUT2 t:AL_MAP_LUT5 t:AL_MAP_LUT6 t:AL_MAP_SEQ %% t:* %D
+select -assert-none t:AL_MAP_LUT* t:AL_MAP_SEQ %% t:* %D
diff --git a/tests/arch/efinix/fsm.ys b/tests/arch/efinix/fsm.ys
index a2db2ad98..aef720d46 100644
--- a/tests/arch/efinix/fsm.ys
+++ b/tests/arch/efinix/fsm.ys
@@ -10,7 +10,6 @@ sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd fsm # Constrain all select calls below inside the top module
-select -assert-count 1 t:EFX_GBUFCE
-select -assert-count 6 t:EFX_FF
-select -assert-count 15 t:EFX_LUT4
+select -assert-count 1 t:EFX_GBUFCE
+select -assert-count 6 t:EFX_FF
select -assert-none t:EFX_GBUFCE t:EFX_FF t:EFX_LUT4 %% t:* %D
diff --git a/tests/opt/opt_expr_alu.ys b/tests/opt/opt_expr_alu.ys
new file mode 100644
index 000000000..a3361ca43
--- /dev/null
+++ b/tests/opt/opt_expr_alu.ys
@@ -0,0 +1,63 @@
+read_verilog <<EOT
+module test(input a, output [1:0] y);
+assign y = {a,1'b0} + 1'b1;
+endmodule
+EOT
+
+alumacc
+equiv_opt opt_expr -fine
+design -load postopt
+select -assert-count 1 t:$pos
+select -assert-count none t:$pos t:* %D
+
+
+design -reset
+read_verilog <<EOT
+module test(input a, output [1:0] y);
+assign y = {a,1'b1} + 1'b1;
+endmodule
+EOT
+
+alumacc
+select -assert-count 1 t:$alu
+select -assert-count none t:$alu t:* %D
+
+
+design -reset
+read_verilog <<EOT
+module test(input a, output [1:0] y);
+assign y = {a,1'b1} - 1'b1;
+endmodule
+EOT
+
+equiv_opt opt_expr -fine
+design -load postopt
+select -assert-count 1 t:$pos
+select -assert-count none t:$pos t:* %D
+
+
+design -reset
+read_verilog <<EOT
+module test(input a, output [3:0] y);
+assign y = {a,3'b101} - 1'b1;
+endmodule
+EOT
+
+equiv_opt opt_expr -fine
+design -load postopt
+select -assert-count 1 t:$pos
+select -assert-count none t:$pos t:* %D
+
+
+design -reset
+read_verilog <<EOT
+module test(input a, output [3:0] y);
+assign y = {a,3'b101} - 1'b1;
+endmodule
+EOT
+
+alumacc
+equiv_opt opt_expr -fine
+design -load postopt
+select -assert-count 1 t:$pos
+select -assert-count none t:$pos t:* %D
diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys
new file mode 100644
index 000000000..21439fd53
--- /dev/null
+++ b/tests/opt/opt_expr_xor.ys
@@ -0,0 +1,52 @@
+read_verilog <<EOT
+module top(input a, output [3:0] y);
+assign y[0] = a^1'b0;
+assign y[1] = 1'b1^a;
+assign y[2] = a~^1'b0;
+assign y[3] = 1'b1^~a;
+endmodule
+EOT
+design -save read
+select -assert-count 2 t:$xor
+select -assert-count 2 t:$xnor
+
+equiv_opt opt_expr
+design -load postopt
+select -assert-none t:$xor
+select -assert-none t:$xnor
+select -assert-count 2 t:$not
+
+
+design -load read
+simplemap
+equiv_opt opt_expr
+design -load postopt
+select -assert-none t:$_XOR_
+select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
+select -assert-count 3 t:$_NOT_
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input a, output [1:0] y);
+$_XNOR_ u0(.A(a), .B(1'b0), .Y(y[0]));
+$_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1]));
+endmodule
+EOT
+select -assert-count 2 t:$_XNOR_
+equiv_opt opt_expr
+design -load postopt
+select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_
+select -assert-count 1 t:$_NOT_
+
+
+design -reset
+read_verilog <<EOT
+module top(input a, output [1:0] w, x, y, z);
+assign w = a^1'b0;
+assign x = a^1'b1;
+assign y = a~^1'b0;
+assign z = a~^1'b1;
+endmodule
+EOT
+equiv_opt opt_expr
diff --git a/tests/opt/opt_merge_init.ys b/tests/opt/opt_merge_init.ys
index a29c29df6..0176f09c7 100644
--- a/tests/opt/opt_merge_init.ys
+++ b/tests/opt/opt_merge_init.ys
@@ -20,6 +20,7 @@ endmodule
EOT
opt_merge
+select -assert-count 1 t:$dff
select -assert-count 1 a:init=1'0
@@ -46,4 +47,31 @@ endmodule
EOT
opt_merge
+select -assert-count 1 t:$dff
select -assert-count 1 a:init=2'bx1
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, (* init = 1'b0 *) output o, /* NB: no init here! */ output p);
+ \$dff #(
+ .CLK_POLARITY(1'h1),
+ .WIDTH(32'd1)
+ ) ffo (
+ .CLK(clk),
+ .D(i),
+ .Q(o)
+ );
+ \$dff #(
+ .CLK_POLARITY(1'h1),
+ .WIDTH(32'd1)
+ ) ffp (
+ .CLK(clk),
+ .D(i),
+ .Q(p)
+ );
+endmodule
+EOT
+
+opt_merge
+select -assert-count 2 t:$dff
diff --git a/tests/opt/opt_merge_keep.ys b/tests/opt/opt_merge_keep.ys
new file mode 100644
index 000000000..2a9202901
--- /dev/null
+++ b/tests/opt/opt_merge_keep.ys
@@ -0,0 +1,64 @@
+read_verilog -icells <<EOT
+module top(input clk, i, output o, p);
+ (* keep *)
+ \$_DFF_P_ ffo (
+ .C(clk),
+ .D(i),
+ .Q(o)
+ );
+ \$_DFF_P_ ffp (
+ .C(clk),
+ .D(i),
+ .Q(p)
+ );
+endmodule
+EOT
+
+opt_merge
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 1 a:keep
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, output o, p);
+ \$_DFF_P_ ffo (
+ .C(clk),
+ .D(i),
+ .Q(o)
+ );
+ (* keep *)
+ \$_DFF_P_ ffp (
+ .C(clk),
+ .D(i),
+ .Q(p)
+ );
+endmodule
+EOT
+
+opt_merge
+select -assert-count 1 t:$_DFF_P_
+select -assert-count 1 a:keep
+
+
+design -reset
+read_verilog -icells <<EOT
+module top(input clk, i, output o, p);
+ (* keep *)
+ \$_DFF_P_ ffo (
+ .C(clk),
+ .D(i),
+ .Q(o)
+ );
+ (* keep *)
+ \$_DFF_P_ ffp (
+ .C(clk),
+ .D(i),
+ .Q(p)
+ );
+endmodule
+EOT
+
+opt_merge
+select -assert-count 2 t:$_DFF_P_
+select -assert-count 2 a:keep
diff --git a/tests/simple/dynslice.v b/tests/simple/dynslice.v
new file mode 100644
index 000000000..7236ac3a5
--- /dev/null
+++ b/tests/simple/dynslice.v
@@ -0,0 +1,12 @@
+module dynslice (
+ input clk ,
+ input [9:0] ctrl ,
+ input [15:0] din ,
+ input [3:0] sel ,
+ output reg [127:0] dout
+);
+always @(posedge clk)
+begin
+ dout[ctrl*sel+:16] <= din ;
+end
+endmodule
diff --git a/tests/techmap/cmp2lcu.ys b/tests/techmap/cmp2lcu.ys
new file mode 100644
index 000000000..7c8a63692
--- /dev/null
+++ b/tests/techmap/cmp2lcu.ys
@@ -0,0 +1,52 @@
+read_verilog <<EOT
+module top(input [12:0] a, b, output gtu, gts, ltu, lts, geu, ges, leu, les);
+assign gtu = a > b;
+assign gts = $signed(a) > $signed(b);
+assign ltu = a < b;
+assign lts = $signed(a) < $signed(b);
+assign geu = a >= b;
+assign ges = $signed(a) >= $signed(b);
+assign leu = a <= b;
+assign les = $signed(a) <= $signed(b);
+endmodule
+EOT
+
+equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=6
+design -load postopt
+select -assert-count 8 t:$lcu r:WIDTH=5 %i
+select -assert-none t:$gt t:$ge t:$lt t:$le
+
+design -load preopt
+equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=4
+design -load postopt
+select -assert-count 8 t:$lcu r:WIDTH=7 %i
+select -assert-none t:$gt t:$ge t:$lt t:$le
+
+
+design -reset
+read_verilog <<EOT
+module top(input [8:0] a, b, output gtu, gts, ltu, lts, geu, ges, leu, les);
+wire [13:0] c = {a[8:6], 3'b101, a[5:4], 2'b11, a[3:0]};
+wire [13:0] d = {b[8], 3'b101, b[7:4], 2'b01, b[3:0]};
+assign gtu = c > d;
+assign gts = $signed(c) > $signed(d);
+assign ltu = c < d;
+assign lts = $signed(c) < $signed(d);
+assign geu = c >= d;
+assign ges = $signed(c) >= $signed(d);
+assign leu = c <= d;
+assign les = $signed(c) <= $signed(d);
+endmodule
+EOT
+design -save gold
+
+equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=5
+design -load postopt
+select -assert-count 8 t:$lcu r:WIDTH=2 %i
+select -assert-none t:$gt t:$ge t:$lt t:$le
+
+design -load preopt
+equiv_opt -assert techmap -map +/cmp2lcu.v -D LUT_WIDTH=3
+design -load postopt
+select -assert-count 8 t:$lcu r:WIDTH=4 %i
+select -assert-none t:$gt t:$ge t:$lt t:$le
diff --git a/tests/techmap/iopadmap.ys b/tests/techmap/iopadmap.ys
index 25ea94dfc..df029b3a0 100644
--- a/tests/techmap/iopadmap.ys
+++ b/tests/techmap/iopadmap.ys
@@ -55,13 +55,19 @@ obuf b (.i(i), .o(tmp));
assign o = tmp;
endmodule
+module k(inout o, o2);
+assign o = 1'bz;
+endmodule
+
EOT
opt_clean
tribuf
simplemap
-iopadmap -bits -inpad ibuf o:i -outpad obuf i:o -toutpad obuft oe:i:o -tinoutpad iobuf oe:o:i:io a b c d e f g h i j
+iopadmap -bits -inpad ibuf o:i -outpad obuf i:o -toutpad obuft oe:i:o -tinoutpad iobuf oe:o:i:io a b c d e f g h i j k
opt_clean
+hierarchy -check
+check
select -assert-count 1 a/t:ibuf
select -assert-count 1 a/t:obuf
@@ -140,6 +146,8 @@ select -assert-count 0 i/t:obuf
select -assert-count 1 j/t:ibuf
select -assert-count 1 j/t:obuf
+select -assert-count 2 k/t:iobuf
+
# Check that \init attributes get moved from output buffer
# to buffer input