diff options
Diffstat (limited to 'tests/various')
-rw-r--r-- | tests/various/bug1480.ys | 18 | ||||
-rw-r--r-- | tests/various/bug1614.ys | 5 | ||||
-rw-r--r-- | tests/various/bug1710.ys | 30 | ||||
-rw-r--r-- | tests/various/pmux2shiftx.v | 2 | ||||
-rw-r--r-- | tests/various/specify.v | 29 | ||||
-rw-r--r-- | tests/various/specify.ys | 21 | ||||
-rw-r--r-- | tests/various/submod.ys | 124 |
7 files changed, 207 insertions, 22 deletions
diff --git a/tests/various/bug1480.ys b/tests/various/bug1480.ys deleted file mode 100644 index 84faea08a..000000000 --- a/tests/various/bug1480.ys +++ /dev/null @@ -1,18 +0,0 @@ -read_verilog << EOF -module top(...); - -input signed [17:0] A; -input signed [17:0] B; -output X; -output Y; - -wire [35:0] P; -assign P = A * B; - -assign X = P[0]; -assign Y = P[35]; - -endmodule -EOF - -synth_xilinx diff --git a/tests/various/bug1614.ys b/tests/various/bug1614.ys new file mode 100644 index 000000000..6fbe84a4c --- /dev/null +++ b/tests/various/bug1614.ys @@ -0,0 +1,5 @@ +read_verilog <<EOT +module testcase; + wire [3:0] #1 a = 4'b0000; +endmodule +EOT diff --git a/tests/various/bug1710.ys b/tests/various/bug1710.ys new file mode 100644 index 000000000..c2ecf3c90 --- /dev/null +++ b/tests/various/bug1710.ys @@ -0,0 +1,30 @@ +logger -werror "out of bounds" +read_verilog <<EOT +module Example; + + parameter FLAG = 1; + wire [3:0] inp; + + reg out1; + initial out1 = FLAG ? &inp[2:0] : &inp[4:0]; + + reg out2; + initial + if (FLAG) + out2 = &inp[2:0]; + else + out2 = &inp[4:0]; + + wire out3; + assign out3 = FLAG ? &inp[2:0] : &inp[4:0]; + + wire out4; + generate + if (FLAG) + assign out4 = &inp[2:0]; + else + assign out4 = &inp[4:0]; + endgenerate + +endmodule +EOT diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v index 563394080..c1994e92c 100644 --- a/tests/various/pmux2shiftx.v +++ b/tests/various/pmux2shiftx.v @@ -33,7 +33,7 @@ module pmux2shiftx_test ( end endmodule -module issue01135(input [7:0] i, output o); +module issue01135(input [7:0] i, output reg o); always @* case (i[6:3]) 4: o <= i[0]; diff --git a/tests/various/specify.v b/tests/various/specify.v index 5d44d78f7..c160d2ec4 100644 --- a/tests/various/specify.v +++ b/tests/various/specify.v @@ -7,11 +7,9 @@ module test ( if (EN) Q <= D; specify -`ifndef SKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS if (EN) (posedge CLK *> (Q : D)) = (1, 2:3:4); $setup(D, posedge CLK &&& EN, 5); $hold(posedge CLK, D &&& EN, 6); -`endif endspecify endmodule @@ -37,3 +35,30 @@ specify (posedge clk *> (q +: d)) = (3,1); endspecify endmodule + +module test3(input clk, input [1:0] d, output [1:0] q); +specify + (posedge clk => (q +: d)) = (3,1); + (posedge clk *> (q +: d)) = (3,1); +endspecify +endmodule + +module test4(input clk, d, output q); +specify + $setup(d, posedge clk, 1:2:3); + $setuphold(d, posedge clk, 1:2:3, 4:5:6); +endspecify +endmodule + +module test5(input clk, d, e, output q); +specify + $setup(d, posedge clk &&& e, 1:2:3); +endspecify +endmodule + +module test6(input clk, d, e, output q); +specify + (d[0] *> q[0]) = (3,1); + (posedge clk[0] => (q[0] +: d[0])) = (3,1); +endspecify +endmodule diff --git a/tests/various/specify.ys b/tests/various/specify.ys index 00597e1e2..9d55b8eb5 100644 --- a/tests/various/specify.ys +++ b/tests/various/specify.ys @@ -55,4 +55,23 @@ equiv_induct -seq 5 equiv_status -assert design -reset -read_verilog -DSKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS specify.v +read_verilog -specify <<EOT +(* blackbox *) +module test7_sub(input i, output o); +specify + (i => o) = 1; +endspecify +assign o = ~i; +endmodule + +module test7(input i, output o); + wire w; + test7_sub unused(i, w); + test7_sub used(i, o); +endmodule +EOT +hierarchy +cd test7 +clean +select -assert-count 1 c:used +select -assert-none c:* c:used %d diff --git a/tests/various/submod.ys b/tests/various/submod.ys new file mode 100644 index 000000000..4fb45043b --- /dev/null +++ b/tests/various/submod.ys @@ -0,0 +1,124 @@ +read_verilog <<EOT +module top(input a, output b); +wire c; +(* submod="bar" *) sub s1(a, c); +assign b = c; +endmodule + +module sub(input a, output c); +assign c = a; +endmodule +EOT + +hierarchy -top top +proc +design -save gold + +submod +check -assert +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports miter + + +design -reset +read_verilog <<EOT +module top(input a, output [1:0] b); +(* submod="bar" *) sub s1(a, b[1]); +assign b[0] = 1'b0; +endmodule + +module sub(input a, output c); +assign c = a; +endmodule +EOT + +hierarchy -top top +proc +design -save gold + +submod +check -assert top +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports miter + + +design -reset +read_verilog <<EOT +module top(input a, output [1:0] b, c); +(* submod="bar" *) sub s1(a, b[0]); +(* submod="bar" *) sub s2(a, c[1]); +assign c = b; +endmodule + +module sub(input a, output c); +assign c = a; +endmodule +EOT + +hierarchy -top top +proc +design -save gold + +submod +check -assert top +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports miter + + +design -reset +read_verilog <<EOT +module top(input d, c, (* init = 3'b011 *) output reg [2:0] q); +(* submod="bar" *) DFF s1(.D(d), .C(c), .Q(q[1])); +DFF s2(.D(d), .C(c), .Q(q[0])); +DFF s3(.D(d), .C(c), .Q(q[2])); +endmodule + +module DFF(input D, C, output Q); +parameter INIT = 1'b0; +endmodule +EOT + +hierarchy -top top +proc + +submod +dffinit -ff DFF Q INIT +check -noinit -assert + + +design -reset +read_verilog <<EOT +module top(input d, c, output reg [2:0] q); +(* submod="bar" *) DFF s1(.D(d), .C(c), .Q(q[1])); +DFF s2(.D(d), .C(c), .Q(q[0])); +DFF s3(.D(d), .C(c), .Q(q[2])); +endmodule +EOT + +hierarchy -top top +proc + +submod +flatten + +read_verilog <<EOT +module DFF(input D, C, output Q); +endmodule +EOT + +check -assert |