mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-01-28 12:58:44 +00:00
Code Activity

satgen, calc: $priority perform more x-bit horrors

Browse source
This commit is contained in:
Emil J. Tywoniak 2026-01-21 11:50:45 +01:00
parent 6a5d74d252
commit 1d468962b7
2 changed files with 24 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

27
kernel/calc.cc
View file

@ -660,21 +660,22 @@ RTLIL::Const RTLIL::const_bmux(const RTLIL::Const &arg1, const RTLIL::Const &arg
RTLIL::Const RTLIL::const_priority(const RTLIL::Const &arg, const RTLIL::Const &polarity)
{
std::vector<State> t;
std::optional<State> first_non_zero = std::nullopt;
for (int i = 0; i < GetSize(arg); i++)
std::vector<RTLIL::State> t;
RTLIL::State previous;
if (GetSize(arg)) {
RTLIL::State s = arg.at(0);
t.push_back(s);
previous = polarity[0] ? s : const_not(s, Const(), false, false, 1)[0];
}
for (int i = 1; i < GetSize(arg); i++)
{
RTLIL::State s = arg.at(i);
if (first_non_zero && s != State::Sx) {
auto inactive = polarity[i] == State::S0 ? State::S1 : State::S0;
auto val = *first_non_zero == State::Sx ? State::Sx : inactive;
t.push_back(val);
} else {
t.push_back(s);
}
if ((!first_non_zero && s == polarity[i]) || s == State::Sx) {
first_non_zero = s;
}
RTLIL::State is_active = const_xnor(s, polarity[i], false, false, 1)[0];
RTLIL::State next = const_or(is_active, previous, false, false, 1)[0];
RTLIL::State inactive_polarity = const_not(polarity[i], Const(), false, false, 1)[0];
RTLIL::State y = const_mux(s, inactive_polarity, previous)[0];
t.push_back(y);
previous = next;
}
return t;
}

13
kernel/satgen.cc
View file

@ -460,13 +460,20 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
}
for (size_t i = 1; i < a.size(); i++) {
int inactive_val = !polarity[i] ? ez->CONST_TRUE : ez->CONST_FALSE;
// $mux emulation
int is_active = ez->XOR(inactive_val, a[i]);
int undef_because_s = ez->AND(any_previous_undef, ez->OR(is_active, undef_a[i]));
int is_not_inactive = ez->OR(is_active, undef_a[i]);
int is_not_active = ez->OR(ez->NOT(is_active), undef_a[i]);
// $mux
int undef_because_s = ez->AND(any_previous_undef, is_not_inactive);
int undef_because_a = ez->AND(ez->OR(any_previous_undef, ez->NOT(active_so_far[i-1])), undef_a[i]);
int undef = ez->OR(undef_because_s, undef_because_a);
any_previous_undef = ez->AND(ez->NOT(is_active), ez->OR(any_previous_undef, undef_a[i]));
ez->assume(ez->IFF(undef_y[i], undef));
// $or
int next_previous_undef_because_previous = ez->AND(any_previous_undef, is_not_active);
int next_previous_undef_because_a = ez->AND(ez->NOT(active_so_far[i-1]), undef_a[i]);
any_previous_undef = ez->OR(next_previous_undef_because_previous, next_previous_undef_because_a);
}
undefGating(y, yy, undef_y);
}