mirror of
https://github.com/YosysHQ/yosys
synced 2025-05-10 09:15:49 +00:00
Merge 390ff5501d
into 5aa9bfbf7d
This commit is contained in:
commit
f3b02fdede
3 changed files with 653 additions and 234 deletions
|
@ -29,6 +29,7 @@
|
||||||
#include "passes/techmap/simplemap.h"
|
#include "passes/techmap/simplemap.h"
|
||||||
#include <stdio.h>
|
#include <stdio.h>
|
||||||
#include <stdlib.h>
|
#include <stdlib.h>
|
||||||
|
#include <optional>
|
||||||
|
|
||||||
USING_YOSYS_NAMESPACE
|
USING_YOSYS_NAMESPACE
|
||||||
PRIVATE_NAMESPACE_BEGIN
|
PRIVATE_NAMESPACE_BEGIN
|
||||||
|
@ -95,6 +96,18 @@ struct OptDffWorker
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// If this bit sigmaps to a bit driven by a mux ouput bit that only drives this
|
||||||
|
// bit, returns that mux otherwise nullopt
|
||||||
|
std::optional<cell_int_t> mergeable_mux(SigBit bit) {
|
||||||
|
sigmap.apply(bit);
|
||||||
|
auto it = bit2mux.find(bit);
|
||||||
|
|
||||||
|
if (it == bit2mux.end() || bitusers[bit] != 1)
|
||||||
|
return std::nullopt;
|
||||||
|
|
||||||
|
return it->second;
|
||||||
|
}
|
||||||
|
|
||||||
State combine_const(State a, State b) {
|
State combine_const(State a, State b) {
|
||||||
if (a == State::Sx && !opt.keepdc)
|
if (a == State::Sx && !opt.keepdc)
|
||||||
return b;
|
return b;
|
||||||
|
@ -591,13 +604,12 @@ struct OptDffWorker
|
||||||
State reset_val = State::Sx;
|
State reset_val = State::Sx;
|
||||||
if (ff.has_srst)
|
if (ff.has_srst)
|
||||||
reset_val = ff.val_srst[i];
|
reset_val = ff.val_srst[i];
|
||||||
while (bit2mux.count(ff.sig_d[i]) && bitusers[ff.sig_d[i]] == 1) {
|
while (const auto mbit = mergeable_mux(ff.sig_d[i])) {
|
||||||
cell_int_t mbit = bit2mux.at(ff.sig_d[i]);
|
if (GetSize(mbit->first->getPort(ID::S)) != 1)
|
||||||
if (GetSize(mbit.first->getPort(ID::S)) != 1)
|
|
||||||
break;
|
break;
|
||||||
SigBit s = mbit.first->getPort(ID::S);
|
SigBit s = mbit->first->getPort(ID::S);
|
||||||
SigBit a = mbit.first->getPort(ID::A)[mbit.second];
|
SigBit a = mbit->first->getPort(ID::A)[mbit->second];
|
||||||
SigBit b = mbit.first->getPort(ID::B)[mbit.second];
|
SigBit b = mbit->first->getPort(ID::B)[mbit->second];
|
||||||
// Workaround for funny memory WE pattern.
|
// Workaround for funny memory WE pattern.
|
||||||
if ((a == State::S0 || a == State::S1) && (b == State::S0 || b == State::S1))
|
if ((a == State::S0 || a == State::S1) && (b == State::S0 || b == State::S1))
|
||||||
break;
|
break;
|
||||||
|
@ -668,13 +680,12 @@ struct OptDffWorker
|
||||||
for (int i = 0 ; i < ff.width; i++) {
|
for (int i = 0 ; i < ff.width; i++) {
|
||||||
// First, eat up as many simple muxes as possible.
|
// First, eat up as many simple muxes as possible.
|
||||||
ctrls_t enables;
|
ctrls_t enables;
|
||||||
while (bit2mux.count(ff.sig_d[i]) && bitusers[ff.sig_d[i]] == 1) {
|
while (const auto mbit = mergeable_mux(ff.sig_d[i])) {
|
||||||
cell_int_t mbit = bit2mux.at(ff.sig_d[i]);
|
if (GetSize(mbit->first->getPort(ID::S)) != 1)
|
||||||
if (GetSize(mbit.first->getPort(ID::S)) != 1)
|
|
||||||
break;
|
break;
|
||||||
SigBit s = mbit.first->getPort(ID::S);
|
SigBit s = mbit->first->getPort(ID::S);
|
||||||
SigBit a = mbit.first->getPort(ID::A)[mbit.second];
|
SigBit a = mbit->first->getPort(ID::A)[mbit->second];
|
||||||
SigBit b = mbit.first->getPort(ID::B)[mbit.second];
|
SigBit b = mbit->first->getPort(ID::B)[mbit->second];
|
||||||
if (a == ff.sig_q[i]) {
|
if (a == ff.sig_q[i]) {
|
||||||
enables.insert(ctrl_t(s, true));
|
enables.insert(ctrl_t(s, true));
|
||||||
ff.sig_d[i] = b;
|
ff.sig_d[i] = b;
|
||||||
|
|
|
@ -24,25 +24,27 @@
|
||||||
#include <sstream>
|
#include <sstream>
|
||||||
#include <stdlib.h>
|
#include <stdlib.h>
|
||||||
#include <stdio.h>
|
#include <stdio.h>
|
||||||
|
#include <algorithm>
|
||||||
|
#include <type_traits>
|
||||||
|
|
||||||
USING_YOSYS_NAMESPACE
|
USING_YOSYS_NAMESPACE
|
||||||
PRIVATE_NAMESPACE_BEGIN
|
PRIVATE_NAMESPACE_BEGIN
|
||||||
|
|
||||||
RTLIL::SigSpec find_any_lvalue(const RTLIL::Process *proc)
|
RTLIL::SigSpec find_any_lvalue(const RTLIL::Process& proc)
|
||||||
{
|
{
|
||||||
RTLIL::SigSpec lvalue;
|
RTLIL::SigSpec lvalue;
|
||||||
|
|
||||||
for (auto sync : proc->syncs)
|
for (const auto* sync : proc.syncs)
|
||||||
for (auto &action : sync->actions)
|
for (const auto& action : sync->actions)
|
||||||
if (action.first.size() > 0) {
|
if (action.first.size() > 0) {
|
||||||
lvalue = action.first;
|
lvalue = action.first;
|
||||||
lvalue.sort_and_unify();
|
lvalue.sort_and_unify();
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
||||||
for (auto sync : proc->syncs) {
|
for (const auto* sync : proc.syncs) {
|
||||||
RTLIL::SigSpec this_lvalue;
|
RTLIL::SigSpec this_lvalue;
|
||||||
for (auto &action : sync->actions)
|
for (const auto& action : sync->actions)
|
||||||
this_lvalue.append(action.first);
|
this_lvalue.append(action.first);
|
||||||
this_lvalue.sort_and_unify();
|
this_lvalue.sort_and_unify();
|
||||||
RTLIL::SigSpec common_sig = this_lvalue.extract(lvalue);
|
RTLIL::SigSpec common_sig = this_lvalue.extract(lvalue);
|
||||||
|
@ -53,238 +55,452 @@ RTLIL::SigSpec find_any_lvalue(const RTLIL::Process *proc)
|
||||||
return lvalue;
|
return lvalue;
|
||||||
}
|
}
|
||||||
|
|
||||||
void gen_dffsr_complex(RTLIL::Module *mod, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, RTLIL::SigSpec clk, bool clk_polarity,
|
std::string new_dff_name() {
|
||||||
std::vector<std::pair<RTLIL::SigSpec, RTLIL::SyncRule*>> &async_rules, RTLIL::Process *proc)
|
std::stringstream sstr;
|
||||||
{
|
sstr << "$procdff$" << (autoidx++);
|
||||||
// A signal should be set/cleared if there is a load trigger that is enabled
|
return sstr.str();
|
||||||
// such that the load value is 1/0 and it is the highest priority trigger
|
}
|
||||||
RTLIL::SigSpec sig_sr_set = RTLIL::SigSpec(0, sig_d.size());
|
|
||||||
RTLIL::SigSpec sig_sr_clr = RTLIL::SigSpec(0, sig_d.size());
|
|
||||||
|
|
||||||
// Reverse iterate through the rules as the first ones are the highest priority
|
class Dff {
|
||||||
// so need to be at the top of the mux trees
|
public:
|
||||||
for (auto it = async_rules.crbegin(); it != async_rules.crend(); it++)
|
// Extract the relevant signals from a process that drives sig as a DFF
|
||||||
|
Dff(RTLIL::Module& mod, const SigSpec& sig_out, RTLIL::Process& proc) :
|
||||||
|
proc{proc}, mod{mod}, sig_in(RTLIL::State::Sz, sig_out.size()), sig_out{sig_out}
|
||||||
{
|
{
|
||||||
const auto& [sync_value, rule] = *it;
|
// We gather sync rules corresponding to always/edge first to check
|
||||||
const auto pos_trig = rule->type == RTLIL::SyncType::ST1 ? rule->signal : mod->Not(NEW_ID, rule->signal);
|
// whether they are conflicting before actually updating clk
|
||||||
|
const RTLIL::SyncRule* sync_edge = nullptr;
|
||||||
// If pos_trig is true, we have priority at this point in the tree so
|
const RTLIL::SyncRule* sync_always = nullptr;
|
||||||
// set a bit if sync_value has a set bit. Otherwise, defer to the rest
|
|
||||||
// of the priority tree
|
|
||||||
sig_sr_set = mod->Mux(NEW_ID, sig_sr_set, sync_value, pos_trig);
|
|
||||||
|
|
||||||
// Same deal with clear bit
|
|
||||||
const auto sync_value_inv = mod->Not(NEW_ID, sync_value);
|
|
||||||
sig_sr_clr = mod->Mux(NEW_ID, sig_sr_clr, sync_value_inv, pos_trig);
|
|
||||||
}
|
|
||||||
|
|
||||||
std::stringstream sstr;
|
|
||||||
sstr << "$procdff$" << (autoidx++);
|
|
||||||
|
|
||||||
RTLIL::Cell *cell = mod->addDffsr(sstr.str(), clk, sig_sr_set, sig_sr_clr, sig_d, sig_q, clk_polarity);
|
|
||||||
cell->attributes = proc->attributes;
|
|
||||||
|
|
||||||
log(" created %s cell `%s' with %s edge clock and multiple level-sensitive resets.\n",
|
|
||||||
cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative");
|
|
||||||
}
|
|
||||||
|
|
||||||
void gen_aldff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_out,
|
|
||||||
bool clk_polarity, bool set_polarity, RTLIL::SigSpec clk, RTLIL::SigSpec set, RTLIL::Process *proc)
|
|
||||||
{
|
|
||||||
std::stringstream sstr;
|
|
||||||
sstr << "$procdff$" << (autoidx++);
|
|
||||||
|
|
||||||
RTLIL::Cell *cell = mod->addCell(sstr.str(), ID($aldff));
|
|
||||||
cell->attributes = proc->attributes;
|
|
||||||
|
|
||||||
cell->parameters[ID::WIDTH] = RTLIL::Const(sig_in.size());
|
|
||||||
cell->parameters[ID::ALOAD_POLARITY] = RTLIL::Const(set_polarity, 1);
|
|
||||||
cell->parameters[ID::CLK_POLARITY] = RTLIL::Const(clk_polarity, 1);
|
|
||||||
cell->setPort(ID::D, sig_in);
|
|
||||||
cell->setPort(ID::Q, sig_out);
|
|
||||||
cell->setPort(ID::AD, sig_set);
|
|
||||||
cell->setPort(ID::CLK, clk);
|
|
||||||
cell->setPort(ID::ALOAD, set);
|
|
||||||
|
|
||||||
log(" created %s cell `%s' with %s edge clock and %s level non-const reset.\n", cell->type.c_str(), cell->name.c_str(),
|
|
||||||
clk_polarity ? "positive" : "negative", set_polarity ? "positive" : "negative");
|
|
||||||
}
|
|
||||||
|
|
||||||
void gen_dff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::Const val_rst, RTLIL::SigSpec sig_out,
|
|
||||||
bool clk_polarity, bool arst_polarity, RTLIL::SigSpec clk, RTLIL::SigSpec *arst, RTLIL::Process *proc)
|
|
||||||
{
|
|
||||||
std::stringstream sstr;
|
|
||||||
sstr << "$procdff$" << (autoidx++);
|
|
||||||
|
|
||||||
RTLIL::Cell *cell = mod->addCell(sstr.str(), clk.empty() ? ID($ff) : arst ? ID($adff) : ID($dff));
|
|
||||||
cell->attributes = proc->attributes;
|
|
||||||
|
|
||||||
cell->parameters[ID::WIDTH] = RTLIL::Const(sig_in.size());
|
|
||||||
if (arst) {
|
|
||||||
cell->parameters[ID::ARST_POLARITY] = RTLIL::Const(arst_polarity, 1);
|
|
||||||
cell->parameters[ID::ARST_VALUE] = val_rst;
|
|
||||||
}
|
|
||||||
if (!clk.empty()) {
|
|
||||||
cell->parameters[ID::CLK_POLARITY] = RTLIL::Const(clk_polarity, 1);
|
|
||||||
}
|
|
||||||
|
|
||||||
cell->setPort(ID::D, sig_in);
|
|
||||||
cell->setPort(ID::Q, sig_out);
|
|
||||||
if (arst)
|
|
||||||
cell->setPort(ID::ARST, *arst);
|
|
||||||
if (!clk.empty())
|
|
||||||
cell->setPort(ID::CLK, clk);
|
|
||||||
|
|
||||||
if (!clk.empty())
|
|
||||||
log(" created %s cell `%s' with %s edge clock", cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative");
|
|
||||||
else
|
|
||||||
log(" created %s cell `%s' with global clock", cell->type.c_str(), cell->name.c_str());
|
|
||||||
if (arst)
|
|
||||||
log(" and %s level reset", arst_polarity ? "positive" : "negative");
|
|
||||||
log(".\n");
|
|
||||||
}
|
|
||||||
|
|
||||||
void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
|
|
||||||
{
|
|
||||||
while (1)
|
|
||||||
{
|
|
||||||
RTLIL::SigSpec sig = find_any_lvalue(proc);
|
|
||||||
|
|
||||||
if (sig.size() == 0)
|
|
||||||
break;
|
|
||||||
|
|
||||||
log("Creating register for signal `%s.%s' using process `%s.%s'.\n",
|
|
||||||
mod->name.c_str(), log_signal(sig), mod->name.c_str(), proc->name.c_str());
|
|
||||||
|
|
||||||
RTLIL::SigSpec insig = RTLIL::SigSpec(RTLIL::State::Sz, sig.size());
|
|
||||||
RTLIL::SyncRule *sync_edge = NULL;
|
|
||||||
RTLIL::SyncRule *sync_always = NULL;
|
|
||||||
bool global_clock = false;
|
bool global_clock = false;
|
||||||
|
|
||||||
// A priority ordered set of rules, pairing the value to be assigned for
|
for (const auto* sync : proc.syncs)
|
||||||
// that rule to the rule
|
for (const auto& action : sync->actions) {
|
||||||
std::vector<std::pair<RTLIL::SigSpec, RTLIL::SyncRule*>> async_rules;
|
if (action.first.extract(sig_out).empty())
|
||||||
|
|
||||||
// Needed when the async rules are collapsed into one as async_rules
|
|
||||||
// works with pointers to SyncRule
|
|
||||||
RTLIL::SyncRule single_async_rule;
|
|
||||||
|
|
||||||
for (auto sync : proc->syncs)
|
|
||||||
for (auto &action : sync->actions)
|
|
||||||
{
|
|
||||||
if (action.first.extract(sig).size() == 0)
|
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
|
// Level sensitive assignments (set/reset/aload)
|
||||||
if (sync->type == RTLIL::SyncType::ST0 || sync->type == RTLIL::SyncType::ST1) {
|
if (sync->type == RTLIL::SyncType::ST0 || sync->type == RTLIL::SyncType::ST1) {
|
||||||
RTLIL::SigSpec rstval = RTLIL::SigSpec(RTLIL::State::Sz, sig.size());
|
RTLIL::SigSpec rstval(RTLIL::State::Sz, sig_out.size());
|
||||||
sig.replace(action.first, action.second, &rstval);
|
sig_out.replace(action.first, action.second, &rstval);
|
||||||
async_rules.emplace_back(rstval, sync);
|
async_rules.emplace_back(rstval, *sync);
|
||||||
|
continue;
|
||||||
}
|
}
|
||||||
else if (sync->type == RTLIL::SyncType::STp || sync->type == RTLIL::SyncType::STn) {
|
|
||||||
|
// Edge sensitive assignments (clock)
|
||||||
|
if (sync->type == RTLIL::SyncType::STp || sync->type == RTLIL::SyncType::STn) {
|
||||||
if (sync_edge != NULL && sync_edge != sync)
|
if (sync_edge != NULL && sync_edge != sync)
|
||||||
log_error("Multiple edge sensitive events found for this signal!\n");
|
log_error("Multiple edge sensitive events found for this signal!\n");
|
||||||
sig.replace(action.first, action.second, &insig);
|
sig_out.replace(action.first, action.second, &sig_in);
|
||||||
sync_edge = sync;
|
sync_edge = sync;
|
||||||
|
continue;
|
||||||
}
|
}
|
||||||
else if (sync->type == RTLIL::SyncType::STa) {
|
|
||||||
|
// Always assignments
|
||||||
|
if (sync->type == RTLIL::SyncType::STa) {
|
||||||
if (sync_always != NULL && sync_always != sync)
|
if (sync_always != NULL && sync_always != sync)
|
||||||
log_error("Multiple always events found for this signal!\n");
|
log_error("Multiple always events found for this signal!\n");
|
||||||
sig.replace(action.first, action.second, &insig);
|
sig_out.replace(action.first, action.second, &sig_in);
|
||||||
sync_always = sync;
|
sync_always = sync;
|
||||||
|
continue;
|
||||||
}
|
}
|
||||||
else if (sync->type == RTLIL::SyncType::STg) {
|
|
||||||
sig.replace(action.first, action.second, &insig);
|
// Global clock assignments
|
||||||
|
if (sync->type == RTLIL::SyncType::STg) {
|
||||||
|
sig_out.replace(action.first, action.second, &sig_in);
|
||||||
global_clock = true;
|
global_clock = true;
|
||||||
|
continue;
|
||||||
}
|
}
|
||||||
else {
|
|
||||||
log_error("Event with any-edge sensitivity found for this signal!\n");
|
log_error("Event with any-edge sensitivity found for this signal!\n");
|
||||||
}
|
}
|
||||||
|
|
||||||
action.first.remove2(sig, &action.second);
|
if (sync_always && (sync_edge || !async_rules.empty()))
|
||||||
}
|
|
||||||
|
|
||||||
// If all async rules assign the same value, priority ordering between
|
|
||||||
// them doesn't matter so they can be collapsed together into one rule
|
|
||||||
// with the disjunction of triggers
|
|
||||||
if (!async_rules.empty() &&
|
|
||||||
std::all_of(async_rules.begin(), async_rules.end(), [&](auto& p) {
|
|
||||||
return p.first == async_rules.front().first;
|
|
||||||
}))
|
|
||||||
{
|
|
||||||
const auto rstval = async_rules.front().first;
|
|
||||||
|
|
||||||
// The trigger is the disjunction of existing triggers
|
|
||||||
// (with appropriate negation)
|
|
||||||
RTLIL::SigSpec triggers;
|
|
||||||
for (const auto &[_, it] : async_rules)
|
|
||||||
triggers.append(it->type == RTLIL::SyncType::ST1 ? it->signal : mod->Not(NEW_ID, it->signal));
|
|
||||||
|
|
||||||
// Put this into the dummy sync rule so it can be treated the same
|
|
||||||
// as ones coming from the module
|
|
||||||
single_async_rule.type = RTLIL::SyncType::ST1;
|
|
||||||
single_async_rule.signal = mod->ReduceOr(NEW_ID, triggers);
|
|
||||||
single_async_rule.actions.push_back(RTLIL::SigSig(sig, rstval));
|
|
||||||
|
|
||||||
// Replace existing rules with this new rule
|
|
||||||
async_rules.clear();
|
|
||||||
async_rules.emplace_back(rstval, &single_async_rule);
|
|
||||||
}
|
|
||||||
|
|
||||||
SigSpec sig_q = sig;
|
|
||||||
ce.assign_map.apply(insig);
|
|
||||||
ce.assign_map.apply(sig);
|
|
||||||
|
|
||||||
// If the reset value assigns the reg to itself, add this as part of
|
|
||||||
// the input signal and delete the rule
|
|
||||||
if (async_rules.size() == 1 && async_rules.front().first == sig) {
|
|
||||||
const auto& [_, rule] = async_rules.front();
|
|
||||||
if (rule->type == RTLIL::SyncType::ST1)
|
|
||||||
insig = mod->Mux(NEW_ID, insig, sig, rule->signal);
|
|
||||||
else
|
|
||||||
insig = mod->Mux(NEW_ID, sig, insig, rule->signal);
|
|
||||||
|
|
||||||
async_rules.clear();
|
|
||||||
}
|
|
||||||
|
|
||||||
if (sync_always) {
|
|
||||||
if (sync_edge || !async_rules.empty())
|
|
||||||
log_error("Mixed always event with edge and/or level sensitive events!\n");
|
log_error("Mixed always event with edge and/or level sensitive events!\n");
|
||||||
log(" created direct connection (no actual register cell created).\n");
|
|
||||||
mod->connect(RTLIL::SigSig(sig, insig));
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (!sync_edge && !global_clock)
|
if (!sync_edge && !global_clock && !sync_always)
|
||||||
log_error("Missing edge-sensitive event for this signal!\n");
|
log_error("Missing edge-sensitive event for this signal!\n");
|
||||||
|
|
||||||
// More than one reset value so we derive a dffsr formulation
|
// Update our internal versions of these signals to track whether things
|
||||||
if (async_rules.size() > 1)
|
// are edge sensitive
|
||||||
{
|
if (sync_edge)
|
||||||
log_warning("Complex async reset for dff `%s'.\n", log_signal(sig));
|
clk = *sync_edge;
|
||||||
gen_dffsr_complex(mod, insig, sig, sync_edge->signal, sync_edge->type == RTLIL::SyncType::STp, async_rules, proc);
|
always = sync_always != nullptr;
|
||||||
|
}
|
||||||
|
|
||||||
|
void optimize(ConstEval& ce) {
|
||||||
|
optimize_const_eval(ce);
|
||||||
|
optimize_same_value(ce);
|
||||||
|
optimize_self_assign(ce);
|
||||||
|
optimize_single_rule_consts();
|
||||||
|
}
|
||||||
|
|
||||||
|
// Const evaluate async rule values and triggers, and remove those that
|
||||||
|
// have triggers that are always false
|
||||||
|
void optimize_const_eval(ConstEval& ce) {
|
||||||
|
ce.eval(sig_in);
|
||||||
|
ce.eval(clk.sig);
|
||||||
|
|
||||||
|
for (auto& [value, trigger] : async_rules) {
|
||||||
|
ce.eval(value);
|
||||||
|
ce.eval(trigger.sig);
|
||||||
|
}
|
||||||
|
|
||||||
|
async_rules.erase(
|
||||||
|
std::remove_if(async_rules.begin(), async_rules.end(),
|
||||||
|
[](const auto& rule) { return rule.trigger.is_never_triggered(); }
|
||||||
|
),
|
||||||
|
async_rules.end()
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
|
// Combine adjacent async rules that assign the same value into one rule
|
||||||
|
// with a disjunction of triggers. The resulting trigger is optimized by
|
||||||
|
// constant evaluation. We apply all of these optimizations that can be
|
||||||
|
// done to the LSB and shrink the size of the signal we are considering if
|
||||||
|
// higher bits cannot be optimized in the same way.
|
||||||
|
void optimize_same_value(ConstEval& ce) {
|
||||||
|
for (size_t i = 0; i + 1 < async_rules.size();) {
|
||||||
|
const bool lsb_optimizable = shrink_while_matching_values([&](const size_t bit) {
|
||||||
|
return async_rules[i].value[bit] == async_rules[i + 1].value[bit];
|
||||||
|
});
|
||||||
|
|
||||||
|
if (!lsb_optimizable) {
|
||||||
|
i++;
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
|
|
||||||
// If there is a reset condition in the async rules, use it
|
// i and i + 1 assign the same value so can be merged by taking
|
||||||
SigSpec rstval = async_rules.empty() ? RTLIL::SigSpec(RTLIL::State::Sz, sig.size()) : async_rules.front().first;
|
// the disjunction of triggers and deleting the second
|
||||||
RTLIL::SyncRule* sync_level = async_rules.empty() ? nullptr : async_rules.front().second;
|
async_rules[i].trigger = mod.ReduceOr(
|
||||||
ce.assign_map.apply(rstval);
|
NEW_ID,
|
||||||
|
SigSpec{
|
||||||
|
async_rules[i].trigger.positive_trigger(mod),
|
||||||
|
async_rules[i + 1].trigger.positive_trigger(mod)
|
||||||
|
}
|
||||||
|
);
|
||||||
|
async_rules.erase(async_rules.begin() + i + 1);
|
||||||
|
|
||||||
if (!rstval.is_fully_const() && !ce.eval(rstval))
|
ce.eval(async_rules[i].trigger.sig);
|
||||||
{
|
}
|
||||||
log_warning("Async reset value `%s' is not constant!\n", log_signal(rstval));
|
|
||||||
gen_aldff(mod, insig, rstval, sig_q,
|
|
||||||
sync_edge->type == RTLIL::SyncType::STp,
|
|
||||||
sync_level && sync_level->type == RTLIL::SyncType::ST1,
|
|
||||||
sync_edge->signal, sync_level->signal, proc);
|
|
||||||
continue;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
gen_dff(mod, insig, rstval.as_const(), sig_q,
|
// If the lowest priority async rule assigns the output value to itself,
|
||||||
sync_edge && sync_edge->type == RTLIL::SyncType::STp,
|
// remove the rule and fold this into the input signal. If the LSB assigns
|
||||||
sync_level && sync_level->type == RTLIL::SyncType::ST1,
|
// the output to itself but higher bits don't, we resize down to just the
|
||||||
sync_edge ? sync_edge->signal : SigSpec(),
|
// LSBs that assign to themselves, allowing more optimized representations
|
||||||
sync_level ? &sync_level->signal : NULL, proc);
|
// for those bits.
|
||||||
|
void optimize_self_assign(ConstEval& ce) {
|
||||||
|
SigSpec sig_out_mapped = sig_out;
|
||||||
|
ce.assign_map.apply(sig_out_mapped);
|
||||||
|
|
||||||
|
// Calculate the number of low priority rules that can be folded into
|
||||||
|
// the input signal for a given bit position
|
||||||
|
const size_t lsb_foldable_rules = shrink_while_matching_values([&](const size_t i) {
|
||||||
|
size_t foldable = 0;
|
||||||
|
for (auto it = async_rules.crbegin(); it != async_rules.crend(); it++, foldable++) {
|
||||||
|
const auto& [value, trigger] = *it;
|
||||||
|
if (value[i] != sig_out_mapped[i])
|
||||||
|
break;
|
||||||
|
}
|
||||||
|
return foldable;
|
||||||
|
});
|
||||||
|
|
||||||
|
if (lsb_foldable_rules == 0)
|
||||||
|
return;
|
||||||
|
|
||||||
|
// Calculate the disjunction of triggers
|
||||||
|
SigSpec triggers;
|
||||||
|
for (size_t i = 0; i < lsb_foldable_rules; i++)
|
||||||
|
triggers.append(async_rules.crbegin()[i].trigger.positive_trigger(mod));
|
||||||
|
|
||||||
|
const auto trigger = mod.ReduceOr(NEW_ID, triggers);
|
||||||
|
sig_in = mod.Mux(NEW_ID, sig_in, sig_out, trigger);
|
||||||
|
ce.eval(sig_in);
|
||||||
|
|
||||||
|
async_rules.resize(async_rules.size() - lsb_foldable_rules);
|
||||||
|
}
|
||||||
|
|
||||||
|
// If we have only a single rule, this means we will generate either an $aldff
|
||||||
|
// or an $adff if the reset value is constant or non-constant respectively.
|
||||||
|
// If there are any non-constant bits in the rule value, an $aldff will be
|
||||||
|
// used for all bits, but we would like to use an $adff for as many
|
||||||
|
// bits as possible. This optimization therefore calculates the longest run
|
||||||
|
// of bits starting at the LSB of the value with the same constness and
|
||||||
|
// removes the rest from consideration in this pass. This means that const
|
||||||
|
// and non-const sections can be separately mapped to $adff and $aldff.
|
||||||
|
void optimize_single_rule_consts() {
|
||||||
|
if (async_rules.size() != 1)
|
||||||
|
return;
|
||||||
|
|
||||||
|
shrink_while_matching_values([&](const size_t i) {
|
||||||
|
return async_rules.front().value[i].is_wire();
|
||||||
|
});
|
||||||
|
}
|
||||||
|
|
||||||
|
void generate() {
|
||||||
|
// Progressively attempt more complex formulations, preferring the
|
||||||
|
// simpler ones. These rules should be able to cover all representable
|
||||||
|
// DFF patterns.
|
||||||
|
if (try_generate_always())
|
||||||
|
return;
|
||||||
|
|
||||||
|
if (try_generate_dff())
|
||||||
|
return;
|
||||||
|
|
||||||
|
if (try_generate_single_async_dff())
|
||||||
|
return;
|
||||||
|
|
||||||
|
if (try_generate_dffsr())
|
||||||
|
return;
|
||||||
|
|
||||||
|
log_error("unable to match a dff type to this signal's rules.\n");
|
||||||
|
}
|
||||||
|
|
||||||
|
// Generates a connection if this dff is an always connection
|
||||||
|
// Returns true if successful
|
||||||
|
bool try_generate_always() {
|
||||||
|
if (!always)
|
||||||
|
return false;
|
||||||
|
|
||||||
|
log_assert(async_rules.empty());
|
||||||
|
log_assert(clk.empty());
|
||||||
|
|
||||||
|
log(" created direct connection (no actual register cell created).\n");
|
||||||
|
mod.connect(sig_out, sig_in);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Generates a $dff if this dff has no async rules and a clock of a $ff
|
||||||
|
// if this dff has no async rules and is globally clocked
|
||||||
|
// Returns true if succesful
|
||||||
|
bool try_generate_dff() {
|
||||||
|
if (always || !async_rules.empty())
|
||||||
|
return false;
|
||||||
|
|
||||||
|
RTLIL::Cell* cell;
|
||||||
|
const char* edge;
|
||||||
|
if (clk.empty()) {
|
||||||
|
edge = "global";
|
||||||
|
cell = mod.addFf(new_dff_name(), sig_in, sig_out);
|
||||||
|
} else {
|
||||||
|
edge = clk.polarity_str();
|
||||||
|
cell = mod.addDff(
|
||||||
|
/* name */ new_dff_name(),
|
||||||
|
/* sig_clk */ clk.sig,
|
||||||
|
/* sig_d */ sig_in,
|
||||||
|
/* sig_q */ sig_out,
|
||||||
|
/* clk_polarity */ clk.polarity()
|
||||||
|
);
|
||||||
|
}
|
||||||
|
cell->attributes = proc.attributes;
|
||||||
|
|
||||||
|
log(" created %s cell `%s' with %s edge clock.", cell->type.c_str(), cell->name.c_str(), edge);
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Generates an $adff or $aldff if this dff has a single async rule that
|
||||||
|
// is constant or non-constant respectively
|
||||||
|
// Returns true if successful
|
||||||
|
bool try_generate_single_async_dff() {
|
||||||
|
if (!explicitly_clocked() || async_rules.size() != 1)
|
||||||
|
return false;
|
||||||
|
|
||||||
|
const auto& aload = async_rules.front();
|
||||||
|
const bool is_const = aload.value.is_fully_const();
|
||||||
|
|
||||||
|
RTLIL::Cell* cell;
|
||||||
|
if (is_const) {
|
||||||
|
cell = mod.addAdff(
|
||||||
|
/* name */ new_dff_name(),
|
||||||
|
/* sig_clk */ clk.sig,
|
||||||
|
/* sig_arst */ aload.trigger.sig,
|
||||||
|
/* sig_d */ sig_in,
|
||||||
|
/* sig_q */ sig_out,
|
||||||
|
/* arst_value */ aload.value.as_const(),
|
||||||
|
/* clk_polarity */ clk.polarity(),
|
||||||
|
/* arst_polarity */ aload.trigger.polarity()
|
||||||
|
);
|
||||||
|
} else {
|
||||||
|
log_warning("Async reset value `%s' is not constant!\n", log_signal(aload.value));
|
||||||
|
cell = mod.addAldff(
|
||||||
|
/* name */ new_dff_name(),
|
||||||
|
/* sig_clk */ clk.sig,
|
||||||
|
/* sig_aload */ aload.trigger.sig,
|
||||||
|
/* sig_d */ sig_in,
|
||||||
|
/* sig_q */ sig_out,
|
||||||
|
/* sig_ad */ aload.value,
|
||||||
|
/* clk_polarity */ clk.polarity(),
|
||||||
|
/* aload_polarity */ aload.trigger.polarity()
|
||||||
|
);
|
||||||
|
}
|
||||||
|
cell->attributes = proc.attributes;
|
||||||
|
|
||||||
|
log(
|
||||||
|
" created %s cell `%s' with %s edge clock and %s level %sconst reset.\n",
|
||||||
|
cell->type.c_str(), cell->name.c_str(), clk.polarity_str(), aload.trigger.polarity_str(),
|
||||||
|
is_const ? "" : "non-"
|
||||||
|
);
|
||||||
|
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
// Generates a $dffsr cell from a complex set of async rules that are converted
|
||||||
|
// into driving conditions for set and reset signals
|
||||||
|
// Returns true if successful
|
||||||
|
bool try_generate_dffsr() {
|
||||||
|
if (!explicitly_clocked())
|
||||||
|
return false;
|
||||||
|
|
||||||
|
// A signal should be set/cleared if there is a load trigger that is enabled
|
||||||
|
// such that the load value is 1/0 and it is the highest priority trigger
|
||||||
|
RTLIL::SigSpec sig_set(0, size()), sig_clr(0, size());
|
||||||
|
|
||||||
|
// Reverse iterate through the rules as the first ones are the highest priority
|
||||||
|
// so need to be at the top of the mux trees
|
||||||
|
for (auto it = async_rules.crbegin(); it != async_rules.crend(); it++) {
|
||||||
|
const auto& [sync_value, trigger] = *it;
|
||||||
|
const auto pos_trig = trigger.positive_trigger(mod);
|
||||||
|
|
||||||
|
// If pos_trig is true, we have priority at this point in the tree so
|
||||||
|
// set a bit if value has a set bit. Otherwise, defer to the rest
|
||||||
|
// of the priority tree
|
||||||
|
sig_set = mod.Mux(NEW_ID, sig_set, sync_value, pos_trig);
|
||||||
|
|
||||||
|
// Same deal with clear bit
|
||||||
|
const auto sync_value_inv = mod.Not(NEW_ID, sync_value);
|
||||||
|
sig_clr = mod.Mux(NEW_ID, sig_clr, sync_value_inv, pos_trig);
|
||||||
|
}
|
||||||
|
|
||||||
|
auto* cell = mod.addDffsr(
|
||||||
|
/* name */ new_dff_name(),
|
||||||
|
/* sig_clk */ clk.sig,
|
||||||
|
/* sig_set */ sig_set,
|
||||||
|
/* sig_clr */ sig_clr,
|
||||||
|
/* sig_d */ sig_in,
|
||||||
|
/* sig_q */ sig_out,
|
||||||
|
/* clk_polarity */ clk.polarity()
|
||||||
|
);
|
||||||
|
cell->attributes = proc.attributes;
|
||||||
|
|
||||||
|
log(" created %s cell `%s' with %s edge clock and multiple level-sensitive resets.\n",
|
||||||
|
cell->type.c_str(), cell->name.c_str(), clk.polarity_str());
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
bool empty() const { return sig_out.empty(); }
|
||||||
|
size_t size() const { return sig_out.size(); }
|
||||||
|
const SigSpec& output() const { return sig_out; }
|
||||||
|
|
||||||
|
// True if there is an explicit clock signal, false if driven by an always
|
||||||
|
// or global clock
|
||||||
|
bool explicitly_clocked() const { return !always && !clk.empty(); }
|
||||||
|
|
||||||
|
private:
|
||||||
|
void resize(const size_t new_size) {
|
||||||
|
if (new_size >= size())
|
||||||
|
return;
|
||||||
|
|
||||||
|
sig_in = sig_in.extract(0, new_size);
|
||||||
|
sig_out = sig_out.extract(0, new_size);
|
||||||
|
for (auto& [value, _] : async_rules)
|
||||||
|
value = value.extract(0, new_size);
|
||||||
|
}
|
||||||
|
|
||||||
|
// Given some function that maps from an index to a value, this resizes
|
||||||
|
// the dff to a range starting at the LSB that all return the same value
|
||||||
|
// from the function as the LSB. This function also returns the value
|
||||||
|
// calculated for the LSB.
|
||||||
|
template <typename F>
|
||||||
|
typename std::invoke_result_t<F, size_t> shrink_while_matching_values(F f) {
|
||||||
|
const auto base_val = f(0);
|
||||||
|
|
||||||
|
size_t new_size;
|
||||||
|
for (new_size = 1; new_size < size(); new_size++)
|
||||||
|
if (f(new_size) != base_val)
|
||||||
|
break;
|
||||||
|
|
||||||
|
resize(new_size);
|
||||||
|
return base_val;
|
||||||
|
}
|
||||||
|
|
||||||
|
RTLIL::Process& proc;
|
||||||
|
RTLIL::Module& mod;
|
||||||
|
|
||||||
|
// A clock or reset trigger that is active when sig goes high (low) when
|
||||||
|
// inverted is false (true)
|
||||||
|
struct TriggerSig {
|
||||||
|
SigSpec sig;
|
||||||
|
bool inverted = false;
|
||||||
|
|
||||||
|
TriggerSig() = default;
|
||||||
|
TriggerSig(const RTLIL::SyncRule& sync) : sig{sync.signal},
|
||||||
|
inverted{sync.type == RTLIL::SyncType::ST0 || sync.type == RTLIL::SyncType::STn} {}
|
||||||
|
|
||||||
|
TriggerSig(const RTLIL::SigSpec& signal) : sig{signal} {}
|
||||||
|
|
||||||
|
bool empty() const { return sig.empty(); }
|
||||||
|
bool polarity() const { return !inverted; }
|
||||||
|
const char* polarity_str() const { return polarity() ? "positive" : "negative"; }
|
||||||
|
|
||||||
|
bool is_never_triggered() const {
|
||||||
|
return inverted ? sig.is_fully_ones() : sig.is_fully_zero();
|
||||||
|
}
|
||||||
|
|
||||||
|
SigSpec positive_trigger(RTLIL::Module& mod) const {
|
||||||
|
if (!inverted)
|
||||||
|
return sig;
|
||||||
|
return mod.Not(NEW_ID, sig);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
|
||||||
|
// An update rule to update sig_q to value when trigger is triggered
|
||||||
|
struct AsyncRule {
|
||||||
|
SigSpec value;
|
||||||
|
TriggerSig trigger;
|
||||||
|
|
||||||
|
AsyncRule() = default;
|
||||||
|
AsyncRule(const SigSpec& value, const RTLIL::SyncRule& sync) : value{value}, trigger{sync} {}
|
||||||
|
};
|
||||||
|
|
||||||
|
// The d input (used when no async rules apply) and q output
|
||||||
|
SigSpec sig_in, sig_out;
|
||||||
|
|
||||||
|
// A priority ordered list of asynchronous rules used for set/reset/aload.
|
||||||
|
// A rule that comes earlier in this vector has higher priority than a later
|
||||||
|
// one (if both of their trigger conditions are met the higher priority
|
||||||
|
// value is taken)
|
||||||
|
std::vector<AsyncRule> async_rules;
|
||||||
|
|
||||||
|
// The clock signal with its polarity. If clk is empty, the DFF is driven
|
||||||
|
// by a global clock (and should have no async rules)
|
||||||
|
TriggerSig clk;
|
||||||
|
|
||||||
|
// If this is true, this isn't really a DFF but instead an always assignment
|
||||||
|
// that can be made with a connection. clk and async_rules should be empty
|
||||||
|
// in this case
|
||||||
|
bool always = false;
|
||||||
|
};
|
||||||
|
|
||||||
|
void proc_dff(RTLIL::Module& mod, RTLIL::Process& proc, ConstEval &ce) {
|
||||||
|
while (1) {
|
||||||
|
// Find a new signal assigned by this process
|
||||||
|
const auto sig = find_any_lvalue(proc);
|
||||||
|
if (sig.empty())
|
||||||
|
break;
|
||||||
|
|
||||||
|
log("Creating register for signal `%s.%s' using process `%s.%s'.\n",
|
||||||
|
mod.name.c_str(), log_signal(sig), mod.name.c_str(), proc.name.c_str());
|
||||||
|
|
||||||
|
Dff dff{mod, sig, proc};
|
||||||
|
dff.optimize(ce);
|
||||||
|
dff.generate();
|
||||||
|
|
||||||
|
// Now that we are done with the signal remove it from the process
|
||||||
|
// We must do this after optimizing the dff as to emit an optimal dff
|
||||||
|
// type we might not actually use all bits of sig in this iteration
|
||||||
|
for (auto* sync : proc.syncs)
|
||||||
|
for (auto& action : sync->actions)
|
||||||
|
action.first.remove2(dff.output(), &action.second);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -311,7 +527,7 @@ struct ProcDffPass : public Pass {
|
||||||
ConstEval ce(mod);
|
ConstEval ce(mod);
|
||||||
for (auto &proc_it : mod->processes)
|
for (auto &proc_it : mod->processes)
|
||||||
if (design->selected(mod, proc_it.second))
|
if (design->selected(mod, proc_it.second))
|
||||||
proc_dff(mod, proc_it.second, ce);
|
proc_dff(*mod, *proc_it.second, ce);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
} ProcDffPass;
|
} ProcDffPass;
|
||||||
|
|
|
@ -78,3 +78,195 @@ select -assert-count 1 t:$assert
|
||||||
sat -tempinduct -verify -prove-asserts
|
sat -tempinduct -verify -prove-asserts
|
||||||
|
|
||||||
design -reset
|
design -reset
|
||||||
|
|
||||||
|
# A mix of different flop types all described together to stress test proc_dff
|
||||||
|
# more
|
||||||
|
read_verilog -formal <<EOT
|
||||||
|
module top(
|
||||||
|
input wire clk,
|
||||||
|
input wire arst,
|
||||||
|
input wire [7:0] d0, d1, d2, d3,
|
||||||
|
input wire [7:0] ad2,
|
||||||
|
output reg [7:0] q0, q1, q2, q3
|
||||||
|
);
|
||||||
|
|
||||||
|
wire never = '0;
|
||||||
|
|
||||||
|
always @(posedge clk, posedge arst) begin
|
||||||
|
{q0, q1, q2, q3} <= {d0, d1, d2, d3};
|
||||||
|
if (arst)
|
||||||
|
{q0, q2[7:4], q3, q2[3:0]} <= {q0, ad2[3:0], 8'hFF, 4'h5};
|
||||||
|
else if (never)
|
||||||
|
{q0, q1, q2, q3} <= {q3, q2, q1, q0};
|
||||||
|
end
|
||||||
|
|
||||||
|
always @* begin
|
||||||
|
if (arst) begin
|
||||||
|
assert(q2 == {ad2[3:0], 4'h5});
|
||||||
|
assert(q3 == 8'hFF);
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt_dff
|
||||||
|
opt_clean
|
||||||
|
|
||||||
|
# q0 is a standard $dffe
|
||||||
|
select w:q0 %ci* c:* %i
|
||||||
|
select -assert-count 1 %
|
||||||
|
select -assert-count 1 % t:$dffe %i
|
||||||
|
|
||||||
|
# q1 is an $aldff where both both aload and data take the same value
|
||||||
|
select w:q1 %ci* c:* %i
|
||||||
|
select -assert-count 1 %
|
||||||
|
select -assert-count 1 % t:$aldff %i
|
||||||
|
select -assert-count 1 % %ci:+[AD,D] w:* %i
|
||||||
|
|
||||||
|
# q2 is part driven by an $adff, and part by an $aldff
|
||||||
|
select w:q2 %ci* c:* %i
|
||||||
|
select -assert-count 2 %
|
||||||
|
select -assert-count 1 % t:$adff %i
|
||||||
|
select -assert-count 1 % t:$aldff %i
|
||||||
|
|
||||||
|
# q3 is driven by an $adff
|
||||||
|
select w:q3 %ci* c:* %i
|
||||||
|
select -assert-count 1 %
|
||||||
|
select -assert-count 1 % t:$adff %i
|
||||||
|
|
||||||
|
# never should appear in none of the cones of flops
|
||||||
|
select -assert-none c:* %x* w:never %i
|
||||||
|
|
||||||
|
select -clear
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
select -assert-any t:$assert
|
||||||
|
sat -tempinduct -verify -prove-asserts
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
|
||||||
|
# A design which is best mapped with different flops for different ranges of
|
||||||
|
# the variable
|
||||||
|
read_verilog <<EOT
|
||||||
|
module top(
|
||||||
|
input wire clk,
|
||||||
|
input wire rsta,
|
||||||
|
input wire rstb,
|
||||||
|
input wire [7:0] d,
|
||||||
|
output reg [7:0] q
|
||||||
|
);
|
||||||
|
|
||||||
|
always @(posedge clk or posedge rsta or posedge rstb) begin
|
||||||
|
if (rsta)
|
||||||
|
q <= '0;
|
||||||
|
else if (rstb)
|
||||||
|
q[3:0] <= 4'b0;
|
||||||
|
else
|
||||||
|
q <= d;
|
||||||
|
end
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt_dff
|
||||||
|
opt_clean
|
||||||
|
|
||||||
|
select w:q %ci* c:* %i
|
||||||
|
select -assert-count 1 % t:$adffe %i
|
||||||
|
select -assert-count 1 % t:$adff %i
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
|
||||||
|
# Another design which is best mapped with different flops for different ranges
|
||||||
|
# of the variable.
|
||||||
|
read_verilog <<EOT
|
||||||
|
module top(
|
||||||
|
input wire clk,
|
||||||
|
input wire rst,
|
||||||
|
output reg [7:0] q,
|
||||||
|
input wire [7:0] d
|
||||||
|
);
|
||||||
|
|
||||||
|
always @(posedge clk or posedge rst) begin
|
||||||
|
if (rst)
|
||||||
|
q[3:0] <= '0;
|
||||||
|
else
|
||||||
|
q <= d;
|
||||||
|
end
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt_dff
|
||||||
|
opt_clean
|
||||||
|
|
||||||
|
select w:q %ci* c:* %i
|
||||||
|
select -assert-count 1 % t:$dffe %i
|
||||||
|
select -assert-count 1 % t:$adff %i
|
||||||
|
|
||||||
|
design -reset
|
||||||
|
|
||||||
|
# A design that relies on merging adjacent sync rules with the same priority
|
||||||
|
# and folding low priority feedback rules into enables at the bit level
|
||||||
|
read_verilog -formal <<EOT
|
||||||
|
module top(
|
||||||
|
input wire clk,
|
||||||
|
input wire rsta, rstb, rstc, rstd,
|
||||||
|
input wire [2:0] d,
|
||||||
|
output reg [2:0] q
|
||||||
|
);
|
||||||
|
|
||||||
|
always @(posedge clk, posedge rsta, negedge rstb, posedge rstc, negedge rstd) begin
|
||||||
|
if (rsta)
|
||||||
|
q <= {1'b1, 1'b0, d[0]};
|
||||||
|
else if (!rstb)
|
||||||
|
q <= {1'b1, 1'b0, d[0]};
|
||||||
|
else if (rstc)
|
||||||
|
q <= {q[2], 1'b0, d[0]};
|
||||||
|
else if (~rstd)
|
||||||
|
q <= {q[2], 1'b1, d[0]};
|
||||||
|
else
|
||||||
|
q <= d;
|
||||||
|
end
|
||||||
|
|
||||||
|
always @* begin
|
||||||
|
if (rsta) begin
|
||||||
|
assert(q[2] == 1'b1);
|
||||||
|
assert(q[1] == 1'b0);
|
||||||
|
assert(q[0] == d[0]);
|
||||||
|
end else if (!rstb) begin
|
||||||
|
assert(q[2] == 1'b1);
|
||||||
|
assert(q[1] == 1'b0);
|
||||||
|
assert(q[0] == d[0]);
|
||||||
|
end else if (rstc) begin
|
||||||
|
assert(q[1] == 1'b0);
|
||||||
|
assert(q[0] == d[0]);
|
||||||
|
end else if (!rstd) begin
|
||||||
|
assert(q[1] == 1'b1);
|
||||||
|
assert(q[0] == d[0]);
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
endmodule
|
||||||
|
EOT
|
||||||
|
|
||||||
|
proc
|
||||||
|
opt_dff
|
||||||
|
opt_clean
|
||||||
|
|
||||||
|
# q is driven by an adffe, a dffsr and an aldff per bit
|
||||||
|
select w:q %ci1 c:* %i
|
||||||
|
select -assert-count 3 %
|
||||||
|
select -assert-count 1 % t:$adffe %i
|
||||||
|
select -assert-count 1 % t:$dffsr %i
|
||||||
|
select -assert-count 1 % t:$aldff %i
|
||||||
|
|
||||||
|
select -clear
|
||||||
|
|
||||||
|
clk2fflogic
|
||||||
|
select -assert-any t:$assert
|
||||||
|
sat -tempinduct -verify -prove-asserts
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue