diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/arch/anlogic/fsm.ys | 5 | ||||
-rw-r--r-- | tests/arch/efinix/fsm.ys | 5 | ||||
-rw-r--r-- | tests/opt/opt_expr_alu.ys | 63 | ||||
-rw-r--r-- | tests/opt/opt_expr_xor.ys | 52 | ||||
-rw-r--r-- | tests/opt/opt_merge_init.ys | 28 | ||||
-rw-r--r-- | tests/opt/opt_merge_keep.ys | 64 | ||||
-rw-r--r-- | tests/simple/dynslice.v | 12 | ||||
-rw-r--r-- | tests/svtypes/typedef_scopes.sv | 7 | ||||
-rw-r--r-- | tests/techmap/cmp2lcu.ys | 52 | ||||
-rw-r--r-- | tests/techmap/iopadmap.ys | 10 | ||||
-rw-r--r-- | tests/techmap/techmap_replace.ys | 18 | ||||
-rw-r--r-- | tests/various/sv_defines.ys | 33 | ||||
-rw-r--r-- | tests/various/sv_defines_dup.ys | 5 | ||||
-rw-r--r-- | tests/various/sv_defines_mismatch.ys | 5 | ||||
-rw-r--r-- | tests/various/sv_defines_too_few.ys | 7 |
15 files changed, 358 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/svtypes/typedef_scopes.sv b/tests/svtypes/typedef_scopes.sv index d41a58147..5507d84f2 100644 --- a/tests/svtypes/typedef_scopes.sv +++ b/tests/svtypes/typedef_scopes.sv @@ -31,5 +31,12 @@ module top; always @(*) assert(inner_i2 == 4'h2); always @(*) assert(inner_enum2 == 3'h4); +endmodule + +typedef logic[7:0] between_t; +module other; + between_t a = 8'h42; + always @(*) assert(a == 8'h42); 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 diff --git a/tests/techmap/techmap_replace.ys b/tests/techmap/techmap_replace.ys index c2f42d50b..8403586bd 100644 --- a/tests/techmap/techmap_replace.ys +++ b/tests/techmap/techmap_replace.ys @@ -16,3 +16,21 @@ EOT techmap -map %techmap select -assert-any w:s0.asdf select -assert-any c:s0.blah + +read_verilog <<EOT +module sub(input i, output o, input j); +wire _TECHMAP_REPLACE_.asdf = i ; +barfoo _TECHMAP_REPLACE_.blah (i, o, j); +endmodule +EOT +design -stash techmap + +read_verilog <<EOT +module top(input i, output o); +sub s0(i, o); +endmodule +EOT + +techmap -map %techmap +select -assert-any w:s0.asdf +select -assert-any c:s0.blah diff --git a/tests/various/sv_defines.ys b/tests/various/sv_defines.ys new file mode 100644 index 000000000..8e70ee0ee --- /dev/null +++ b/tests/various/sv_defines.ys @@ -0,0 +1,33 @@ +# Check that basic macro expansions do what you'd expect + +read_verilog <<EOT +`define empty_arglist() 123 +`define one_arg(x) 123+x +`define opt_arg(x = 1) 123+x +`define two_args(x, y = (1+23)) x+y +`define nested_comma(x = {31'b0, 1'b1}, y=3) x+y + +module top; + localparam a = `empty_arglist(); + localparam b = `one_arg(10); + localparam c = `opt_arg(10); + localparam d = `opt_arg(); + localparam e = `two_args(1,2); + localparam f = `two_args(1); + localparam g = `nested_comma(1, 2); + localparam h = `nested_comma({31'b0, (1'b0)}); + localparam i = `nested_comma(, 1); + + generate + if (a != 123) $error("a bad"); + if (b != 133) $error("b bad"); + if (c != 133) $error("c bad"); + if (d != 124) $error("d bad"); + if (e != 3) $error("e bad"); + if (f != 25) $error("f bad"); + if (g != 3) $error("g bad"); + if (h != 3) $error("h bad"); + if (i != 2) $error("i bad"); + endgenerate +endmodule +EOT diff --git a/tests/various/sv_defines_dup.ys b/tests/various/sv_defines_dup.ys new file mode 100644 index 000000000..38418ba8f --- /dev/null +++ b/tests/various/sv_defines_dup.ys @@ -0,0 +1,5 @@ +# Check for duplicate arguments +logger -expect error "Duplicate macro arguments with name `x'" 1 +read_verilog <<EOT +`define duplicate_arg(x, x) +EOT diff --git a/tests/various/sv_defines_mismatch.ys b/tests/various/sv_defines_mismatch.ys new file mode 100644 index 000000000..ab6e899de --- /dev/null +++ b/tests/various/sv_defines_mismatch.ys @@ -0,0 +1,5 @@ +# Check that we spot mismatched brackets +logger -expect error "Mismatched brackets in macro argument: \[ and }." 1 +read_verilog <<EOT +`define foo(x=[1,2}) +EOT diff --git a/tests/various/sv_defines_too_few.ys b/tests/various/sv_defines_too_few.ys new file mode 100644 index 000000000..295884809 --- /dev/null +++ b/tests/various/sv_defines_too_few.ys @@ -0,0 +1,7 @@ +# Check that we don't allow passing too few arguments (and, while we're at it, check that passing "no" +# arguments actually passes 1 empty argument). +logger -expect error "Cannot expand macro `foo by giving only 1 argument \(argument 2 has no default\)." 1 +read_verilog <<EOT +`define foo(x=1, y) +`foo() +EOT |