mirror of https://github.com/YosysHQ/yosys.git
Initial implementation of addsub_c with no intermediate fanout allowed
This commit is contained in:
Akash Levy
parent
a43de44f9d
commit
ccf3909982
|
|
@ -33,6 +33,7 @@ PEEPOPT_PATTERN += passes/opt/peepopt_shiftmul_left.pmg
|
|||
PEEPOPT_PATTERN += passes/opt/peepopt_shiftadd.pmg
|
||||
PEEPOPT_PATTERN += passes/opt/peepopt_muldiv.pmg
|
||||
PEEPOPT_PATTERN += passes/opt/peepopt_muldiv_c.pmg
|
||||
PEEPOPT_PATTERN += passes/opt/peepopt_addsub_c.pmg
|
||||
PEEPOPT_PATTERN += passes/opt/peepopt_muxorder.pmg
|
||||
PEEPOPT_PATTERN += passes/opt/peepopt_formal_clockgateff.pmg
|
||||
PEEPOPT_PATTERN += passes/opt/peepopt_sub_neg.pmg
|
||||
|
|
|
|||
|
|
@ -51,6 +51,8 @@ struct PeepoptPass : public Pass {
|
|||
log("\n");
|
||||
log("This pass employs the following rules by default:\n");
|
||||
log("\n");
|
||||
log(" * addsub_c - Replace (A+-B)+-C with A+(B+-C) when B and C are constants.\n");
|
||||
log("\n");
|
||||
log(" * muldiv - Replace (A*B)/B with A\n");
|
||||
log("\n");
|
||||
log(" * muldiv_c - Replace (A*B)/C with A*(B/C) when C is a const divisible by B.\n");
|
||||
|
|
@ -127,6 +129,7 @@ struct PeepoptPass : public Pass {
|
|||
pm.run_shiftmul_left();
|
||||
pm.run_muldiv();
|
||||
pm.run_muldiv_c();
|
||||
pm.run_addsub_c();
|
||||
pm.run_sub_neg();
|
||||
if (muxorder)
|
||||
pm.run_muxorder();
|
||||
|
|
|
|||
|
|
@ -0,0 +1,129 @@
|
|||
pattern addsub_c
|
||||
//
|
||||
// Authored by Akash Levy of Silimate, Inc. under ISC license.
|
||||
// Transforms add->add/sub_c into add_c canceling the constants out:
|
||||
// y = (a +- b_const) +- c_const ===> a +- eval(b_const +- c_const)
|
||||
//
|
||||
|
||||
state <SigSpec> a b_const addsub1_y
|
||||
|
||||
match addsub1
|
||||
// Select add/sub
|
||||
select addsub1->type.in($add, $sub)
|
||||
endmatch
|
||||
|
||||
code a b_const addsub1_y
|
||||
// Get adder signals
|
||||
a = port(addsub1, \A);
|
||||
b_const = port(addsub1, \B);
|
||||
addsub1_y = port(addsub1, \Y);
|
||||
|
||||
// Fanout of each add/sub Y bit should be 1 (no bit-split)
|
||||
if (nusers(addsub1_y) != 2)
|
||||
reject;
|
||||
|
||||
// A and B can be interchanged for adder
|
||||
if (addsub1->type == $add) {
|
||||
branch;
|
||||
std::swap(a, b_const);
|
||||
}
|
||||
endcode
|
||||
|
||||
match addsub2
|
||||
// Select add/sub of form (a +- b_const) +- c_const
|
||||
select addsub2->type.in($add, $sub)
|
||||
|
||||
// Check that b_const and c_const is constant
|
||||
filter b_const.is_fully_const()
|
||||
filter port(addsub2, \B).is_fully_const()
|
||||
index <SigSpec> remove_bottom_padding(port(addsub2, \A)) === addsub1_y
|
||||
endmatch
|
||||
|
||||
code
|
||||
// Get addsub2 signals
|
||||
SigSpec addsub2_a = port(addsub2, \A);
|
||||
SigSpec c_const = port(addsub2, \B);
|
||||
SigSpec addsub2_y = port(addsub2, \Y);
|
||||
|
||||
// Get offset of addsub1 result chunk in addsub2
|
||||
int offset = GetSize(addsub2_a) - GetSize(addsub1_y);
|
||||
|
||||
// Get properties and values of b_const and c_const
|
||||
// b_const may be coming from the A port
|
||||
// But it is an RTLIL invariant that A_SIGNED equals B_SIGNED
|
||||
bool b_const_signed = addsub1->getParam(ID::B_SIGNED).as_bool();
|
||||
bool c_const_signed = addsub2->getParam(ID::B_SIGNED).as_bool();
|
||||
int b_const_int = b_const.as_int(b_const_signed);
|
||||
int c_const_int = c_const.as_int(c_const_signed);
|
||||
int b_const_int_shifted = b_const_int << offset;
|
||||
|
||||
// Helper lambdas for two's complement math
|
||||
auto sign2sComplement = [](auto value, int numBits) {
|
||||
if (value & (1 << (numBits - 1))) {
|
||||
return -1;
|
||||
} else {
|
||||
return 1;
|
||||
}
|
||||
};
|
||||
auto twosComplement = [](auto value, int numBits) {
|
||||
if (value & (1 << (numBits - 1))) {
|
||||
return (~value) + 1; // invert bits before adding 1
|
||||
} else {
|
||||
return value;
|
||||
}
|
||||
};
|
||||
|
||||
// Two's complement conversion
|
||||
if (b_const_signed)
|
||||
b_const_int = sign2sComplement(b_const_int, GetSize(b_const)) * twosComplement(b_const_int, GetSize(b_const));
|
||||
if (c_const_signed)
|
||||
c_const_int = sign2sComplement(c_const_int, GetSize(c_const)) * twosComplement(c_const_int, GetSize(c_const));
|
||||
// Calculate the constant and compress the width to fit the value
|
||||
Const const_value;
|
||||
Const b_const_actual;
|
||||
b_const_actual = b_const_int_shifted;
|
||||
b_const_actual.compress(b_const_signed);
|
||||
|
||||
if (addsub1->type == $add)
|
||||
if (addsub2->type == $add)
|
||||
const_value = b_const_int_shifted + c_const_int;
|
||||
else
|
||||
const_value = b_const_int_shifted - c_const_int;
|
||||
else
|
||||
if (addsub2->type == $add)
|
||||
const_value = b_const_int_shifted - c_const_int;
|
||||
else
|
||||
const_value = b_const_int_shifted + c_const_int;
|
||||
const_value.compress(b_const_signed | c_const_signed);
|
||||
|
||||
// Integer values should be lesser than 32 bits
|
||||
// This is because we are using C++ types, and int is 32 bits
|
||||
// FIXME: use long long or BigInteger to make pass work with >32 bits
|
||||
if (GetSize(addsub1->getParam(ID::B_WIDTH)) > 32)
|
||||
reject;
|
||||
if (GetSize(b_const) > 32)
|
||||
reject;
|
||||
if (GetSize(c_const) + offset > 32)
|
||||
reject;
|
||||
|
||||
// // Check for potential overflow
|
||||
// if (std::max(GetSize(b_const_actual), GetSize(a)) + 1 > GetSize(addsub1_y))
|
||||
// reject;
|
||||
|
||||
// Check that there are only zeros before offset
|
||||
if (offset < 0 || !addsub2_a.extract(0, offset).is_fully_zero())
|
||||
reject;
|
||||
|
||||
// Rewire to only keep addsub1
|
||||
addsub1->setPort(\A, a);
|
||||
addsub1->setPort(\B, const_value);
|
||||
addsub1->setPort(\Y, addsub2_y);
|
||||
|
||||
// Remove addsub2
|
||||
autoremove(addsub2);
|
||||
|
||||
// Log, fixup, accept
|
||||
log("addsub_const pattern in %s: addsub1=%s, addsub2=%s\n", log_id(module), log_id(addsub1), log_id(addsub2));
|
||||
addsub1->fixup_parameters();
|
||||
accept;
|
||||
endcode
|
||||
|
|
@ -0,0 +1,954 @@
|
|||
log -header "Test simple positive case 1"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [31:0] a,
|
||||
output wire [31:0] y
|
||||
);
|
||||
assign y = a + 1023 + 127;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Test simple positive case 2"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [31:0] a,
|
||||
output wire [31:0] y
|
||||
);
|
||||
assign y = a + 1023 - 127;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Test simple positive case 3"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [31:0] a,
|
||||
output wire [31:0] y
|
||||
);
|
||||
assign y = a - 1023 + 127;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 0
|
||||
select t:$sub -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Test simple positive case 4"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [31:0] a,
|
||||
output wire [31:0] y
|
||||
);
|
||||
assign y = a - 1023 - 127;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 0
|
||||
select t:$sub -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
|
||||
|
||||
log -header "Signed pattern transformed: (a +- b) +- c case 1"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + 4'sd6;
|
||||
assign y = add + 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Signed pattern transformed: (a +- b) +- c case 2"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + 4'sd6;
|
||||
assign y = add - 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Signed pattern transformed: (a +- b) +- c case 3"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - 4'sd6;
|
||||
assign y = sub + 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Signed pattern transformed: (a +- b) +- c case 3"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - 4'sd6;
|
||||
assign y = sub - 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
|
||||
|
||||
log -header "Symmetry case 1"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = 4'sd6 + a;
|
||||
assign y = add + 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Symmetry case 2"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = 4'sd6 + a;
|
||||
assign y = add - 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Symmetry case 3: no transformation since constant is first"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = 4'sd6 - a;
|
||||
assign y = sub + 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Symmetry case 4: no transformation since constant is first"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = 4'sd6 - a;
|
||||
assign y = sub - 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 2 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
|
||||
|
||||
log -header "Transformed on b == c case 1"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + 4'sd6;
|
||||
assign y = add + 8'sd6;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Transformed on b == c case 2"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + 4'sd6;
|
||||
assign y = add - 8'sd6;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Transformed on b == c case 3"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - 4'sd6;
|
||||
assign y = sub + 8'sd6;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Transformed on b == c case 4"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - 4'sd6;
|
||||
assign y = sub - 8'sd6;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
|
||||
|
||||
log -header "b negative, c positive case 1"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + (-4'sd6);
|
||||
assign y = add + 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "b negative, c positive case 2"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + (-4'sd6);
|
||||
assign y = add - 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "b negative, c positive case 3"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - (-4'sd6);
|
||||
assign y = sub + 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "b negative, c positive case 4"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - (-4'sd6);
|
||||
assign y = sub - 8'sd3;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
|
||||
|
||||
log -header "No transform when addsub1 has a second fanout case 1"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
output signed [7:0] z,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + 4'sd6;
|
||||
assign y = add + 8'sd3;
|
||||
assign z = add;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$add
|
||||
select -assert-count 0 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "No transform when addsub1 has a second fanout case 2"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
output signed [7:0] z,
|
||||
);
|
||||
wire signed [7:0] add;
|
||||
assign add = a + 4'sd6;
|
||||
assign y = add - 8'sd3;
|
||||
assign z = add;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "No transform when addsub1 has a second fanout case 3"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
output signed [7:0] z,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - 4'sd6;
|
||||
assign y = sub + 8'sd3;
|
||||
assign z = sub;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "No transform when addsub1 has a second fanout case 4"
|
||||
log -push
|
||||
read_verilog <<EOT
|
||||
module top(
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y,
|
||||
output signed [7:0] z,
|
||||
);
|
||||
wire signed [7:0] sub;
|
||||
assign sub = a - 4'sd6;
|
||||
assign y = sub - 8'sd3;
|
||||
assign z = sub;
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select -assert-count 0 t:$add
|
||||
select -assert-count 2 t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
|
||||
|
||||
# =============================================================================
|
||||
# OVERFLOW TESTS
|
||||
# =============================================================================
|
||||
|
||||
log -header "Overflow test: unsigned 4-bit max value + constant"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [3:0] a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
assign y = a + 4'd15 + 4'd1; // 15 + 1 = 16 (overflows 4-bit but not 7-bit)
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Overflow test: signed 4-bit max value + constant"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y
|
||||
);
|
||||
assign y = a + 4'sd7 + 4'sd1; // 7 + 1 = 8 (overflows 4-bit signed but not 7-bit)
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Overflow test: negative signed constants"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input signed [3:0] a,
|
||||
output signed [7:0] y
|
||||
);
|
||||
assign y = a + (-4'sd8) + (-4'sd1); // -8 + (-1) = -9 (underflows 4-bit signed but not 7-bit)
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Large constant test: 32-bit constants"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [31:0] a,
|
||||
output wire [31:0] y
|
||||
);
|
||||
assign y = a + 32'h7FFFFFFF + 32'h1; // Large positive constants
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# SIGNEDNESS MIXING TESTS
|
||||
# =============================================================================
|
||||
|
||||
log -header "Mixed signedness: unsigned input with signed constants"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output signed [15:0] y
|
||||
);
|
||||
wire signed [15:0] temp;
|
||||
assign temp = a + 8'sd10;
|
||||
assign y = temp + 16'sd5;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Mixed signedness: signed input with unsigned constants"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input signed [7:0] a,
|
||||
output wire [15:0] y
|
||||
);
|
||||
wire [15:0] temp;
|
||||
assign temp = a + 8'd10;
|
||||
assign y = temp + 16'd5;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# DRIVING OTHER OPERATIONS TESTS
|
||||
# =============================================================================
|
||||
|
||||
log -header "Result drives multiplication"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
input wire [7:0] b,
|
||||
output wire [15:0] y
|
||||
);
|
||||
wire [7:0] temp;
|
||||
assign temp = a + 8'd10 + 8'd5;
|
||||
assign y = temp * b;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
select t:$mul -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Result drives comparison"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire y
|
||||
);
|
||||
wire [7:0] temp;
|
||||
assign temp = a + 8'd10 + 8'd5;
|
||||
assign y = temp > 8'd100;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
select t:$gt -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Result drives logical operations"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
input wire [7:0] b,
|
||||
output wire [7:0] y
|
||||
);
|
||||
wire [7:0] temp;
|
||||
assign temp = a + 8'd10 + 8'd5;
|
||||
assign y = temp & b;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
select t:$and -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Result drives shift operation"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
wire [7:0] temp;
|
||||
assign temp = a + 8'd10 + 8'd5;
|
||||
assign y = temp << 2;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
select t:$shl -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# WEIRD STRUCTURES AND EDGE CASES
|
||||
# =============================================================================
|
||||
|
||||
log -header "Zero constant optimization"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
assign y = a + 8'd10 + 8'd0; // Should optimize to just a + 10
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Constants that cancel out"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
assign y = a + 8'd10 - 8'd10; // Should optimize to just a
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
# After optimization, this should either be no operations or just a wire connection
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Triple chained operations (optimizes fully)"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
wire [7:0] temp1, temp2;
|
||||
assign temp1 = a + 8'd5;
|
||||
assign temp2 = temp1 + 8'd10;
|
||||
assign y = temp2 + 8'd3;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
# The optimization actually works on multiple levels
|
||||
select t:$add -assert-count 1 // Optimizes to single add (a + 18)
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Different bit widths in chain"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [4:0] a,
|
||||
output wire [15:0] y
|
||||
);
|
||||
wire [10:0] temp;
|
||||
assign temp = a + 5'd10;
|
||||
assign y = temp + 11'd500;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative result from subtraction chain"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input signed [7:0] a,
|
||||
output signed [7:0] y
|
||||
);
|
||||
assign y = a - 8'sd100 - 8'sd50; // Should result in a - 150
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 0
|
||||
select t:$sub -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Mixed add/sub with large intermediate result"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire [15:0] y
|
||||
);
|
||||
wire [15:0] temp;
|
||||
assign temp = a + 8'd255;
|
||||
assign y = temp - 16'd100;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Single bit operations"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
wire [7:0] temp;
|
||||
assign temp = a + 1'd1;
|
||||
assign y = temp + 8'd5;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Constants with different representations (hex, decimal, binary)"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
assign y = a + 8'hFF + 8'b00000001; // 255 + 1 = 256 (overflows to 0 in 8-bit)
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
# =============================================================================
|
||||
# CORNER CASES FOR PATTERN MATCHING
|
||||
# =============================================================================
|
||||
|
||||
log -header "Constants in A position (commutative add)"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [7:0] a,
|
||||
output wire [7:0] y
|
||||
);
|
||||
wire [7:0] temp;
|
||||
assign temp = 8'd10 + a; // Constant first
|
||||
assign y = temp + 8'd5;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Very small bit widths"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top (
|
||||
input wire [1:0] a,
|
||||
output wire [3:0] y
|
||||
);
|
||||
wire [3:0] temp;
|
||||
assign temp = a + 2'd1;
|
||||
assign y = temp + 4'd2;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Test with parameters/generics"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top #(parameter WIDTH = 8) (
|
||||
input wire [WIDTH-1:0] a,
|
||||
output wire [WIDTH+2:0] y
|
||||
);
|
||||
wire [WIDTH+2:0] temp;
|
||||
assign temp = a + 5;
|
||||
assign y = temp + 3;
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
wreduce
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
select t:$add -assert-count 1
|
||||
select t:$sub -assert-count 0
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Final test case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog -sv <<EOF
|
||||
module top (
|
||||
input logic [7:0] var_exp_a,
|
||||
input logic var_zero_a,
|
||||
input logic var_inf_a,
|
||||
output logic var_zero_ac,
|
||||
output logic var_inf_ac,
|
||||
output logic signed [11:0] var_exp_ac
|
||||
);
|
||||
assign var_exp_ac = $signed({1'b0, var_exp_a}) - 1023 + 127;
|
||||
assign var_zero_ac = var_zero_a | (var_exp_ac <= 0);
|
||||
assign var_inf_ac = var_inf_a | (var_exp_ac >= 255);
|
||||
endmodule
|
||||
EOF
|
||||
check -assert
|
||||
equiv_opt -assert peepopt
|
||||
design -load postopt
|
||||
write_verilog test.v
|
||||
select t:$add -assert-count 0
|
||||
select t:$sub -assert-count 1
|
||||
design -reset
|
||||
log -pop
|
||||
Loading…
Reference in New Issue