mirror of https://github.com/YosysHQ/yosys.git
fixed edge cases in negopt passes, fixed cell naming inconsistencies
This commit is contained in:
parent
dc1847f89a
commit
6bb43f109c
|
|
@ -1,24 +1,23 @@
|
|||
/*
|
||||
* Copyright (C) 2025 Silimate, Inc.
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
* Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
|
||||
* Abhinav Tondapu <abhinav@silimate.com>
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
*
|
||||
*/
|
||||
|
||||
//
|
||||
// Authored by Abhinav Tondapu of Silimate, Inc.
|
||||
//
|
||||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/sigtools.h"
|
||||
|
||||
|
|
|
|||
|
|
@ -10,13 +10,15 @@ pattern manual2sub
|
|||
// designs where intermediate results are used by output assignments.
|
||||
//
|
||||
|
||||
state <SigSpec> minuend subtrahend result_sig
|
||||
state <SigSpec> minuend subtrahend result_sig root_a root_b
|
||||
state <bool> is_signed
|
||||
state <SigSpec> inner_y
|
||||
|
||||
// 1. Match the "root" add (the one that produces the final result)
|
||||
match root_add
|
||||
select root_add->type == $add
|
||||
set root_a port(root_add, \A)
|
||||
set root_b port(root_add, \B)
|
||||
set result_sig port(root_add, \Y)
|
||||
set is_signed root_add->getParam(ID::A_SIGNED).as_bool()
|
||||
endmatch
|
||||
|
|
@ -25,8 +27,8 @@ endmatch
|
|||
// Check if root_add has a constant 1
|
||||
code root_add inner_y
|
||||
{
|
||||
SigSpec pa = root_add->getPort(ID::A);
|
||||
SigSpec pb = root_add->getPort(ID::B);
|
||||
SigSpec pa = root_a;
|
||||
SigSpec pb = root_b;
|
||||
|
||||
auto is_one = [](SigSpec s) {
|
||||
if (!s.is_fully_const()) return false;
|
||||
|
|
@ -50,22 +52,18 @@ code root_add inner_y
|
|||
endcode
|
||||
|
||||
// Find the inner add
|
||||
// inner_y is discovered in code so gating happens in the code block
|
||||
match inner_add_A
|
||||
select inner_add_A->type == $add
|
||||
index <SigSpec> port(inner_add_A, \Y) === inner_y
|
||||
select nusers(port(inner_add_A, \Y)) == 2
|
||||
endmatch
|
||||
|
||||
// Find the NOT gate on one of the ports of inner_add_A
|
||||
match not_gate_A
|
||||
select not_gate_A->type == $not
|
||||
filter not_gate_A->getPort(ID::Y) == inner_add_A->getPort(ID::A) || not_gate_A->getPort(ID::Y) == inner_add_A->getPort(ID::B)
|
||||
set subtrahend port(not_gate_A, \A)
|
||||
endmatch
|
||||
|
||||
code root_add inner_add_A not_gate_A subtrahend minuend result_sig is_signed
|
||||
{
|
||||
|
||||
// Require consistent signedness on the root add.
|
||||
if (root_add->getParam(ID::B_SIGNED).as_bool() != is_signed)
|
||||
reject;
|
||||
|
|
@ -75,14 +73,49 @@ code root_add inner_add_A not_gate_A subtrahend minuend result_sig is_signed
|
|||
if (inner_add_A->getParam(ID::B_SIGNED).as_bool() != is_signed)
|
||||
reject;
|
||||
|
||||
if (not_gate_A->getPort(ID::Y) == inner_add_A->getPort(ID::A))
|
||||
if (port(inner_add_A, \Y) != inner_y)
|
||||
reject;
|
||||
if (nusers(port(inner_add_A, \Y)) != 2)
|
||||
reject;
|
||||
|
||||
SigSpec not_y = port(not_gate_A, \Y);
|
||||
SigSpec add_a = port(inner_add_A, \A);
|
||||
SigSpec add_b = port(inner_add_A, \B);
|
||||
|
||||
if (not_y == add_a) {
|
||||
minuend = inner_add_A->getPort(ID::B);
|
||||
else
|
||||
} else if (not_y == add_b) {
|
||||
minuend = inner_add_A->getPort(ID::A);
|
||||
} else {
|
||||
reject;
|
||||
}
|
||||
|
||||
subtrahend = port(not_gate_A, \A);
|
||||
|
||||
// Create the subtraction cell
|
||||
log("manual2sub in %s: Found (a + ~b) + 1 pattern, creating $sub for %s\n", log_id(module), log_signal(result_sig));
|
||||
Cell *sub = module->addSub(NEW_ID, minuend, subtrahend, result_sig, is_signed);
|
||||
Cell *cell = root_add;
|
||||
int width = GetSize(result_sig);
|
||||
int inner_width = GetSize(inner_y);
|
||||
// Reject if the +1 wrap boundary is narrower than the final result
|
||||
if (inner_width < width)
|
||||
reject;
|
||||
SigSpec minuend_rs = minuend;
|
||||
SigSpec subtrahend_rs = subtrahend;
|
||||
// Anchor both operands to the inner add width to preserve carry behavior
|
||||
minuend_rs.extend_u0(inner_width, is_signed);
|
||||
subtrahend_rs.extend_u0(inner_width, is_signed);
|
||||
SigSpec sub_y = result_sig;
|
||||
// Extend the sub result back to the root width when needed
|
||||
if (inner_width != width) {
|
||||
sub_y = module->addWire(NEW_ID2_SUFFIX("sub_y"), inner_width);
|
||||
}
|
||||
Cell *sub = module->addSub(NEW_ID2_SUFFIX("sub"), minuend_rs, subtrahend_rs, sub_y, is_signed);
|
||||
if (inner_width != width) {
|
||||
SigSpec sub_y_rs = sub_y;
|
||||
sub_y_rs.extend_u0(width, is_signed);
|
||||
module->connect(result_sig, sub_y_rs);
|
||||
}
|
||||
|
||||
// Let fixup_parameters handle width adjustments
|
||||
sub->fixup_parameters();
|
||||
|
|
@ -98,26 +131,21 @@ code root_add inner_add_A not_gate_A subtrahend minuend result_sig is_signed
|
|||
endcode
|
||||
|
||||
// 3. Case B: a + (~b + 1)
|
||||
code root_add
|
||||
// Just fall through to the next match
|
||||
endcode
|
||||
|
||||
// Find the inner add on either port of root_add
|
||||
match inner_add_B
|
||||
select inner_add_B->type == $add
|
||||
filter inner_add_B->getPort(ID::Y) == root_add->getPort(ID::A) || inner_add_B->getPort(ID::Y) == root_add->getPort(ID::B)
|
||||
filter port(inner_add_B, \Y) == root_a || port(inner_add_B, \Y) == root_b
|
||||
select nusers(port(inner_add_B, \Y)) == 2
|
||||
endmatch
|
||||
|
||||
// Check if inner_add_B has a constant 1 and a NOT gate
|
||||
match not_gate_B
|
||||
select not_gate_B->type == $not
|
||||
filter not_gate_B->getPort(ID::Y) == inner_add_B->getPort(ID::A) || not_gate_B->getPort(ID::Y) == inner_add_B->getPort(ID::B)
|
||||
endmatch
|
||||
|
||||
code root_add inner_add_B not_gate_B minuend subtrahend result_sig is_signed
|
||||
{
|
||||
|
||||
// Require consistent signedness on the root add.
|
||||
if (root_add->getParam(ID::B_SIGNED).as_bool() != is_signed)
|
||||
reject;
|
||||
|
|
@ -129,7 +157,7 @@ code root_add inner_add_B not_gate_B minuend subtrahend result_sig is_signed
|
|||
|
||||
SigSpec pa = inner_add_B->getPort(ID::A);
|
||||
SigSpec pb = inner_add_B->getPort(ID::B);
|
||||
SigSpec not_y = not_gate_B->getPort(ID::Y);
|
||||
SigSpec not_y = port(not_gate_B, \Y);
|
||||
|
||||
auto is_one = [](SigSpec s) {
|
||||
if (!s.is_fully_const()) return false;
|
||||
|
|
@ -147,15 +175,42 @@ code root_add inner_add_B not_gate_B minuend subtrahend result_sig is_signed
|
|||
|
||||
if (!valid) reject;
|
||||
|
||||
subtrahend = not_gate_B->getPort(ID::A);
|
||||
subtrahend = port(not_gate_B, \A);
|
||||
if (inner_add_B->getPort(ID::Y) == root_add->getPort(ID::A))
|
||||
minuend = root_add->getPort(ID::B);
|
||||
minuend = root_b;
|
||||
else
|
||||
minuend = root_add->getPort(ID::A);
|
||||
minuend = root_a;
|
||||
|
||||
// Create the subtraction cell
|
||||
log("manual2sub in %s: Found a + (~b + 1) pattern, creating $sub for %s\n", log_id(module), log_signal(result_sig));
|
||||
Cell *sub = module->addSub(NEW_ID, minuend, subtrahend, result_sig, is_signed);
|
||||
Cell *cell = root_add;
|
||||
int width = GetSize(result_sig);
|
||||
int inner_width = GetSize(inner_add_B->getPort(ID::Y));
|
||||
|
||||
// Reject if the +1 wrap boundary is narrower than the final result
|
||||
if (inner_width < width)
|
||||
reject;
|
||||
|
||||
SigSpec minuend_rs = minuend;
|
||||
SigSpec subtrahend_rs = subtrahend;
|
||||
|
||||
// Anchor both operands to the inner add width to preserve carry behavior
|
||||
minuend_rs.extend_u0(inner_width, is_signed);
|
||||
subtrahend_rs.extend_u0(inner_width, is_signed);
|
||||
SigSpec sub_y = result_sig;
|
||||
|
||||
// Extend the sub result back to the root width when needed
|
||||
if (inner_width != width) {
|
||||
sub_y = module->addWire(NEW_ID2_SUFFIX("sub_y"), inner_width);
|
||||
}
|
||||
|
||||
Cell *sub = module->addSub(NEW_ID2_SUFFIX("sub"), minuend_rs, subtrahend_rs, sub_y, is_signed);
|
||||
|
||||
if (inner_width != width) {
|
||||
SigSpec sub_y_rs = sub_y;
|
||||
sub_y_rs.extend_u0(width, is_signed);
|
||||
module->connect(result_sig, sub_y_rs);
|
||||
}
|
||||
|
||||
// Let fixup_parameters handle width adjustments
|
||||
sub->fixup_parameters();
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ pattern muxneg
|
|||
// s ? (-a) : (-b) ===> -(s ? a : b)
|
||||
//
|
||||
|
||||
state <SigSpec> mux_a mux_b mux_s mux_y neg_a_in neg_b_in
|
||||
state <SigSpec> mux_a mux_b mux_s mux_y neg_a_in neg_a_y neg_b_in neg_b_y
|
||||
state <bool> neg_a_signed neg_b_signed
|
||||
|
||||
match mux
|
||||
|
|
@ -23,6 +23,7 @@ match neg_a
|
|||
select nusers(port(neg_a, \Y)) == 2
|
||||
index <SigSpec> port(neg_a, \Y) === mux_a
|
||||
set neg_a_in port(neg_a, \A)
|
||||
set neg_a_y port(neg_a, \Y)
|
||||
set neg_a_signed neg_a->getParam(\A_SIGNED).as_bool()
|
||||
endmatch
|
||||
|
||||
|
|
@ -31,19 +32,33 @@ match neg_b
|
|||
select nusers(port(neg_b, \Y)) == 2
|
||||
index <SigSpec> port(neg_b, \Y) === mux_b
|
||||
set neg_b_in port(neg_b, \A)
|
||||
set neg_b_y port(neg_b, \Y)
|
||||
set neg_b_signed neg_b->getParam(\A_SIGNED).as_bool()
|
||||
endmatch
|
||||
|
||||
code mux_a mux_b mux_s mux_y neg_a_in neg_b_in neg_a_signed neg_b_signed
|
||||
code mux_a mux_b mux_s mux_y neg_a_in neg_a_y neg_b_in neg_b_y neg_a_signed neg_b_signed
|
||||
if (neg_a_signed != neg_b_signed)
|
||||
reject;
|
||||
|
||||
{
|
||||
int width = GetSize(mux_y);
|
||||
// Anchor to the narrower negation width to preserve wrap behavior
|
||||
int width = std::min(GetSize(neg_a_y), GetSize(neg_b_y));
|
||||
|
||||
SigSpec mux_out = module->addWire(NEW_ID, width);
|
||||
Cell *new_mux = module->addMux(NEW_ID, neg_a_in, neg_b_in, mux_s, mux_out);
|
||||
Cell *new_neg = module->addNeg(NEW_ID, mux_out, mux_y, neg_a_signed);
|
||||
Cell *cell = mux;
|
||||
SigSpec neg_a_rs = neg_a_in;
|
||||
SigSpec neg_b_rs = neg_b_in;
|
||||
neg_a_rs.extend_u0(width, neg_a_signed);
|
||||
neg_b_rs.extend_u0(width, neg_a_signed);
|
||||
|
||||
SigSpec mux_out = module->addWire(NEW_ID2_SUFFIX("y"), width);
|
||||
Cell *new_mux = module->addMux(NEW_ID2_SUFFIX("mux"), neg_a_rs, neg_b_rs, mux_s, mux_out);
|
||||
SigSpec neg_out = module->addWire(NEW_ID2_SUFFIX("neg_y"), width);
|
||||
Cell *new_neg = module->addNeg(NEW_ID2_SUFFIX("neg"), mux_out, neg_out, neg_a_signed);
|
||||
|
||||
// Extend back to mux output width when needed
|
||||
SigSpec neg_out_rs = neg_out;
|
||||
neg_out_rs.extend_u0(GetSize(mux_y), neg_a_signed);
|
||||
module->connect(mux_y, neg_out_rs);
|
||||
|
||||
log("muxneg pattern in %s: mux=%s, neg_a=%s, neg_b=%s\n",
|
||||
log_id(module), log_id(mux), log_id(neg_a), log_id(neg_b));
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ pattern neg2sub
|
|||
// a + (-b) ===> a - b
|
||||
//
|
||||
|
||||
state <SigSpec> add_a add_b add_y neg_a
|
||||
state <SigSpec> add_a add_b add_y neg_a neg_y
|
||||
state <bool> add_a_signed add_b_signed neg_signed
|
||||
state <bool> neg_on_a
|
||||
|
||||
|
|
@ -31,10 +31,11 @@ match neg
|
|||
select nusers(port(neg, \Y)) == 2
|
||||
index <SigSpec> port(neg, \Y) === (neg_on_a ? add_a : add_b)
|
||||
set neg_a port(neg, \A)
|
||||
set neg_y port(neg, \Y)
|
||||
set neg_signed neg->getParam(\A_SIGNED).as_bool()
|
||||
endmatch
|
||||
|
||||
code add_a add_b add_y neg_a neg_on_a add_a_signed add_b_signed neg_signed
|
||||
code add_a add_b add_y neg_a neg_y neg_on_a add_a_signed add_b_signed neg_signed
|
||||
if (add_a_signed != add_b_signed)
|
||||
reject;
|
||||
|
||||
|
|
@ -42,17 +43,29 @@ code add_a add_b add_y neg_a neg_on_a add_a_signed add_b_signed neg_signed
|
|||
reject;
|
||||
|
||||
{
|
||||
Cell *new_sub;
|
||||
if (neg_on_a)
|
||||
new_sub = module->addSub(NEW_ID, add_b, neg_a, add_y, add_b_signed);
|
||||
else
|
||||
new_sub = module->addSub(NEW_ID, add_a, neg_a, add_y, add_a_signed);
|
||||
int neg_y_width = GetSize(neg_y);
|
||||
int add_y_width = GetSize(add_y);
|
||||
|
||||
log("neg2sub pattern in %s: add=%s, neg=%s\n",
|
||||
// Reject if the negation truncates its input
|
||||
if (GetSize(neg_a) > neg_y_width)
|
||||
reject;
|
||||
|
||||
// Reject if the add result is wider than the negation boundary
|
||||
if (add_y_width > neg_y_width)
|
||||
reject;
|
||||
|
||||
SigSpec pos_op = neg_on_a ? add_b : add_a;
|
||||
|
||||
// Reuse the original add cell for stable naming
|
||||
add->setPort(\A, pos_op);
|
||||
add->setPort(\B, neg_a);
|
||||
add->setPort(\Y, add_y);
|
||||
add->type = $sub;
|
||||
|
||||
log("neg2sub pattern in %s: add=%s, neg=%s (safe sub replacement)\n",
|
||||
log_id(module), log_id(add), log_id(neg));
|
||||
|
||||
new_sub->fixup_parameters();
|
||||
autoremove(add);
|
||||
add->fixup_parameters();
|
||||
autoremove(neg);
|
||||
did_something = true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -32,15 +32,22 @@ code neg_a neg_y add_a add_b a_signed
|
|||
reject;
|
||||
|
||||
{
|
||||
// Use output width for negations to handle overflow correctly
|
||||
// Anchor negations to the original negation width to preserve wrap behavior
|
||||
int width = GetSize(neg_y);
|
||||
SigSpec neg_add_a = module->addWire(NEW_ID, width);
|
||||
Cell *neg_a_cell = module->addNeg(NEW_ID, add_a, neg_add_a, a_signed);
|
||||
Cell *cell = neg;
|
||||
SigSpec add_a_rs = add_a;
|
||||
SigSpec add_b_rs = add_b;
|
||||
// Signedness is consistent for A and B here
|
||||
add_a_rs.extend_u0(width, a_signed);
|
||||
add_b_rs.extend_u0(width, a_signed);
|
||||
|
||||
SigSpec neg_add_b = module->addWire(NEW_ID, width);
|
||||
Cell *neg_b_cell = module->addNeg(NEW_ID, add_b, neg_add_b, a_signed);
|
||||
SigSpec neg_add_a = module->addWire(NEW_ID2_SUFFIX("na"), width);
|
||||
Cell *neg_a_cell = module->addNeg(NEW_ID2_SUFFIX("nega"), add_a_rs, neg_add_a, a_signed);
|
||||
|
||||
Cell *new_add = module->addAdd(NEW_ID, neg_add_a, neg_add_b, neg_y, a_signed);
|
||||
SigSpec neg_add_b = module->addWire(NEW_ID2_SUFFIX("nb"), width);
|
||||
Cell *neg_b_cell = module->addNeg(NEW_ID2_SUFFIX("negb"), add_b_rs, neg_add_b, a_signed);
|
||||
|
||||
Cell *new_add = module->addAdd(NEW_ID2_SUFFIX("add"), neg_add_a, neg_add_b, neg_y, a_signed);
|
||||
|
||||
log("negexpand pattern in %s: neg=%s, add=%s\n",
|
||||
log_id(module), log_id(neg), log_id(add));
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ pattern negmux
|
|||
// -(s ? a : b) ===> s ? (-a) : (-b)
|
||||
//
|
||||
|
||||
state <SigSpec> neg_a neg_y mux_a mux_b mux_s
|
||||
state <SigSpec> neg_a neg_y mux_a mux_b mux_s mux_y
|
||||
state <bool> a_signed
|
||||
|
||||
match neg
|
||||
|
|
@ -18,25 +18,47 @@ match neg
|
|||
endmatch
|
||||
|
||||
match mux
|
||||
select mux->type == $mux
|
||||
index <SigSpec> port(mux, \Y) === neg_a
|
||||
select nusers(port(mux, \Y)) == 2
|
||||
select mux->type == $mux
|
||||
select nusers(port(mux, \Y)) == 2
|
||||
set mux_a port(mux, \A)
|
||||
set mux_b port(mux, \B)
|
||||
set mux_s port(mux, \S)
|
||||
set mux_y port(mux, \Y)
|
||||
endmatch
|
||||
|
||||
code neg_a neg_y mux_a mux_b mux_s a_signed
|
||||
code neg_a neg_y mux_a mux_b mux_s mux_y a_signed
|
||||
// Require neg input to be exactly mux_y or a sign/zero extension of it
|
||||
if (GetSize(neg_a) < GetSize(mux_y))
|
||||
reject;
|
||||
for (int i = 0; i < GetSize(mux_y); i++) {
|
||||
if (neg_a[i] != mux_y[i])
|
||||
reject;
|
||||
}
|
||||
if (GetSize(neg_a) > GetSize(mux_y)) {
|
||||
RTLIL::SigBit ext = a_signed ? mux_y[GetSize(mux_y)-1] : RTLIL::SigBit(RTLIL::State::S0);
|
||||
for (int i = GetSize(mux_y); i < GetSize(neg_a); i++) {
|
||||
if (neg_a[i] != ext)
|
||||
reject;
|
||||
}
|
||||
}
|
||||
|
||||
{
|
||||
// Anchor negations to the original negation width
|
||||
int width = GetSize(neg_y);
|
||||
|
||||
SigSpec neg_mux_a = module->addWire(NEW_ID, width);
|
||||
Cell *neg_a_cell = module->addNeg(NEW_ID, mux_a, neg_mux_a, a_signed);
|
||||
Cell *cell = neg;
|
||||
SigSpec mux_a_rs = mux_a;
|
||||
SigSpec mux_b_rs = mux_b;
|
||||
mux_a_rs.extend_u0(width, a_signed);
|
||||
mux_b_rs.extend_u0(width, a_signed);
|
||||
|
||||
SigSpec neg_mux_b = module->addWire(NEW_ID, width);
|
||||
Cell *neg_b_cell = module->addNeg(NEW_ID, mux_b, neg_mux_b, a_signed);
|
||||
SigSpec neg_mux_a = module->addWire(NEW_ID2_SUFFIX("na"), width);
|
||||
Cell *neg_a_cell = module->addNeg(NEW_ID2_SUFFIX("nega"), mux_a_rs, neg_mux_a, a_signed);
|
||||
|
||||
Cell *new_mux = module->addMux(NEW_ID, neg_mux_a, neg_mux_b, mux_s, neg_y);
|
||||
SigSpec neg_mux_b = module->addWire(NEW_ID2_SUFFIX("nb"), width);
|
||||
Cell *neg_b_cell = module->addNeg(NEW_ID2_SUFFIX("negb"), mux_b_rs, neg_mux_b, a_signed);
|
||||
|
||||
Cell *new_mux = module->addMux(NEW_ID2_SUFFIX("mux"), neg_mux_a, neg_mux_b, mux_s, neg_y);
|
||||
|
||||
log("negmux pattern in %s: neg=%s, mux=%s\n",
|
||||
log_id(module), log_id(neg), log_id(mux));
|
||||
|
|
|
|||
|
|
@ -23,6 +23,10 @@ match neg2
|
|||
endmatch
|
||||
|
||||
code neg1_a neg1_y neg2_a
|
||||
// Reject if inner negation truncates
|
||||
if (GetSize(neg1_a) > GetSize(neg2_a))
|
||||
reject;
|
||||
|
||||
module->connect(neg1_y, neg2_a);
|
||||
|
||||
log("negneg pattern in %s: neg1=%s, neg2=%s\n",
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ pattern negrebuild
|
|||
// (-a) + (-b) ===> -(a + b)
|
||||
//
|
||||
|
||||
state <SigSpec> add_a add_b add_y neg1_a neg2_a
|
||||
state <SigSpec> add_a add_b add_y neg1_a neg1_y neg2_a neg2_y
|
||||
state <bool> add_signed add_b_signed neg1_signed neg2_signed
|
||||
|
||||
match add
|
||||
|
|
@ -22,32 +22,81 @@ endmatch
|
|||
match neg1
|
||||
select neg1->type == $neg
|
||||
select nusers(port(neg1, \Y)) == 2
|
||||
index <SigSpec> port(neg1, \Y) === add_a
|
||||
set neg1_a port(neg1, \A)
|
||||
set neg1_y port(neg1, \Y)
|
||||
set neg1_signed neg1->getParam(\A_SIGNED).as_bool()
|
||||
endmatch
|
||||
|
||||
match neg2
|
||||
select neg2->type == $neg
|
||||
select nusers(port(neg2, \Y)) == 2
|
||||
index <SigSpec> port(neg2, \Y) === add_b
|
||||
set neg2_a port(neg2, \A)
|
||||
set neg2_y port(neg2, \Y)
|
||||
set neg2_signed neg2->getParam(\A_SIGNED).as_bool()
|
||||
endmatch
|
||||
|
||||
code add_a add_b add_y neg1_a neg2_a add_signed add_b_signed neg1_signed neg2_signed
|
||||
code add_a add_b add_y neg1_a neg1_y neg2_a neg2_y add_signed add_b_signed neg1_signed neg2_signed
|
||||
if (add_signed != add_b_signed)
|
||||
reject;
|
||||
|
||||
// Require negations to share the add signedness
|
||||
if (neg1_signed != add_signed || neg2_signed != add_signed)
|
||||
reject;
|
||||
|
||||
{
|
||||
int width = GetSize(add_y);
|
||||
// Avoid matching the same neg cell twice
|
||||
if (neg1 == neg2)
|
||||
reject;
|
||||
|
||||
SigSpec sum = module->addWire(NEW_ID, width);
|
||||
Cell *new_add = module->addAdd(NEW_ID, neg1_a, neg2_a, sum, add_signed);
|
||||
Cell *new_neg = module->addNeg(NEW_ID, sum, add_y, add_signed);
|
||||
// Require a single wrap boundary for both negations and the sum
|
||||
if (GetSize(neg1_y) != GetSize(neg2_y))
|
||||
reject;
|
||||
if (GetSize(add_y) != GetSize(neg1_y))
|
||||
reject;
|
||||
|
||||
// These guards prevent wrap boundary shifts that break formal equivalence
|
||||
|
||||
SigSpec neg_a = neg1_a;
|
||||
SigSpec neg_b = neg2_a;
|
||||
SigSpec neg_a_y = neg1_y;
|
||||
SigSpec neg_b_y = neg2_y;
|
||||
|
||||
SigSpec neg_a_y_ext = neg_a_y;
|
||||
SigSpec neg_b_y_ext = neg_b_y;
|
||||
// Allow add inputs to see sign or zero extensions of neg outputs
|
||||
neg_a_y_ext.extend_u0(GetSize(add_a), add_signed);
|
||||
neg_b_y_ext.extend_u0(GetSize(add_b), add_signed);
|
||||
|
||||
bool direct_match = (add_a == neg_a_y || add_a == neg_a_y_ext) &&
|
||||
(add_b == neg_b_y || add_b == neg_b_y_ext);
|
||||
bool swapped_match = (add_a == neg_b_y || add_a == neg_b_y_ext) &&
|
||||
(add_b == neg_a_y || add_b == neg_a_y_ext);
|
||||
|
||||
if (!direct_match && !swapped_match)
|
||||
reject;
|
||||
|
||||
if (swapped_match) {
|
||||
std::swap(neg_a, neg_b);
|
||||
std::swap(neg_a_y, neg_b_y);
|
||||
}
|
||||
|
||||
// Anchored width matches the common negation boundary
|
||||
int width = std::min(GetSize(neg_a_y), GetSize(neg_b_y));
|
||||
Cell *cell = add;
|
||||
|
||||
SigSpec neg1_a_rs = neg_a;
|
||||
SigSpec neg2_a_rs = neg_b;
|
||||
neg1_a_rs.extend_u0(width, add_signed);
|
||||
neg2_a_rs.extend_u0(width, add_signed);
|
||||
|
||||
SigSpec sum = module->addWire(NEW_ID2_SUFFIX("sum"), width);
|
||||
Cell *new_add = module->addAdd(NEW_ID2_SUFFIX("add"), neg1_a_rs, neg2_a_rs, sum, add_signed);
|
||||
SigSpec neg_out = module->addWire(NEW_ID2_SUFFIX("neg_y"), width);
|
||||
Cell *new_neg = module->addNeg(NEW_ID2_SUFFIX("neg"), sum, neg_out, add_signed);
|
||||
|
||||
SigSpec neg_out_rs = neg_out;
|
||||
neg_out_rs.extend_u0(GetSize(add_y), add_signed);
|
||||
module->connect(add_y, neg_out_rs);
|
||||
|
||||
log("negrebuild pattern in %s: add=%s, neg1=%s, neg2=%s\n",
|
||||
log_id(module), log_id(add), log_id(neg1), log_id(neg2));
|
||||
|
|
|
|||
|
|
@ -26,16 +26,28 @@ code sub_a sub_b sub_y a_signed b_signed
|
|||
|
||||
{
|
||||
int width = GetSize(sub_y);
|
||||
SigSpec neg_y = module->addWire(NEW_ID, width);
|
||||
Cell *neg = module->addNeg(NEW_ID, sub_b, neg_y, b_signed);
|
||||
Cell *add = module->addAdd(NEW_ID, sub_a, neg_y, sub_y, a_signed);
|
||||
|
||||
Cell *cell = sub;
|
||||
SigSpec sub_a_rs = sub_a;
|
||||
SigSpec sub_b_rs = sub_b;
|
||||
// Anchor operands to the original subtract width to preserve wrap behavior
|
||||
sub_a_rs.extend_u0(width, a_signed);
|
||||
sub_b_rs.extend_u0(width, b_signed);
|
||||
|
||||
// Negate within the anchored width, then reuse the original cell as $add
|
||||
SigSpec neg_y = module->addWire(NEW_ID2_SUFFIX("neg_y"), width);
|
||||
Cell *neg = module->addNeg(NEW_ID2_SUFFIX("neg"), sub_b_rs, neg_y, b_signed);
|
||||
|
||||
sub->setPort(\A, sub_a_rs);
|
||||
sub->setPort(\B, neg_y);
|
||||
sub->setPort(\Y, sub_y);
|
||||
sub->type = $add;
|
||||
|
||||
log("sub2neg pattern in %s: sub=%s -> neg=%s, add=%s\n",
|
||||
log_id(module), log_id(sub), log_id(neg), log_id(add));
|
||||
log_id(module), log_id(sub), log_id(neg), log_id(sub));
|
||||
|
||||
sub->fixup_parameters();
|
||||
neg->fixup_parameters();
|
||||
add->fixup_parameters();
|
||||
autoremove(sub);
|
||||
did_something = true;
|
||||
}
|
||||
accept;
|
||||
|
|
|
|||
|
|
@ -21,6 +21,28 @@ select -assert-none t:$sub
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Unsigned positive case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [7:0] y;
|
||||
assign y = (a + ~b) + 1;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$not
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Positive case B: 1 + (a + ~b) => a - b => a + (-b)"
|
||||
log -push
|
||||
design -reset
|
||||
|
|
@ -44,6 +66,26 @@ select -assert-none t:$sub
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Anchor case: output wider than operands"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [11:0] y;
|
||||
assign y = (a + ~b) + 1;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: fanout on inner add output"
|
||||
log -push
|
||||
design -reset
|
||||
|
|
@ -71,3 +113,42 @@ select -assert-none t:$neg
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: mixed signedness on inner add"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire signed [7:0] y;
|
||||
assign y = (a + ~b) + 1;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: ~b not directly on inner add input"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [7:0] y;
|
||||
wire [7:0] nb;
|
||||
assign nb = ~b;
|
||||
assign y = (a + (nb ^ 8'h00)) + 1;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
|
|
@ -42,3 +42,80 @@ select -assert-count 1 t:$mux
|
|||
select -assert-count 1 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Anchor case: neg branches narrower than mux output"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, s, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
input wire s;
|
||||
output wire signed [11:0] y;
|
||||
wire signed [5:0] neg_a;
|
||||
wire signed [7:0] neg_b;
|
||||
assign neg_a = -a[5:0];
|
||||
assign neg_b = -b[7:0];
|
||||
assign y = s ? neg_a : neg_b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$mux
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: signedness mismatch on negations"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, s, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire [7:0] b;
|
||||
input wire s;
|
||||
output wire signed [7:0] y;
|
||||
(* keep *) wire signed [7:0] neg_a;
|
||||
(* keep *) wire [7:0] neg_b;
|
||||
assign neg_a = -a;
|
||||
assign neg_b = -b;
|
||||
assign y = s ? neg_a : neg_b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$mux
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: neg output has extra fanout"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, s, y, z);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
input wire s;
|
||||
output wire signed [7:0] y;
|
||||
output wire signed [7:0] z;
|
||||
(* keep *) wire signed [7:0] neg_a;
|
||||
(* keep *) wire signed [7:0] neg_b;
|
||||
assign neg_a = -a;
|
||||
assign neg_b = -b;
|
||||
assign y = s ? neg_a : neg_b;
|
||||
assign z = neg_a;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$mux
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ read_verilog <<EOF
|
|||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
output wire signed [8:0] y;
|
||||
output wire signed [7:0] y;
|
||||
assign y = a + (-b);
|
||||
endmodule
|
||||
EOF
|
||||
|
|
@ -26,7 +26,7 @@ read_verilog <<EOF
|
|||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
output wire signed [8:0] y;
|
||||
output wire signed [7:0] y;
|
||||
assign y = (-a) + b;
|
||||
endmodule
|
||||
EOF
|
||||
|
|
@ -39,3 +39,95 @@ select -assert-none t:$add
|
|||
select -assert-none t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Unsigned positive case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [7:0] y;
|
||||
assign y = a + (-b);
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$sub
|
||||
select -assert-none t:$add
|
||||
select -assert-none t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: output wider than negation"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
output wire signed [8:0] y;
|
||||
wire signed [7:0] nb;
|
||||
assign nb = -b;
|
||||
assign y = a + nb;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: negation truncates input"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
output wire signed [3:0] y;
|
||||
wire signed [3:0] nb;
|
||||
assign nb = -b;
|
||||
assign y = a[3:0] + nb;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: neg output has extra fanout"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y, z);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
output wire signed [7:0] y;
|
||||
output wire signed [7:0] z;
|
||||
(* keep *) wire signed [7:0] nb;
|
||||
assign nb = -b;
|
||||
assign y = a + nb;
|
||||
assign z = nb;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
|
|
@ -18,6 +18,26 @@ select -assert-count 2 t:$neg
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Unsigned positive case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [7:0] y;
|
||||
assign y = -(a + b);
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Width extension case (output wider than inputs)"
|
||||
log -push
|
||||
design -reset
|
||||
|
|
@ -39,6 +59,26 @@ select -assert-count 2 t:$neg
|
|||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Anchor case: inputs narrower than neg output"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [3:0] a;
|
||||
input wire signed [3:0] b;
|
||||
output wire signed [7:0] y;
|
||||
assign y = -(a + b);
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: fanout on add output"
|
||||
log -push
|
||||
design -reset
|
||||
|
|
@ -63,3 +103,23 @@ select -assert-count 1 t:$add
|
|||
select -assert-count 1 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Coerced signedness case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire signed [7:0] y;
|
||||
assign y = -(a + b);
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
|
|
@ -67,3 +67,72 @@ select -assert-count 1 t:$mux
|
|||
select -assert-count 1 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Anchor case: mux inputs narrower than neg output"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, s, y);
|
||||
input wire signed [3:0] a;
|
||||
input wire signed [3:0] b;
|
||||
input wire s;
|
||||
output wire signed [7:0] y;
|
||||
wire signed [3:0] m;
|
||||
assign m = s ? a : b;
|
||||
assign y = -m;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$mux
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: signedness mismatch on mux output"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, s, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire [7:0] b;
|
||||
input wire s;
|
||||
output wire signed [7:0] y;
|
||||
wire [7:0] m;
|
||||
assign m = s ? a : b;
|
||||
assign y = -m;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$mux
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: neg input not from mux output"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, s, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
input wire s;
|
||||
output wire signed [7:0] y;
|
||||
wire signed [7:0] m;
|
||||
assign m = s ? a : b;
|
||||
assign y = -(m ^ 8'h00);
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$mux
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
|
|
@ -58,3 +58,23 @@ design -load postopt
|
|||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Anchor case: inner neg truncates"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, y);
|
||||
input wire signed [7:0] a;
|
||||
output wire signed [6:0] y;
|
||||
wire signed [6:0] neg_a;
|
||||
assign neg_a = -a;
|
||||
assign y = -neg_a;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
|
|
@ -15,5 +15,96 @@ equiv_opt -assert negopt -post
|
|||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Unsigned positive case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [7:0] y;
|
||||
assign y = (-a) + (-b);
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Anchor case: neg branches with different widths"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [9:0] b;
|
||||
output wire signed [11:0] y;
|
||||
wire signed [5:0] n1;
|
||||
wire signed [7:0] n2;
|
||||
assign n1 = -a[5:0];
|
||||
assign n2 = -b[7:0];
|
||||
assign y = n1 + n2;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: signedness mismatch on negations"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire signed [7:0] y;
|
||||
assign y = (-a) + (-b);
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Negative case: add input not direct neg output"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
output wire signed [7:0] y;
|
||||
wire signed [7:0] na;
|
||||
wire signed [7:0] nb;
|
||||
assign na = -a;
|
||||
assign nb = -b;
|
||||
assign y = (na ^ 8'h00) + nb;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -post
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 2 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
|
|
@ -9,6 +9,28 @@ module top(a, b, y);
|
|||
assign y = a - b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Unsigned positive case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire [7:0] y;
|
||||
assign y = a - b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
|
|
@ -28,6 +50,7 @@ module top(a, y);
|
|||
assign y = a - 8'd5;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
|
|
@ -37,3 +60,45 @@ select -assert-none t:$add
|
|||
select -assert-none t:$neg
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Anchor case: output wider than inputs"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire signed [7:0] b;
|
||||
output wire signed [11:0] y;
|
||||
assign y = a - b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
||||
log -header "Signedness case"
|
||||
log -push
|
||||
design -reset
|
||||
read_verilog <<EOF
|
||||
module top(a, b, y);
|
||||
input wire signed [7:0] a;
|
||||
input wire [7:0] b;
|
||||
output wire signed [7:0] y;
|
||||
assign y = a - b;
|
||||
endmodule
|
||||
EOF
|
||||
proc; opt
|
||||
check -assert
|
||||
equiv_opt -assert negopt -pre
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$neg
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
log -pop
|
||||
|
|
|
|||
Loading…
Reference in New Issue