aboutsummaryrefslogtreecommitdiffstats
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/simple/dff_init.v12
-rw-r--r--tests/simple/forloops.v25
-rw-r--r--tests/various/chparam.sh52
-rw-r--r--tests/various/specify.v30
-rw-r--r--tests/various/specify.ys56
5 files changed, 175 insertions, 0 deletions
diff --git a/tests/simple/dff_init.v b/tests/simple/dff_init.v
index be947042e..375ea5c4d 100644
--- a/tests/simple/dff_init.v
+++ b/tests/simple/dff_init.v
@@ -40,3 +40,15 @@ module dff1a_test(n1, n1_inv, clk);
n1 <= n1_inv;
assign n1_inv = ~n1;
endmodule
+
+module dff_test_997 (y, clk, wire4);
+// https://github.com/YosysHQ/yosys/issues/997
+ output wire [1:0] y;
+ input clk;
+ input signed wire4;
+ reg [1:0] reg10 = 0;
+ always @(posedge clk) begin
+ reg10 <= wire4;
+ end
+ assign y = reg10;
+endmodule
diff --git a/tests/simple/forloops.v b/tests/simple/forloops.v
new file mode 100644
index 000000000..8665222d8
--- /dev/null
+++ b/tests/simple/forloops.v
@@ -0,0 +1,25 @@
+module forloops01 (input clk, a, b, output reg [3:0] p, q, x, y);
+ integer k;
+ always @(posedge clk) begin
+ for (k=0; k<2; k=k+1)
+ p[2*k +: 2] = {a, b} ^ {2{k}};
+ x <= k + {a, b};
+ end
+ always @* begin
+ for (k=0; k<4; k=k+1)
+ q[k] = {~a, ~b, a, b} >> k[1:0];
+ y = k - {a, b};
+ end
+endmodule
+
+module forloops02 (input clk, a, b, output reg [3:0] q, x, output [3:0] y);
+ integer k;
+ always @* begin
+ for (k=0; k<4; k=k+1)
+ q[k] = {~a, ~b, a, b} >> k[1:0];
+ end
+ always @* begin
+ x = k + {a, b};
+ end
+ assign y = k - {a, b};
+endmodule
diff --git a/tests/various/chparam.sh b/tests/various/chparam.sh
new file mode 100644
index 000000000..9bb8d81db
--- /dev/null
+++ b/tests/various/chparam.sh
@@ -0,0 +1,52 @@
+#!/bin/bash
+
+trap 'echo "ERROR in chparam.sh" >&2; exit 1' ERR
+
+cat > chparam1.sv << "EOT"
+module top #(
+ parameter [31:0] X = 0
+) (
+ input [31:0] din,
+ output [31:0] dout
+);
+ assign dout = X-din;
+endmodule
+
+module top_props #(
+ parameter [31:0] X = 0
+) (
+ input [31:0] dout
+);
+ always @* assert (dout != X);
+endmodule
+
+bind top top_props #(.X(123456789)) props (.*);
+EOT
+
+cat > chparam2.sv << "EOT"
+module top #(
+ parameter [31:0] X = 0
+) (
+ input [31:0] din,
+ output [31:0] dout
+);
+ assign dout = X-din;
+ always @* assert (dout != 123456789);
+endmodule
+EOT
+
+if ../../yosys -q -p 'verific -sv chparam1.sv'; then
+ ../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+ -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
+ -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
+
+ ../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+ -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
+ -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
+fi
+../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+ -p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
+ -p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
+
+rm chparam1.sv
+rm chparam2.sv
diff --git a/tests/various/specify.v b/tests/various/specify.v
new file mode 100644
index 000000000..afc421da8
--- /dev/null
+++ b/tests/various/specify.v
@@ -0,0 +1,30 @@
+module test (
+ input EN, CLK,
+ input [3:0] D,
+ output reg [3:0] Q
+);
+ always @(posedge CLK)
+ if (EN) Q <= D;
+
+ specify
+ if (EN) (CLK *> (Q : D)) = (1, 2:3:4);
+ $setup(D, posedge CLK &&& EN, 5);
+ $hold(posedge CLK, D &&& EN, 6);
+ endspecify
+endmodule
+
+module test2 (
+ input A, B,
+ output Q
+);
+ xor (Q, A, B);
+ specify
+ //specparam T_rise = 1;
+ //specparam T_fall = 2;
+ `define T_rise 1
+ `define T_fall 2
+ (A => Q) = (`T_rise,`T_fall);
+ //(B => Q) = (`T_rise+`T_fall)/2.0;
+ (B => Q) = 1.5;
+ endspecify
+endmodule
diff --git a/tests/various/specify.ys b/tests/various/specify.ys
new file mode 100644
index 000000000..a5ca07219
--- /dev/null
+++ b/tests/various/specify.ys
@@ -0,0 +1,56 @@
+read_verilog -specify specify.v
+prep
+cd test
+select t:$specify2 -assert-count 0
+select t:$specify3 -assert-count 1
+select t:$specrule -assert-count 2
+cd test2
+select t:$specify2 -assert-count 2
+select t:$specify3 -assert-count 0
+select t:$specrule -assert-count 0
+cd
+write_verilog specify.out
+design -stash gold
+
+read_verilog -specify specify.out
+prep
+cd test
+select t:$specify2 -assert-count 0
+select t:$specify3 -assert-count 1
+select t:$specrule -assert-count 2
+cd test2
+select t:$specify2 -assert-count 2
+select t:$specify3 -assert-count 0
+select t:$specrule -assert-count 0
+cd
+design -stash gate
+
+design -copy-from gold -as gold test
+design -copy-from gate -as gate test
+rename -hide
+rename -enumerate -pattern A_% t:$specify3
+rename -enumerate -pattern B_% t:$specrule r:TYPE=$setup %i
+rename -enumerate -pattern C_% t:$specrule r:TYPE=$hold %i
+select n:A_* -assert-count 2
+select n:B_* -assert-count 2
+select n:C_* -assert-count 2
+equiv_make gold gate equiv
+hierarchy -top equiv
+equiv_struct
+equiv_induct -seq 5
+equiv_status -assert
+design -reset
+
+design -copy-from gold -as gold test2
+design -copy-from gate -as gate test2
+rename -hide
+rename -enumerate -pattern A_% t:$specify2 r:T_RISE_TYP=1 %i
+rename -enumerate -pattern B_% t:$specify2 n:A_* %d
+select n:A_* -assert-count 2
+select n:B_* -assert-count 2
+equiv_make gold gate equiv
+hierarchy -top equiv
+equiv_struct
+equiv_induct -seq 5
+equiv_status -assert
+design -reset