2025-01-16 01:57:19 +01:00
|
|
|
|
log -header "Test basic s?(a+b):a pattern gets transformed (a,b module inputs)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
log -header "Test basic s?(a+b):a pattern gets transformed (a,b module inputs)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
|
|
|
|
|
|
wire [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
|
|
|
|
|
|
log -header "Test basic s?(a+b):a pattern gets transformed (a,b module inputs)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
assign y = s ? (a + b) : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
|
|
|
|
|
|
log -header "Test basic s?(a+b):a pattern with intermediate var gets transformed (a,b module inputs)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
|
|
|
|
|
|
wire [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
|
|
|
|
|
|
log -header "Test basic s?(a+b):a pattern gets transformed (a is driven by a cell)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a_, b, s, y);
|
|
|
|
|
|
input wire [3:0] a_;
|
|
|
|
|
|
wire [3:0] a = ~a_;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
|
|
|
|
|
|
wire [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
|
|
|
|
|
|
log -header "Test basic s?(a+b):a pattern gets transformed (b is driven by a cell, output consumed by a cell)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b_, f, s, y_);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b_;
|
|
|
|
|
|
input wire [3:0] f;
|
|
|
|
|
|
wire [3:0] b = b_ ^ f;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire [3:0] y;
|
|
|
|
|
|
output wire [3:0] y_;
|
|
|
|
|
|
assign y_ = ~y;
|
|
|
|
|
|
|
|
|
|
|
|
wire [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
|
|
|
|
|
|
log -header "Test no transform when a+b has more fanouts (module output)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, ab, s, y);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [2:0] b;
|
|
|
|
|
|
output wire [2:0] ab;
|
|
|
|
|
|
output wire [2:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
assign ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-none t:$add %co1 %a w:y %i
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
|
|
|
|
|
|
log -header "Test no transform when a+b has more fanouts (single bit, cell)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y, z);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [2:0] b;
|
|
|
|
|
|
output wire [2:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire [2:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
output wire [2:0] z = !ab[1];
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-none t:$add %co1 %a w:y %i
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test no transform when a+b width smaller than a's width"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire [2:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-none t:$add %co1 %a w:y %i
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test no transform when (a+b) wider than a, adder’s a input is unsigned, a is not padded with zeros on the muxes input"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : {a[2], a};
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-none t:$add %co1 %a w:y %i
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test no transform when (a+b) wider than a, adder’s a input is signed, a is not sign-extended on the muxes input"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire signed [3:0] ab = $signed(a) + $signed(b);
|
|
|
|
|
|
assign y = s ? ab : {1'b0, a};
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-none t:$add %co1 %a w:y %i
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test no transform when adder and mux not connected together but otherwise fitting transform. criteria"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire [3:0] ab = a + b;
|
|
|
|
|
|
wire [3:0] ab_ = !a;
|
|
|
|
|
|
assign y = s ? ab_ : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-none t:$add %co1 %a w:y %i
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when (a+b) wider than a, adder’s a input is unsigned, a padded with zeros on the muxes input"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : {1'b0, a};
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when (a+b) wider than a, adder’s a input is signed, a sign-extended on the muxes input"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire signed [3:0] ab = $signed(a) + $signed(b);
|
|
|
|
|
|
assign y = s ? ab : {a[2], a};
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when pattern is s?a:(a+b)"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire signed [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? a : ab;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when pattern is a?(b+a):a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire signed [3:0] ab = b + a;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when widths b > (a+b) > a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [4:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire signed [3:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when widths (a+b) > a > b"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [2:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [4:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire signed [4:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when widths (a+b) > b > a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [2:0] b;
|
|
|
|
|
|
output wire [4:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
wire signed [4:0] ab = a + b;
|
|
|
|
|
|
assign y = s ? ab : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
2025-03-07 01:57:47 +01:00
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
2025-01-16 01:57:19 +01:00
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
2025-05-08 23:05:13 +02:00
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test transform when widths are uneven with no intermediate values"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [2:0] b;
|
|
|
|
|
|
output wire [4:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
assign y = s ? a + b : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
|
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
|
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test basic s ? (a * b) : a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
assign y = s ? a * b : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
|
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
|
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$mul %co1 %a w:y %i # assert mult rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test basic s ? (a & b) : a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
assign y = s ? a & b : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
|
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
|
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$and %co1 %a w:y %i # assert and rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test basic s ? (a | b) : a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire a;
|
|
|
|
|
|
input wire b;
|
|
|
|
|
|
output wire y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
assign y = s ? a | b : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
|
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
|
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$or %co1 %a w:y %i # assert or rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test basic s ? (a ^ b) : a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
assign y = s ? a ^ b : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
|
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
|
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$xor %co1 %a w:y %i # assert xor rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Test basic s ? (a ~^ b) : a"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, s, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s;
|
|
|
|
|
|
assign y = s ? a ~^ b : a;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
|
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
|
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$xnor %co1 %a w:y %i # assert xnor rewired
|
|
|
|
|
|
|
|
|
|
|
|
log -pop
|
|
|
|
|
|
log -header "Nested conditionals"
|
|
|
|
|
|
log -push
|
|
|
|
|
|
design -reset
|
|
|
|
|
|
read_verilog <<EOF
|
|
|
|
|
|
module top(a, b, c, s0, s1, y);
|
|
|
|
|
|
input wire [3:0] a;
|
|
|
|
|
|
input wire [3:0] b;
|
|
|
|
|
|
input wire [3:0] c;
|
|
|
|
|
|
output wire [3:0] y;
|
|
|
|
|
|
input wire s0, s1;
|
|
|
|
|
|
|
|
|
|
|
|
wire [3:0] inter;
|
|
|
|
|
|
|
|
|
|
|
|
assign inter = s0 ? a + b : a;
|
|
|
|
|
|
assign y = s1 ? inter + c : inter;
|
|
|
|
|
|
endmodule
|
|
|
|
|
|
EOF
|
|
|
|
|
|
check -assert
|
|
|
|
|
|
wreduce
|
|
|
|
|
|
opt_clean
|
|
|
|
|
|
equiv_opt -assert peepopt -muxorder
|
|
|
|
|
|
design -load postopt
|
|
|
|
|
|
select -assert-any t:$add %co1 %a w:y %i # assert adder rewired
|