aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various
diff options
context:
space:
mode:
Diffstat (limited to 'tests/various')
-rw-r--r--tests/various/bug1480.ys18
-rw-r--r--tests/various/bug1614.ys5
-rw-r--r--tests/various/bug1710.ys30
-rw-r--r--tests/various/pmux2shiftx.v2
-rw-r--r--tests/various/specify.v29
-rw-r--r--tests/various/specify.ys21
-rw-r--r--tests/various/submod.ys124
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