aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various
diff options
context:
space:
mode:
Diffstat (limited to 'tests/various')
-rw-r--r--tests/various/abc9.v4
-rw-r--r--tests/various/equiv_opt_multiclock.ys12
-rw-r--r--tests/various/hierarchy_defer.ys27
-rw-r--r--tests/various/peepopt.ys175
4 files changed, 217 insertions, 1 deletions
diff --git a/tests/various/abc9.v b/tests/various/abc9.v
index a08b613a8..30ebd4e26 100644
--- a/tests/various/abc9.v
+++ b/tests/various/abc9.v
@@ -5,5 +5,7 @@ always @*
endmodule
module abc9_test028(input i, output o);
-unknown u(~i, o);
+wire w;
+unknown u(~i, w);
+unknown2 u2(w, o);
endmodule
diff --git a/tests/various/equiv_opt_multiclock.ys b/tests/various/equiv_opt_multiclock.ys
new file mode 100644
index 000000000..81e36d018
--- /dev/null
+++ b/tests/various/equiv_opt_multiclock.ys
@@ -0,0 +1,12 @@
+read_verilog <<EOT
+module top(input clk, pre, d, output reg q);
+ always @(posedge clk, posedge pre)
+ if (pre)
+ q <= 1'b1;
+ else
+ q <= d;
+endmodule
+EOT
+
+prep
+equiv_opt -assert -multiclock -map +/simcells.v synth
diff --git a/tests/various/hierarchy_defer.ys b/tests/various/hierarchy_defer.ys
new file mode 100644
index 000000000..70f5b70a3
--- /dev/null
+++ b/tests/various/hierarchy_defer.ys
@@ -0,0 +1,27 @@
+read -noverific
+read -vlog2k <<EOT
+module first;
+endmodule
+
+(* top *)
+module top(input i, output o);
+sub s0(i, o);
+endmodule
+
+(* constant_expression=1+1?2*2:3/3 *)
+module sub(input i, output o);
+assign o = ~i;
+endmodule
+EOT
+design -save read
+
+hierarchy -auto-top
+select -assert-any top
+select -assert-any sub
+select -assert-none foo
+
+design -load read
+hierarchy
+select -assert-any top
+select -assert-any sub
+select -assert-none foo
diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
new file mode 100644
index 000000000..6bca62e2b
--- /dev/null
+++ b/tests/various/peepopt.ys
@@ -0,0 +1,175 @@
+read_verilog <<EOT
+module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o);
+assign o = i[s*W+:W];
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$shiftx
+select -assert-count 0 t:$shiftx t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_shiftmul_1 (output [7:0] y, input [2:0] w);
+assign y = 1'b1 >> (w * (3'b110));
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$shr
+select -assert-count 1 t:$mul
+select -assert-count 0 t:$shr t:$mul %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_shiftmul_2 (input [11:0] D, input [1:0] S, output [11:0] Y);
+ assign Y = D >> (S*3);
+endmodule
+EOT
+
+prep
+design -save gold
+peepopt
+design -stash gate
+
+design -import gold -as gold peepopt_shiftmul_2
+design -import gate -as gate peepopt_shiftmul_2
+
+miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter
+sat -show-public -enable_undef -prove-asserts miter
+cd gate
+select -assert-count 1 t:$shr
+select -assert-count 1 t:$mul
+select -assert-count 0 t:$shr t:$mul %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_muldiv_0(input [1:0] i, output [1:0] o);
+wire [3:0] t;
+assign t = i * 3;
+assign o = t / 3;
+endmodule
+EOT
+
+prep -nokeepdc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 0 t:*
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o);
+ always @(posedge clk) if (ce) o <= i;
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o);
+ always @(posedge clk) if (ce) o <= i;
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+clean
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+###################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_const(input clk, ce, input [1:0] i, output reg [5:0] o);
+ always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+###################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_const_init(input clk, ce, input [1:0] i, (* init=6'b0x00x1 *) output reg [5:0] o);
+ always @(posedge clk) if (ce) o <= {1'b0, i[1], 2'b1x, i[0], 1'bz};
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+select -assert-count 1 t:$dff r:WIDTH=5 %i
+select -assert-count 1 t:$mux r:WIDTH=5 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_unsigned_rst(input clk, ce, rst, input [1:0] i, output reg [3:0] o);
+ always @(posedge clk) if (rst) o <= 0; else if (ce) o <= i;
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+wreduce
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 2 t:$mux
+select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_signed_rst(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
+ always @(posedge clk) begin
+ if (ce) o <= i;
+ if (!rstn) o <= 4'b1111;
+ end
+endmodule
+EOT
+
+proc
+equiv_opt -assert peepopt
+design -load postopt
+wreduce
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 2 t:$mux
+select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D