diff options
Diffstat (limited to 'tests')
-rw-r--r-- | tests/simple/genblk_port_shadow.v | 10 | ||||
-rw-r--r-- | tests/various/port_sign_extend.v | 22 | ||||
-rw-r--r-- | tests/various/port_sign_extend.ys | 13 | ||||
-rw-r--r-- | tests/verilog/atom_type_signedness.ys | 19 | ||||
-rw-r--r-- | tests/verilog/block_labels.ys | 26 | ||||
-rw-r--r-- | tests/verilog/genblk_port_decl.ys | 12 |
6 files changed, 95 insertions, 7 deletions
diff --git a/tests/simple/genblk_port_shadow.v b/tests/simple/genblk_port_shadow.v new file mode 100644 index 000000000..a04631a20 --- /dev/null +++ b/tests/simple/genblk_port_shadow.v @@ -0,0 +1,10 @@ +module top(x); + generate + if (1) begin : blk + wire x; + assign x = 0; + end + endgenerate + output wire x; + assign x = blk.x; +endmodule diff --git a/tests/various/port_sign_extend.v b/tests/various/port_sign_extend.v index 446268268..813ceb503 100644 --- a/tests/various/port_sign_extend.v +++ b/tests/various/port_sign_extend.v @@ -24,8 +24,8 @@ module PassThrough(a, b); assign b = a; endmodule -module act(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2); - output wire [3:0] o1, o2, o3, o4, o5, o6; +module act(o1, o2, o3, o4, o5, o6, o7, o8, o9, yay1, nay1, yay2, nay2); + output wire [3:0] o1, o2, o3, o4, o5, o6, o7, o8, o9; // unsigned constant PassThrough pt1(1'b1, o1); @@ -52,6 +52,17 @@ module act(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2); wire signed [2:0] tmp6b = 3'b001; PassThrough pt6(tmp6a ? tmp6a : tmp6b, o6); + wire signed [2:0] tmp7 = 3'b011; + PassThrough pt7(~tmp7, o7); + + reg signed [2:0] tmp8 [0:0]; + initial tmp8[0] = 3'b101; + PassThrough pt8(tmp8[0], o8); + + wire signed [2:0] tmp9a = 3'b100; + wire signed [1:0] tmp9b = 2'b11; + PassThrough pt9(0 ? tmp9a : tmp9b, o9); + output wire [2:0] yay1, nay1; GeneratorSigned1 os1(yay1); GeneratorUnsigned1 ou1(nay1); @@ -61,8 +72,8 @@ module act(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2); GeneratorUnsigned2 ou2(nay2); endmodule -module ref(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2); - output wire [3:0] o1, o2, o3, o4, o5, o6; +module ref(o1, o2, o3, o4, o5, o6, o7, o8, o9, yay1, nay1, yay2, nay2); + output wire [3:0] o1, o2, o3, o4, o5, o6, o7, o8, o9; assign o1 = 4'b0001; assign o2 = 4'b0001; @@ -70,6 +81,9 @@ module ref(o1, o2, o3, o4, o5, o6, yay1, nay1, yay2, nay2); assign o4 = 4'b1111; assign o5 = 4'b1110; assign o6 = 4'b1100; + assign o7 = 4'b1100; + assign o8 = 4'b1101; + assign o9 = 4'b1111; output wire [2:0] yay1, nay1; assign yay1 = 3'b111; diff --git a/tests/various/port_sign_extend.ys b/tests/various/port_sign_extend.ys index 0a6a93810..6d1adf7f3 100644 --- a/tests/various/port_sign_extend.ys +++ b/tests/various/port_sign_extend.ys @@ -1,22 +1,29 @@ -read_verilog port_sign_extend.v +read_verilog -nomem2reg port_sign_extend.v hierarchy flatten +proc +memory equiv_make ref act equiv equiv_simple equiv_status -assert delete -read_verilog port_sign_extend.v +read_verilog -nomem2reg port_sign_extend.v flatten +proc +memory equiv_make ref act equiv equiv_simple equiv_status -assert delete -read_verilog port_sign_extend.v +read_verilog -nomem2reg port_sign_extend.v hierarchy +proc +memory equiv_make ref act equiv prep -flatten -top equiv +equiv_induct equiv_status -assert diff --git a/tests/verilog/atom_type_signedness.ys b/tests/verilog/atom_type_signedness.ys new file mode 100644 index 000000000..22bbe6efc --- /dev/null +++ b/tests/verilog/atom_type_signedness.ys @@ -0,0 +1,19 @@ +read_verilog -dump_ast1 -dump_ast2 -sv <<EOT +module dut(); + +enum integer { uInteger = -10 } a; +enum int { uInt = -11 } b; +enum shortint { uShortInt = -12 } c; +enum byte { uByte = -13 } d; + +always_comb begin + assert(-10 == uInteger); + assert(-11 == uInt); + assert(-12 == uShortInt); + assert(-13 == uByte); +end +endmodule +EOT +hierarchy; proc; opt +select -module dut +sat -verify -seq 1 -tempinduct -prove-asserts -show-all diff --git a/tests/verilog/block_labels.ys b/tests/verilog/block_labels.ys new file mode 100644 index 000000000..e76bcf771 --- /dev/null +++ b/tests/verilog/block_labels.ys @@ -0,0 +1,26 @@ +read_verilog <<EOT +module foo; + + genvar a = 0; + for (a = 0; a < 10; a++) begin : a + end : a +endmodule +EOT +read_verilog <<EOT +module foo2; + + genvar a = 0; + for (a = 0; a < 10; a++) begin : a + end +endmodule +EOT + +logger -expect error "Begin label \(a\) and end label \(b\) don't match\." 1 +read_verilog <<EOT +module foo3; + + genvar a = 0; + for (a = 0; a < 10; a++) begin : a + end : b +endmodule +EOT diff --git a/tests/verilog/genblk_port_decl.ys b/tests/verilog/genblk_port_decl.ys new file mode 100644 index 000000000..589d3d2e1 --- /dev/null +++ b/tests/verilog/genblk_port_decl.ys @@ -0,0 +1,12 @@ +logger -expect error "Cannot declare module port `\\x' within a generate block\." 1 +read_verilog <<EOT +module top(x); + generate + if (1) begin : blk + output wire x; + assign x = 1; + end + endgenerate + output wire x; +endmodule +EOT |