aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various
diff options
context:
space:
mode:
Diffstat (limited to 'tests/various')
-rw-r--r--tests/various/attrib05_port_conn.v21
-rw-r--r--tests/various/attrib05_port_conn.ys2
-rw-r--r--tests/various/attrib07_func_call.v21
-rw-r--r--tests/various/attrib07_func_call.ys2
-rw-r--r--tests/various/chparam.sh52
-rw-r--r--tests/various/elab_sys_tasks.sv30
-rw-r--r--tests/various/elab_sys_tasks.ys1
-rw-r--r--tests/various/hierarchy.sh1
-rw-r--r--tests/various/opt_rmdff.v50
-rw-r--r--tests/various/opt_rmdff.ys26
-rw-r--r--tests/various/pmux2shiftx.v34
-rw-r--r--tests/various/pmux2shiftx.ys28
-rw-r--r--tests/various/specify.v30
-rw-r--r--tests/various/specify.ys56
14 files changed, 354 insertions, 0 deletions
diff --git a/tests/various/attrib05_port_conn.v b/tests/various/attrib05_port_conn.v
new file mode 100644
index 000000000..e20e66319
--- /dev/null
+++ b/tests/various/attrib05_port_conn.v
@@ -0,0 +1,21 @@
+module bar(clk, rst, inp, out);
+ input wire clk;
+ input wire rst;
+ input wire inp;
+ output reg out;
+
+ always @(posedge clk)
+ if (rst) out <= 1'd0;
+ else out <= ~inp;
+
+endmodule
+
+module foo(clk, rst, inp, out);
+ input wire clk;
+ input wire rst;
+ input wire inp;
+ output wire out;
+
+ bar bar_instance ( (* clock_connected *) clk, rst, (* this_is_the_input *) inp, out);
+endmodule
+
diff --git a/tests/various/attrib05_port_conn.ys b/tests/various/attrib05_port_conn.ys
new file mode 100644
index 000000000..27a016733
--- /dev/null
+++ b/tests/various/attrib05_port_conn.ys
@@ -0,0 +1,2 @@
+# Read and parse Verilog file
+read_verilog attrib05_port_conn.v
diff --git a/tests/various/attrib07_func_call.v b/tests/various/attrib07_func_call.v
new file mode 100644
index 000000000..f55ef2316
--- /dev/null
+++ b/tests/various/attrib07_func_call.v
@@ -0,0 +1,21 @@
+function [7:0] do_add;
+ input [7:0] inp_a;
+ input [7:0] inp_b;
+
+ do_add = inp_a + inp_b;
+
+endfunction
+
+module foo(clk, rst, inp_a, inp_b, out);
+ input wire clk;
+ input wire rst;
+ input wire [7:0] inp_a;
+ input wire [7:0] inp_b;
+ output wire [7:0] out;
+
+ always @(posedge clk)
+ if (rst) out <= 0;
+ else out <= do_add (* combinational_adder *) (inp_a, inp_b);
+
+endmodule
+
diff --git a/tests/various/attrib07_func_call.ys b/tests/various/attrib07_func_call.ys
new file mode 100644
index 000000000..774827651
--- /dev/null
+++ b/tests/various/attrib07_func_call.ys
@@ -0,0 +1,2 @@
+# Read and parse Verilog file
+read_verilog attrib07_func_call.v
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/elab_sys_tasks.sv b/tests/various/elab_sys_tasks.sv
new file mode 100644
index 000000000..774d85b32
--- /dev/null
+++ b/tests/various/elab_sys_tasks.sv
@@ -0,0 +1,30 @@
+module test;
+localparam X=1;
+genvar i;
+generate
+if (X == 1)
+ $info("X is 1");
+if (X == 1)
+ $warning("X is 1");
+else
+ $error("X is not 1");
+case (X)
+ 1: $info("X is 1 in a case statement");
+endcase
+//case (X-1)
+// 1: $warn("X is 2");
+// default: $warn("X might be anything in a case statement");
+//endcase
+for (i = 0; i < 3; i = i + 1)
+begin
+ case(i)
+ 0: $info;
+ 1: $warning;
+ default: $info("default case statemnent");
+ endcase
+end
+
+$info("This is a standalone $info(). Next $info has no parameters");
+$info;
+endgenerate
+endmodule
diff --git a/tests/various/elab_sys_tasks.ys b/tests/various/elab_sys_tasks.ys
new file mode 100644
index 000000000..45bee3a60
--- /dev/null
+++ b/tests/various/elab_sys_tasks.ys
@@ -0,0 +1 @@
+read_verilog -sv elab_sys_tasks.sv
diff --git a/tests/various/hierarchy.sh b/tests/various/hierarchy.sh
index d33a247be..9dbd1c89f 100644
--- a/tests/various/hierarchy.sh
+++ b/tests/various/hierarchy.sh
@@ -53,6 +53,7 @@ echo -n " no explicit top - "
module noTop(a, y);
input a;
output [31:0] y;
+ assign y = a;
endmodule
EOV
hierarchy -auto-top
diff --git a/tests/various/opt_rmdff.v b/tests/various/opt_rmdff.v
new file mode 100644
index 000000000..b1c06703c
--- /dev/null
+++ b/tests/various/opt_rmdff.v
@@ -0,0 +1,50 @@
+module opt_rmdff_test (input C, input D, input E, output [29:0] Q);
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove0 (.CLK(C), .D(D), .EN(1'b0), .Q(Q[0])); // EN is never active
+(* init = "1'b1" *) wire Q1; assign Q[1] = Q1;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove1 (.CLK(C), .D(D), .EN(1'b0), .Q(Q1)); // EN is never active
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove2 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[2])); // EN is don't care
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep3 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[3])); // EN is always active
+(* init = "1'b0" *) wire Q4; assign Q[4] = Q4;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) keep4 (.CLK(C), .D(D), .EN(1'b1), .Q(Q4)); // EN is always active
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove5 (.CLK(C), .D(D), .EN(1'b1), .Q(Q[5])); // EN is never active
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove6 (.CLK(C), .D(D), .EN(1'bx), .Q(Q[6])); // EN is don't care
+(* init = "1'b0" *) wire Q7; assign Q[7] = Q7;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(0)) keep7 (.CLK(C), .D(D), .EN(E), .Q(Q7)); // EN is non constant
+
+\$_DFFE_PP_ remove8 (.C(C), .D(D), .E(1'b0), .Q(Q[8])); // EN is never active
+(* init = "1'b1" *) wire Q9; assign Q[9] = Q9;
+\$_DFFE_PP_ remove9 (.C(C), .D(D), .E(1'b0), .Q(Q9)); // EN is never active
+\$_DFFE_PP_ remove10 (.C(C), .D(D), .E(1'bx), .Q(Q[10])); // EN is don't care
+\$_DFFE_PP_ keep11 (.C(C), .D(D), .E(1'b1), .Q(Q[11])); // EN is always active
+(* init = "1'b0" *) wire Q12; assign Q[12] = Q12;
+\$_DFFE_PP_ keep12 (.C(C), .D(D), .E(1'b1), .Q(Q12)); // EN is always active
+
+\$_DFFE_NN_ remove13 (.C(C), .D(D), .E(1'b1), .Q(Q[13])); // EN is never active
+(* init = "1'b1" *) wire Q14; assign Q[14] = Q14;
+\$_DFFE_NN_ remove14 (.C(C), .D(D), .E(1'b1), .Q(Q14)); // EN is never active
+\$_DFFE_NN_ remove15 (.C(C), .D(D), .E(1'bx), .Q(Q[15])); // EN is don't care
+\$_DFFE_NN_ keep16 (.C(C), .D(D), .E(1'b0), .Q(Q[16])); // EN is always active
+(* init = "1'b0" *) wire Q17; assign Q[17] = Q17;
+\$_DFFE_NN_ keep17 (.C(C), .D(D), .E(1'b0), .Q(Q17)); // EN is always active
+
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove18 (.CLK(1'b0), .D(D), .EN(E), .Q(Q[18])); // CLK is constant
+(* init = "1'b1" *) wire Q19; assign Q[19] = Q19;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove19 (.CLK(1'b1), .D(D), .EN(E), .Q(Q19)); // CLK is constant
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove20 (.CLK(C), .D(1'bx), .EN(E), .Q(Q[20])); // D is undriven, Q has no initial value
+(* init = "1'b0" *) wire Q21; assign Q[21] = Q21;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep21 (.CLK(C), .D(1'bx), .EN(E), .Q(Q21)); // D is undriven, Q has initial value
+//\$dffe #(.WIDTH(1), .CLK_POLARITY(0), .EN_POLARITY(1)) remove22 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q[22])); // D is constant, no initial Q value, EN is always active
+// // (TODO, Q starts with 1'bx and becomes 1'b0)
+(* init = "1'b0" *) wire Q23; assign Q[23] = Q23;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) noenable23 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q23)); // D is constant, initial Q value same as D, EN is always active
+(* init = "1'b1" *) wire Q24; assign Q[24] = Q24;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) keep24 (.CLK(C), .D(1'b0), .EN(1'b0), .Q(Q24)); // D is constant, initial Q value NOT same as D, EN is always active
+(* init = "1'b1" *) wire Q25; assign Q[25] = Q25;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove25 (.CLK(C), .D(1'b0), .EN(1'b1), .Q(Q25)); // D is constant, EN is never active
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) remove26 (.CLK(C), .D(Q[26]), .EN(1'b1), .Q(Q[26])); // D is Q, EN is always active
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove27 (.CLK(C), .D(Q[27]), .EN(1'b1), .Q(Q[27])); // D is Q, EN is never active, but no initial value
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(0)) remove28 (.CLK(C), .D(Q[28]), .EN(E), .Q(Q[28])); // EN is nonconst, but no initial value
+(* init = "1'b1" *) wire Q29; assign Q[29] = Q29;
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1), .EN_POLARITY(1)) keep29 (.CLK(C), .D(Q[29]), .EN(1'b1), .Q(Q29)); // EN is always active, but with initial value
+
+endmodule
diff --git a/tests/various/opt_rmdff.ys b/tests/various/opt_rmdff.ys
new file mode 100644
index 000000000..081f81782
--- /dev/null
+++ b/tests/various/opt_rmdff.ys
@@ -0,0 +1,26 @@
+read_verilog -icells opt_rmdff.v
+prep
+design -stash gold
+read_verilog -icells opt_rmdff.v
+proc
+opt_rmdff
+
+select -assert-count 0 c:remove*
+select -assert-min 7 c:keep*
+select -assert-count 0 t:$dffe 7:$_DFFE_* %u c:noenable* %i
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+equiv_make gold gate equiv
+hierarchy -top equiv
+equiv_simple -undef
+equiv_status -assert
+
+design -load gold
+stat
+
+design -load gate
+stat
diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v
new file mode 100644
index 000000000..fec84187b
--- /dev/null
+++ b/tests/various/pmux2shiftx.v
@@ -0,0 +1,34 @@
+module pmux2shiftx_test (
+ input [2:0] S1,
+ input [5:0] S2,
+ input [1:0] S3,
+ input [9:0] A, B, C, D, D, E, F, G, H,
+ input [9:0] I, J, K, L, M, N, O, P, Q,
+ output reg [9:0] X
+);
+ always @* begin
+ case (S1)
+ 3'd 0: X = A;
+ 3'd 1: X = B;
+ 3'd 2: X = C;
+ 3'd 3: X = D;
+ 3'd 4: X = E;
+ 3'd 5: X = F;
+ 3'd 6: X = G;
+ 3'd 7: X = H;
+ endcase
+ case (S2)
+ 6'd 45: X = I;
+ 6'd 47: X = J;
+ 6'd 49: X = K;
+ 6'd 55: X = L;
+ 6'd 57: X = M;
+ 6'd 59: X = N;
+ endcase
+ case (S3)
+ 2'd 1: X = O;
+ 2'd 2: X = P;
+ 2'd 3: X = Q;
+ endcase
+ end
+endmodule
diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys
new file mode 100644
index 000000000..deb134083
--- /dev/null
+++ b/tests/various/pmux2shiftx.ys
@@ -0,0 +1,28 @@
+read_verilog pmux2shiftx.v
+prep
+design -save gold
+
+pmux2shiftx -min_density 70
+
+opt
+
+stat
+# show -width
+select -assert-count 1 t:$sub
+select -assert-count 1 t:$mux
+select -assert-count 1 t:$shift
+select -assert-count 3 t:$shiftx
+
+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 -load gold
+stat
+
+design -load gate
+stat
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
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-29 12:36:09 +0000