diff options
Diffstat (limited to 'tests/various')
-rw-r--r-- | tests/various/.gitignore | 3 | ||||
-rw-r--r-- | tests/various/attrib05_port_conn.v | 21 | ||||
-rw-r--r-- | tests/various/attrib05_port_conn.ys | 2 | ||||
-rw-r--r-- | tests/various/attrib07_func_call.v | 21 | ||||
-rw-r--r-- | tests/various/attrib07_func_call.ys | 2 | ||||
-rw-r--r-- | tests/various/chparam.sh | 52 | ||||
-rw-r--r-- | tests/various/elab_sys_tasks.sv | 30 | ||||
-rw-r--r-- | tests/various/elab_sys_tasks.ys | 1 | ||||
-rw-r--r-- | tests/various/hierarchy.sh | 1 | ||||
-rw-r--r-- | tests/various/muxcover.ys | 461 | ||||
-rw-r--r-- | tests/various/muxpack.v | 259 | ||||
-rw-r--r-- | tests/various/muxpack.ys | 268 | ||||
-rw-r--r-- | tests/various/opt_rmdff.v | 50 | ||||
-rw-r--r-- | tests/various/opt_rmdff.ys | 26 | ||||
-rw-r--r-- | tests/various/pmux2shiftx.v | 44 | ||||
-rw-r--r-- | tests/various/pmux2shiftx.ys | 39 | ||||
-rw-r--r-- | tests/various/shregmap.v | 48 | ||||
-rw-r--r-- | tests/various/shregmap.ys | 66 | ||||
-rw-r--r-- | tests/various/signext.ys | 33 | ||||
-rw-r--r-- | tests/various/specify.v | 39 | ||||
-rw-r--r-- | tests/various/specify.ys | 58 |
21 files changed, 1522 insertions, 2 deletions
diff --git a/tests/various/.gitignore b/tests/various/.gitignore index 397b4a76..7b3e8c68 100644 --- a/tests/various/.gitignore +++ b/tests/various/.gitignore @@ -1 +1,2 @@ -*.log +/*.log +/*.out diff --git a/tests/various/attrib05_port_conn.v b/tests/various/attrib05_port_conn.v new file mode 100644 index 00000000..e20e6631 --- /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 00000000..27a01673 --- /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 00000000..f55ef231 --- /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 00000000..77482765 --- /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 00000000..9bb8d81d --- /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 00000000..774d85b3 --- /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 00000000..45bee3a6 --- /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 d33a247b..9dbd1c89 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/muxcover.ys b/tests/various/muxcover.ys index 7ac460f1..67e9625e 100644 --- a/tests/various/muxcover.ys +++ b/tests/various/muxcover.ys @@ -13,7 +13,7 @@ read_verilog -formal <<EOT EOT -## Examle usage for "pmuxtree" and "muxcover" +## Example usage for "pmuxtree" and "muxcover" proc pmuxtree @@ -49,3 +49,462 @@ hierarchy -top equiv equiv_simple -undef equiv_status -assert +## Partial matching MUX4 + +design -reset +read_verilog -formal <<EOT +module mux_if_bal_3_1 #(parameter N=3, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {{W{{1'bx}}}}; + if (s[0] == 1'b0) + if (s[1] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[1] == 1'b0) + o <= i[2*W+:W]; +end +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux4=150 +select -assert-count 0 t:$_MUX_ +select -assert-count 1 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX4_ +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 + +## Partial matching MUX8 + +design -reset +read_verilog -formal <<EOT +module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {{W{{1'bx}}}}; + if (s[0] == 1'b0) + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[2] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[4*W+:W]; +end +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux4=150 -mux8=200 +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +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 + +## Partial matching MUX16 + +design -reset +read_verilog -formal <<EOT +module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {{W{{1'bx}}}}; + if (s[0] == 1'b0) + if (s[1] == 1'b0) + if (s[2] == 1'b0) + if (s[3] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[3] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + if (s[2] == 1'b0) + if (s[3] == 1'b0) + o <= i[4*W+:W]; + else + o <= i[5*W+:W]; + else + if (s[3] == 1'b0) + o <= i[6*W+:W]; + else + o <= i[7*W+:W]; + else + if (s[1] == 1'b0) + if (s[2] == 1'b0) + if (s[3] == 1'b0) + o <= i[8*W+:W]; +end +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux4=150 -mux8=200 -mux16=250 +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +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 + +## MUX2 in MUX4 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux2in4(input [1:0] i, input s, output o); + assign o = s ? i[1] : i[0]; +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux4=99 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 1 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX4_ +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 + +## MUX2 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux2in8(input [1:0] i, input s, output o); + assign o = s ? i[1] : i[0]; +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux8=99 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +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 + +## MUX4 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux4in8(input [3:0] i, input [1:0] s, output o); + assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]); +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux8=299 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +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 + +## MUX2 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux2in16(input [1:0] i, input s, output o); + assign o = s ? i[1] : i[0]; +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux16=99 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +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 + +## MUX4 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux4in16(input [3:0] i, input [1:0] s, output o); + assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]); +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux16=299 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +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 + +## MUX8 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux4in16(input [7:0] i, input [2:0] s, output o); + assign o = s[2] ? s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]) + : s[1] ? (s[0] ? i[7] : i[6]) : (s[0] ? i[5] : i[4]); +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux16=699 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +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 + +## mux_if_bal_5_1 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {{W{{1'bx}}}}; + if (s[0] == 1'b0) + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[2] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[4*W+:W]; +end +endmodule +EOT +prep +design -save gold + +wreduce +opt -full +techmap +muxcover -mux8=350 +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter + +## mux_if_bal_5_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132 +design -load gold + +wreduce +opt -full +techmap +muxcover -mux8=350 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter + +## mux_if_bal_9_1 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {{W{{1'bx}}}}; + if (s[3] == 1'b0) + if (s[2] == 1'b0) + if (s[1] == 1'b0) + if (s[0] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[0] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + if (s[1] == 1'b0) + if (s[0] == 1'b0) + o <= i[4*W+:W]; + else + o <= i[5*W+:W]; + else + if (s[0] == 1'b0) + o <= i[6*W+:W]; + else + o <= i[7*W+:W]; + else + if (s[2] == 1'b0) + if (s[1] == 1'b0) + if (s[0] == 1'b0) + o <= i[8*W+:W]; +end +endmodule +EOT +prep +design -save gold + +wreduce +opt -full +techmap +muxcover -mux16=750 +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter + +## mux_if_bal_9_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132 + +design -load gold + +wreduce +opt -full +techmap +muxcover -mux16=750 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter diff --git a/tests/various/muxpack.v b/tests/various/muxpack.v new file mode 100644 index 00000000..33ece1f1 --- /dev/null +++ b/tests/various/muxpack.v @@ -0,0 +1,259 @@ +module mux_if_unbal_4_1 #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* + if (s == 0) o <= i[0*W+:W]; + else if (s == 1) o <= i[1*W+:W]; + else if (s == 2) o <= i[2*W+:W]; + else if (s == 3) o <= i[3*W+:W]; + else o <= {W{1'bx}}; +endmodule + +module mux_if_unbal_5_3 #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {W{1'bx}}; + if (s == 0) o <= i[0*W+:W]; + if (s == 1) o <= i[1*W+:W]; + if (s == 2) o <= i[2*W+:W]; + if (s == 3) o <= i[3*W+:W]; + if (s == 4) o <= i[4*W+:W]; +end +endmodule + +module mux_if_unbal_5_3_invert #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* + if (s != 0) + if (s != 1) + if (s != 2) + if (s != 3) + if (s != 4) o <= i[4*W+:W]; + else o <= i[0*W+:W]; + else o <= i[3*W+:W]; + else o <= i[2*W+:W]; + else o <= i[1*W+:W]; + else o <= {W{1'bx}}; +endmodule + +module mux_if_unbal_5_3_width_mismatch #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {W{1'bx}}; + if (s == 0) o <= i[0*W+:W]; + if (s == 1) o <= i[1*W+:W]; + if (s == 2) o[W-2:0] <= i[2*W+:W-1]; + if (s == 3) o <= i[3*W+:W]; + if (s == 4) o <= i[4*W+:W]; +end +endmodule + +module mux_if_unbal_4_1_missing #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + if (s == 0) o <= i[0*W+:W]; +// else if (s == 1) o <= i[1*W+:W]; +// else if (s == 2) o <= i[2*W+:W]; + else if (s == 3) o <= i[3*W+:W]; + else o <= {W{1'bx}}; +end +endmodule + +module mux_if_unbal_5_3_order #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {W{1'bx}}; + if (s == 3) o <= i[3*W+:W]; + if (s == 2) o <= i[2*W+:W]; + if (s == 1) o <= i[1*W+:W]; + if (s == 4) o <= i[4*W+:W]; + if (s == 0) o <= i[0*W+:W]; +end +endmodule + +module mux_if_unbal_4_1_nonexcl #(parameter N=4, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* + if (s == 0) o <= i[0*W+:W]; + else if (s == 1) o <= i[1*W+:W]; + else if (s == 2) o <= i[2*W+:W]; + else if (s == 3) o <= i[3*W+:W]; + else if (s == 0) o <= {W{1'b0}}; + else o <= {W{1'bx}}; +endmodule + +module mux_if_unbal_5_3_nonexcl #(parameter N=5, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {W{1'bx}}; + if (s == 0) o <= i[0*W+:W]; + if (s == 1) o <= i[1*W+:W]; + if (s == 2) o <= i[2*W+:W]; + if (s == 3) o <= i[3*W+:W]; + if (s == 4) o <= i[4*W+:W]; + if (s == 0) o <= i[2*W+:W]; +end +endmodule + +module mux_case_unbal_8_7#(parameter N=8, parameter W=7) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {W{1'bx}}; + case (s) + 0: o <= i[0*W+:W]; + default: + case (s) + 1: o <= i[1*W+:W]; + 2: o <= i[2*W+:W]; + default: + case (s) + 3: o <= i[3*W+:W]; + 4: o <= i[4*W+:W]; + 5: o <= i[5*W+:W]; + default: + case (s) + 6: o <= i[6*W+:W]; + default: o <= i[7*W+:W]; + endcase + endcase + endcase + endcase +end +endmodule + +module mux_if_bal_8_2 #(parameter N=8, parameter W=2) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* + if (s[0] == 1'b0) + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[2] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[4*W+:W]; + else + o <= i[5*W+:W]; + else + if (s[2] == 1'b0) + o <= i[6*W+:W]; + else + o <= i[7*W+:W]; +endmodule + +module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* + if (s[0] == 1'b0) + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[2] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + o <= i[4*W+:W]; +endmodule + +module cliffordwolf_nonexclusive_select ( + input wire x, y, z, + input wire a, b, c, d, + output reg o +); + always @* begin + o = a; + if (x) o = b; + if (y) o = c; + if (z) o = d; + end +endmodule + +module cliffordwolf_freduce ( + input wire [1:0] s, + input wire a, b, c, d, + output reg [3:0] o +); + always @* begin + o = {4{a}}; + if (s == 0) o = {3{b}}; + if (s == 1) o = {2{c}}; + if (s == 2) o = d; + end +endmodule + +module case_nonexclusive_select ( + input wire [1:0] x, y, + input wire a, b, c, d, e, + output reg o +); + always @* begin + case (x) + 0: o = b; + 2: o = b; + 1: o = c; + default: begin + o = a; + if (y == 0) o = d; + if (y == 1) o = e; + end + endcase + end +endmodule + +module case_nonoverlap ( + input wire [2:0] x, + input wire a, b, c, d, e, + output reg o +); + always @* begin + case (x) + 0, 2: o = b; // Creates $reduce_or + 1: o = c; + default: + case (x) + 3: o = d; 4: o = d; // Creates $reduce_or + 5: o = e; + default: o = 1'b0; + endcase + endcase + end +endmodule + +module case_overlap ( + input wire [2:0] x, + input wire a, b, c, d, e, + output reg o +); + always @* begin + case (x) + 0, 2: o = b; // Creates $reduce_or + 1: o = c; + default: + case (x) + 0: o = 1'b1; // OVERLAP! + 3, 4: o = d; // Creates $reduce_or + 5: o = e; + default: o = 1'b0; + endcase + endcase + end +endmodule + +module case_overlap2 ( + input wire [2:0] x, + input wire a, b, c, d, e, + output reg o +); + always @* begin + case (x) + 0: o = b; 2: o = b; // Creates $reduce_or + 1: o = c; + default: + case (x) + 0: o = d; 2: o = d; // Creates $reduce_or + 3: o = d; 4: o = d; // Creates $reduce_or + 5: o = e; + default: o = 1'b0; + endcase + endcase + end +endmodule diff --git a/tests/various/muxpack.ys b/tests/various/muxpack.ys new file mode 100644 index 00000000..af23fcec --- /dev/null +++ b/tests/various/muxpack.ys @@ -0,0 +1,268 @@ +read_verilog muxpack.v +design -save read + +hierarchy -top mux_if_unbal_4_1 +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 read +hierarchy -top mux_if_unbal_5_3 +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 + +# TODO: Currently ExclusiveDatabase only analyses $eq cells +#design -load read +#hierarchy -top mux_if_unbal_5_3_invert +#prep +#design -save gold +#muxpack +#opt +#stat +#select -assert-count 0 t:$mux +#select -assert-count 1 t:$pmux +#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 read +hierarchy -top mux_if_unbal_5_3_width_mismatch +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 2 t:$pmux +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 read +hierarchy -top mux_if_unbal_4_1_missing +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 read +hierarchy -top mux_if_unbal_5_3_order +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 read +hierarchy -top mux_if_unbal_4_1_nonexcl +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 read +hierarchy -top mux_if_unbal_5_3_nonexcl +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 read +hierarchy -top mux_case_unbal_8_7 +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 read +hierarchy -top mux_if_bal_8_2 +prep +design -save gold +muxpack +opt +stat +select -assert-count 7 t:$mux +select -assert-count 0 t:$pmux +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 read +hierarchy -top mux_if_bal_5_1 +prep +design -save gold +muxpack +opt +stat +select -assert-count 4 t:$mux +select -assert-count 0 t:$pmux +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 read +hierarchy -top cliffordwolf_nonexclusive_select +prep +design -save gold +muxpack +opt +stat +select -assert-count 3 t:$mux +select -assert-count 0 t:$pmux +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 read +#hierarchy -top cliffordwolf_freduce +#prep +#design -save gold +#proc; opt; freduce; opt +#show +#muxpack +#opt +#stat +#select -assert-count 0 t:$mux +#select -assert-count 1 t:$pmux +#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 read +hierarchy -top case_nonexclusive_select +prep +design -save gold +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 2 t:$pmux +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 read +hierarchy -top case_nonoverlap +#prep # Do not prep otherwise $pmux's overlapping entry will get removed +proc +design -save gold +opt -fast -mux_undef +select -assert-count 2 t:$pmux +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 1 t:$pmux +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 read +hierarchy -top case_overlap +#prep # Do not prep otherwise $pmux's overlapping entry will get removed +proc +design -save gold +opt -fast -mux_undef +select -assert-count 2 t:$pmux +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 2 t:$pmux +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 read +hierarchy -top case_overlap2 +#prep # Do not prep otherwise $pmux's overlapping entry will get removed +proc +design -save gold +opt -fast -mux_undef +select -assert-count 2 t:$pmux +muxpack +opt +stat +select -assert-count 0 t:$mux +select -assert-count 2 t:$pmux +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 diff --git a/tests/various/opt_rmdff.v b/tests/various/opt_rmdff.v new file mode 100644 index 00000000..b1c06703 --- /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 00000000..081f8178 --- /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 00000000..56339408 --- /dev/null +++ b/tests/various/pmux2shiftx.v @@ -0,0 +1,44 @@ +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 + +module issue01135(input [7:0] i, output o); +always @* +case (i[6:3]) + 4: o <= i[0]; + 3: o <= i[2]; + 7: o <= i[3]; + default: o <= 1'b0; +endcase +endmodule diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys new file mode 100644 index 00000000..51ee2f7b --- /dev/null +++ b/tests/various/pmux2shiftx.ys @@ -0,0 +1,39 @@ +read_verilog pmux2shiftx.v +design -save read + +hierarchy -top pmux2shiftx_test +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 + +design -load read +hierarchy -top issue01135 +proc +pmux2shiftx -norange +opt -full +select -assert-count 0 t:$shift* +select -assert-count 1 t:$pmux diff --git a/tests/various/shregmap.v b/tests/various/shregmap.v new file mode 100644 index 00000000..604c2c97 --- /dev/null +++ b/tests/various/shregmap.v @@ -0,0 +1,48 @@ +module shregmap_static_test(input i, clk, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[3], shift1[3]}; +endmodule + +module $__SHREG_DFF_P_(input C, D, output Q); +parameter DEPTH = 1; +parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}}; +reg [DEPTH-1:0] r = INIT; +always @(posedge C) + r <= { r[DEPTH-2:0], D }; +assign Q = r[DEPTH-1]; +endmodule + +module shregmap_variable_test(input i, clk, input [1:0] l1, l2, output [1:0] q); +reg head = 1'b0; +reg [3:0] shift1 = 4'b0000; +reg [3:0] shift2 = 4'b0000; + +always @(posedge clk) begin + head <= i; + shift1 <= {shift1[2:0], head}; + shift2 <= {shift2[2:0], head}; +end + +assign q = {shift2[l2], shift1[l1]}; +endmodule + +module $__XILINX_SHREG_(input C, D, input [1:0] L, output Q); +parameter CLKPOL = 1; +parameter ENPOL = 1; +parameter DEPTH = 1; +parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}}; +reg [DEPTH-1:0] r = INIT; +wire clk = C ^ CLKPOL; +always @(posedge C) + r <= { r[DEPTH-2:0], D }; +assign Q = r[L]; +endmodule diff --git a/tests/various/shregmap.ys b/tests/various/shregmap.ys new file mode 100644 index 00000000..d644a88a --- /dev/null +++ b/tests/various/shregmap.ys @@ -0,0 +1,66 @@ +read_verilog shregmap.v +design -save read + +design -copy-to model $__SHREG_DFF_P_ +hierarchy -top shregmap_static_test +prep +design -save gold + +techmap +shregmap -init + +opt + +stat +# show -width +select -assert-count 1 t:$_DFF_P_ +select -assert-count 2 t:$__SHREG_DFF_P_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__SHREG_DFF_P_ \$__SHREG_DFF_P_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -seq 5 miter + +design -load gold +stat + +design -load gate +stat + +########## + +design -load read +design -copy-to model $__XILINX_SHREG_ +hierarchy -top shregmap_variable_test +prep +design -save gold + +simplemap t:$dff t:$dffe +shregmap -tech xilinx + +stat +# show -width +write_verilog -noexpr -norename +select -assert-count 1 t:$_DFF_P_ +select -assert-count 2 t:$__XILINX_SHREG_ + +design -stash gate + +design -import gold -as gold +design -import gate -as gate +design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_ +prep + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -seq 5 miter + +design -load gold +stat + +design -load gate +stat diff --git a/tests/various/signext.ys b/tests/various/signext.ys new file mode 100644 index 00000000..0c8d671e --- /dev/null +++ b/tests/various/signext.ys @@ -0,0 +1,33 @@ + +read_verilog -formal <<EOT +module gate(input clk, output [32:0] o, p, q, r, s, t, u); +assign o = 'bx; +assign p = 1'bx; +assign q = 'bz; +assign r = 1'bz; +assign s = 1'b0; +assign t = 'b1; +assign u = -'sb1; +endmodule +EOT + +proc + +## Equivalence checking + +read_verilog -formal <<EOT +module gold(input clk, output [32:0] o, p, q, r, s, t, u); +assign o = {33{1'bx}}; +assign p = {{32{1'b0}}, 1'bx}; +assign q = {33{1'bz}}; +assign r = {{32{1'b0}}, 1'bz}; +assign s = {33{1'b0}}; +assign t = {{32{1'b0}}, 1'b1}; +assign u = {33{1'b1}}; +endmodule +EOT + +proc + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -enable_undef miter diff --git a/tests/various/specify.v b/tests/various/specify.v new file mode 100644 index 00000000..5d44d78f --- /dev/null +++ b/tests/various/specify.v @@ -0,0 +1,39 @@ +module test ( + input EN, CLK, + input [3:0] D, + output reg [3:0] Q +); + always @(posedge CLK) + 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 + +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 + +module issue01144(input clk, d, output q); +specify + (posedge clk => (q +: d)) = (3,1); + (posedge clk *> (q +: d)) = (3,1); +endspecify +endmodule diff --git a/tests/various/specify.ys b/tests/various/specify.ys new file mode 100644 index 00000000..00597e1e --- /dev/null +++ b/tests/various/specify.ys @@ -0,0 +1,58 @@ +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 + +read_verilog -DSKIP_UNSUPPORTED_IGN_PARSER_CONSTRUCTS specify.v |