mirror of https://github.com/YosysHQ/yosys.git
Merge upstream
This commit is contained in:
Akash Levy
commit
16215b8786
2
Makefile
2
Makefile
|
|
@ -180,7 +180,7 @@ ifeq ($(OS), Haiku)
|
|||
CXXFLAGS += -D_DEFAULT_SOURCE
|
||||
endif
|
||||
|
||||
YOSYS_VER := 0.57+218
|
||||
YOSYS_VER := 0.57+244
|
||||
YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
|
||||
YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2)
|
||||
YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'.' -f3)
|
||||
|
|
|
|||
|
|
@ -105,6 +105,13 @@ struct Index {
|
|||
if (allow_blackboxes) {
|
||||
info.found_blackboxes.insert(cell);
|
||||
} else {
|
||||
// Even if we don't allow blackboxes these might still be
|
||||
// present outside of any traversed input cones, so we
|
||||
// can't bail at this point. If they are hit by a traversal
|
||||
// (which can only really happen with $tribuf not
|
||||
// $connect), we can still detect this as an error later.
|
||||
if (cell->type == ID($connect) || (cell->type == ID($tribuf) && cell->has_attribute(ID(aiger2_zbuf))))
|
||||
continue;
|
||||
if (!submodule || submodule->get_blackbox_attribute())
|
||||
log_warning("Unsupported cell type: %s (%s in %s)\n",
|
||||
log_id(cell->type), log_id(cell), log_id(m));
|
||||
|
|
@ -483,7 +490,8 @@ struct Index {
|
|||
{
|
||||
Design *design = index.design;
|
||||
auto &minfo = leaf_minfo(index);
|
||||
log_assert(minfo.suboffsets.count(cell));
|
||||
if (!minfo.suboffsets.count(cell))
|
||||
log_error("Reached unsupport cell %s (%s in %s)\n", log_id(cell->type), log_id(cell), log_id(cell->module));
|
||||
Module *def = design->module(cell->type);
|
||||
log_assert(def);
|
||||
levels.push_back(Level(index.modules.at(def), cell));
|
||||
|
|
|
|||
|
|
@ -205,8 +205,8 @@ YosysStreamCallBackHandler verific_read_cb;
|
|||
|
||||
// ==================================================================
|
||||
|
||||
VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
|
||||
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
|
||||
VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
|
||||
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), mode_sva_continue(mode_sva_continue),
|
||||
mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover),
|
||||
mode_fullinit(mode_fullinit)
|
||||
{
|
||||
|
|
@ -2374,6 +2374,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
|
|||
wire->attributes.erase(ID::init);
|
||||
}
|
||||
}
|
||||
|
||||
if (num_sva_continue) {
|
||||
log_warning("Encountered %d items containing unsupported SVA!\n", num_sva_continue);
|
||||
log_warning("Unsupported SVA imported as 'x and marked using the `unsupported_sva' attribute due to -sva-continue-on-err.\n");
|
||||
}
|
||||
num_sva_continue = 0;
|
||||
}
|
||||
|
||||
// ==================================================================
|
||||
|
|
@ -3132,7 +3138,7 @@ std::string verific_import(Design *design, const std::map<std::string,std::strin
|
|||
}
|
||||
|
||||
if (nl_done.count(it->first) == 0) {
|
||||
VerificImporter importer(false, false, false, false, false, false, false);
|
||||
VerificImporter importer(false, false, false, false, false, false, false, false);
|
||||
nl_done[it->first] = it->second;
|
||||
importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName()));
|
||||
}
|
||||
|
|
@ -3369,6 +3375,11 @@ struct VerificPass : public Pass {
|
|||
log(" -nosva\n");
|
||||
log(" Ignore SVA properties, do not infer checker logic.\n");
|
||||
log("\n");
|
||||
log(" -sva-continue-on-err\n");
|
||||
log(" Turns unsupported SVA from an error into a warning. Properties are imported\n");
|
||||
log(" with their trigger condition replaced with 'x and with an `unsupported_sva'\n");
|
||||
log(" attribute to produce a later error in SBY if they remain in the design.\n");
|
||||
log("\n");
|
||||
log(" -L <int>\n");
|
||||
log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
|
||||
log("\n");
|
||||
|
|
@ -4234,7 +4245,8 @@ struct VerificPass : public Pass {
|
|||
{
|
||||
std::map<std::string,Netlist*> nl_todo, nl_done;
|
||||
bool mode_all = false, mode_gates = false, mode_keep = false;
|
||||
bool mode_nosva = false, mode_names = false, mode_verific = false;
|
||||
bool mode_nosva = false, mode_sva_continue = false;
|
||||
bool mode_names = false, mode_verific = false;
|
||||
bool mode_autocover = false, mode_fullinit = false;
|
||||
bool flatten = false, extnets = false, mode_cells = false;
|
||||
bool split_complex_ports = true;
|
||||
|
|
@ -4272,6 +4284,10 @@ struct VerificPass : public Pass {
|
|||
mode_nosva = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-sva-continue-on-err") {
|
||||
mode_sva_continue = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
|
||||
verific_sva_fsm_limit = atoi(args[++argidx].c_str());
|
||||
continue;
|
||||
|
|
@ -4402,7 +4418,7 @@ struct VerificPass : public Pass {
|
|||
auto it = nl_todo.begin();
|
||||
Netlist *nl = it->second;
|
||||
if (nl_done.count(it->first) == 0) {
|
||||
VerificImporter importer(mode_gates, mode_keep, mode_nosva,
|
||||
VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_sva_continue,
|
||||
mode_names, mode_verific, mode_autocover, mode_fullinit);
|
||||
nl_done[it->first] = it->second;
|
||||
importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName()));
|
||||
|
|
|
|||
|
|
@ -77,10 +77,12 @@ struct VerificImporter
|
|||
std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
|
||||
pool<Verific::Net*> any_all_nets;
|
||||
|
||||
bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
|
||||
bool mode_gates, mode_keep, mode_nosva, mode_sva_continue, mode_names, mode_verific;
|
||||
bool mode_autocover, mode_fullinit;
|
||||
|
||||
VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit);
|
||||
int num_sva_continue = 0;
|
||||
|
||||
VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit);
|
||||
|
||||
RTLIL::SigBit net_map_at(Verific::Net *net);
|
||||
|
||||
|
|
|
|||
|
|
@ -124,6 +124,7 @@ struct SvaFsm
|
|||
{
|
||||
Module *module;
|
||||
VerificClocking clocking;
|
||||
std::function<void (std::string)> parser_error;
|
||||
|
||||
SigBit trigger_sig = State::S1, disable_sig;
|
||||
SigBit throughout_sig = State::S1;
|
||||
|
|
@ -148,6 +149,7 @@ struct SvaFsm
|
|||
module = clking.module;
|
||||
clocking = clking;
|
||||
trigger_sig = trig;
|
||||
parser_error = [](std::string msg){ log_error("%s", msg); };
|
||||
|
||||
startNode = createNode();
|
||||
acceptNode = createNode();
|
||||
|
|
@ -475,8 +477,8 @@ struct SvaFsm
|
|||
dump();
|
||||
log(" ctrl signal: %s\n", log_signal(dnode.ctrl));
|
||||
}
|
||||
log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
|
||||
GetSize(dnode.ctrl), verific_sva_fsm_limit);
|
||||
parser_error(stringf("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
|
||||
GetSize(dnode.ctrl), verific_sva_fsm_limit));
|
||||
}
|
||||
|
||||
for (unsigned long long i = 0; i < (1ull << GetSize(dnode.ctrl)); i++)
|
||||
|
|
@ -1023,7 +1025,7 @@ struct VerificSvaImporter
|
|||
|
||||
[[noreturn]] void parser_error(std::string errmsg)
|
||||
{
|
||||
if (!importer->mode_keep)
|
||||
if (!importer->mode_keep && !importer->mode_sva_continue)
|
||||
log_error("%s", errmsg);
|
||||
log_warning("%s", errmsg);
|
||||
throw ParserErrorException();
|
||||
|
|
@ -1260,6 +1262,7 @@ struct VerificSvaImporter
|
|||
if (inst->Type() == PRIM_SVA_FIRST_MATCH)
|
||||
{
|
||||
SvaFsm match_fsm(clocking);
|
||||
match_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode);
|
||||
|
||||
int node = fsm.createNode();
|
||||
|
|
@ -1426,12 +1429,15 @@ struct VerificSvaImporter
|
|||
if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND)
|
||||
{
|
||||
SvaFsm fsm1(clocking);
|
||||
fsm1.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode);
|
||||
|
||||
SvaFsm fsm2(clocking);
|
||||
fsm2.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode);
|
||||
|
||||
SvaFsm combined_fsm(clocking);
|
||||
combined_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
|
||||
fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
|
||||
|
||||
|
|
@ -1456,6 +1462,7 @@ struct VerificSvaImporter
|
|||
if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN)
|
||||
{
|
||||
SvaFsm intersect_fsm(clocking);
|
||||
intersect_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
|
||||
if (inst->Type() == PRIM_SVA_INTERSECT)
|
||||
{
|
||||
|
|
@ -1562,6 +1569,7 @@ struct VerificSvaImporter
|
|||
int node;
|
||||
|
||||
SvaFsm antecedent_fsm(clocking, trig);
|
||||
antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
|
||||
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
|
||||
int next_node = antecedent_fsm.createNode();
|
||||
|
|
@ -1623,6 +1631,7 @@ struct VerificSvaImporter
|
|||
int node;
|
||||
|
||||
SvaFsm antecedent_fsm(clocking, trig);
|
||||
antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
|
||||
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION || inst->Type() == PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY) {
|
||||
int next_node = antecedent_fsm.createNode();
|
||||
|
|
@ -1677,6 +1686,7 @@ struct VerificSvaImporter
|
|||
}
|
||||
|
||||
SvaFsm consequent_fsm(clocking, antecedent_match);
|
||||
consequent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net);
|
||||
consequent_fsm.createLink(node, consequent_fsm.acceptNode);
|
||||
|
||||
|
|
@ -1696,6 +1706,7 @@ struct VerificSvaImporter
|
|||
}
|
||||
|
||||
SvaFsm fsm(clocking, trig);
|
||||
fsm.parser_error = [&](std::string msg) { this->parser_error(msg); };
|
||||
int node = parse_sequence(fsm, fsm.createStartNode(), net);
|
||||
fsm.createLink(node, fsm.acceptNode);
|
||||
|
||||
|
|
@ -1710,30 +1721,34 @@ struct VerificSvaImporter
|
|||
|
||||
void import()
|
||||
{
|
||||
try
|
||||
{
|
||||
module = importer->module;
|
||||
netlist = root->Owner();
|
||||
module = importer->module;
|
||||
netlist = root->Owner();
|
||||
|
||||
if (verific_verbose)
|
||||
log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
|
||||
LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
|
||||
int initial_cell_count = GetSize(module->cells_);
|
||||
int initial_wire_count = GetSize(module->wires_);
|
||||
int initial_connection_count = GetSize(module->connections_);
|
||||
|
||||
bool is_user_declared = root->IsUserDeclared();
|
||||
if (verific_verbose)
|
||||
log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
|
||||
LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
|
||||
|
||||
// FIXME
|
||||
if (!is_user_declared) {
|
||||
const char *name = root->Name();
|
||||
for (int i = 0; name[i]; i++) {
|
||||
if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
|
||||
is_user_declared = true;
|
||||
break;
|
||||
}
|
||||
bool is_user_declared = root->IsUserDeclared();
|
||||
|
||||
// FIXME
|
||||
if (!is_user_declared) {
|
||||
const char *name = root->Name();
|
||||
for (int i = 0; name[i]; i++) {
|
||||
if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
|
||||
is_user_declared = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);
|
||||
RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);
|
||||
|
||||
try
|
||||
{
|
||||
// parse SVA sequence into trigger signal
|
||||
|
||||
clocking = VerificClocking(importer, root->GetInput(), true);
|
||||
|
|
@ -1836,6 +1851,36 @@ struct VerificSvaImporter
|
|||
}
|
||||
catch (ParserErrorException)
|
||||
{
|
||||
if (importer->mode_sva_continue) {
|
||||
|
||||
std::vector<Cell *> remove_cells;
|
||||
pool<Wire *> remove_wires;
|
||||
|
||||
for (int i = 0, end = GetSize(module->cells_) - initial_cell_count; i != end; ++i)
|
||||
remove_cells.push_back(module->cells_.element(i)->second);
|
||||
|
||||
for (int i = 0, end = GetSize(module->wires_) - initial_wire_count; i != end; ++i)
|
||||
remove_wires.emplace(module->wires_.element(i)->second);
|
||||
|
||||
for (auto cell : remove_cells)
|
||||
module->remove(cell);
|
||||
module->remove(remove_wires);
|
||||
|
||||
module->connections_.resize(initial_connection_count);
|
||||
|
||||
RTLIL::Cell *c = nullptr;
|
||||
|
||||
if (mode_assert) c = module->addAssert(root_name, State::Sx, State::Sx);
|
||||
if (mode_assume) c = module->addAssume(root_name, State::Sx, State::Sx);
|
||||
if (mode_cover) c = module->addCover(root_name, State::Sx, State::Sx);
|
||||
|
||||
if (c) {
|
||||
importer->import_attributes(c->attributes, root);
|
||||
c->set_bool_attribute(ID(unsupported_sva));
|
||||
}
|
||||
|
||||
importer->num_sva_continue++;
|
||||
}
|
||||
}
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -2845,6 +2845,13 @@ void RTLIL::Module::remove(const pool<RTLIL::Wire*> &wires)
|
|||
delete_wire_worker.wires_p = &wires;
|
||||
rewrite_sigspecs2(delete_wire_worker);
|
||||
|
||||
if (design->flagBufferedNormalized) {
|
||||
for (auto wire : wires) {
|
||||
buf_norm_wire_queue.erase(wire);
|
||||
buf_norm_connect_index.erase(wire);
|
||||
}
|
||||
}
|
||||
|
||||
for (auto &it : wires) {
|
||||
log_assert(wires_.count(it->name) != 0);
|
||||
wires_.erase(it->name);
|
||||
|
|
|
|||
|
|
@ -43,6 +43,7 @@ void RTLIL::Design::bufNormalize(bool enable)
|
|||
wire->driverCell_ = nullptr;
|
||||
wire->driverPort_ = IdString();
|
||||
}
|
||||
module->buf_norm_connect_index.clear();
|
||||
}
|
||||
|
||||
flagBufferedNormalized = false;
|
||||
|
|
@ -126,15 +127,19 @@ void RTLIL::Module::bufNormalize()
|
|||
idict<Wire *> wire_queue_entries; // Ordered queue of wires to process
|
||||
int wire_queue_pos = 0; // Index up to which we processed the wires
|
||||
|
||||
// Wires with their unique driving cell port. If we know a wire is
|
||||
// driven by multiple (potential) drivers, this is indicated by a
|
||||
// nullptr as cell.
|
||||
// Wires with their unique driving cell port. We pick the first driver
|
||||
// we encounter, with the exception that we ensure that a module input
|
||||
// port can only get $input_port drivers and that $input_port drivers
|
||||
// cannot drive any other modules. If we reject an $input_port driver
|
||||
// because it's not driving an input port or because there already is
|
||||
// another $input_port driver for the same port, we also delete that
|
||||
// $input_port cell.
|
||||
dict<Wire *, std::pair<Cell *, IdString>> direct_driven_wires;
|
||||
|
||||
// Set of non-unique or driving cell ports for each processed wire.
|
||||
dict<Wire *, pool<std::pair<Cell *, IdString>>> direct_driven_wires_conflicts;
|
||||
|
||||
// Set of cell ports that need a fresh intermediate wire.
|
||||
// Set of cell ports that need a fresh intermediate wire. These are all
|
||||
// cell ports that drive non-full-wire sigspecs, cell ports driving
|
||||
// module input ports, and cell ports driving wires that are already
|
||||
// driven.
|
||||
pool<std::pair<Cell *, IdString>> pending_ports;
|
||||
|
||||
// This helper will be called for every output/inout cell port that is
|
||||
|
|
@ -149,27 +154,14 @@ void RTLIL::Module::bufNormalize()
|
|||
|
||||
|
||||
SigSpec const &sig = cell->getPort(port);
|
||||
if (cell->type == ID($input_port)) {
|
||||
// If an `$input_port` cell isn't fully connected to a full
|
||||
// input port wire, we remove it since the wires are still the
|
||||
// canonical source of module ports and the `$input_port` cells
|
||||
// are just helpers to simplfiy the bufnorm invariant.
|
||||
log_assert(port == ID::Y);
|
||||
if (!sig.is_wire()) {
|
||||
buf_norm_cell_queue.insert(cell);
|
||||
remove(cell);
|
||||
return;
|
||||
}
|
||||
|
||||
Wire *w = sig.as_wire();
|
||||
if (!w->port_input || w->port_output) {
|
||||
buf_norm_cell_queue.insert(cell);
|
||||
remove(cell);
|
||||
return;
|
||||
}
|
||||
w->driverCell_ = cell;
|
||||
w->driverPort_ = ID::Y;
|
||||
} else if (cell->type == ID($buf) && cell->attributes.empty() && !cell->name.isPublic()) {
|
||||
// Make sure all wires of the cell port are enqueued, ensuring we
|
||||
// detect other connected drivers (output and inout).
|
||||
for (auto chunk : sig.chunks())
|
||||
if (chunk.is_wire())
|
||||
wire_queue_entries(chunk.wire);
|
||||
|
||||
if (cell->type == ID($buf) && cell->attributes.empty() && !cell->name.isPublic()) {
|
||||
// For a plain `$buf` cell, we enqueue all wires on its input
|
||||
// side, bypass it using module level connections (skipping 'z
|
||||
// bits) and then remove the cell. Eventually the module level
|
||||
|
|
@ -206,47 +198,40 @@ void RTLIL::Module::bufNormalize()
|
|||
|
||||
if (!sig_y.empty())
|
||||
connect(sig_y, sig_a);
|
||||
remove(cell);
|
||||
log_assert(GetSize(buf_norm_wire_queue) <= 1);
|
||||
buf_norm_wire_queue.clear();
|
||||
return;
|
||||
} else if (cell->type == ID($input_port)) {
|
||||
log_assert(port == ID::Y);
|
||||
if (sig.is_wire()) {
|
||||
Wire *w = sig.as_wire();
|
||||
if (w->port_input && !w->port_output) {
|
||||
// An $input_port cell can only drive a full wire module input port
|
||||
auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port});
|
||||
if (!inserted || (found->second.first == cell && found->second.second == port))
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
// If an `$input_port` cell isn't driving a full
|
||||
// input port wire, we remove it since the wires are still the
|
||||
// canonical source of module ports
|
||||
|
||||
buf_norm_cell_queue.insert(cell);
|
||||
remove(cell);
|
||||
log_assert(GetSize(buf_norm_wire_queue) <= 1);
|
||||
buf_norm_wire_queue.clear();
|
||||
return;
|
||||
}
|
||||
|
||||
// Make sure all wires of the cell port are enqueued, ensuring we
|
||||
// detect other connected drivers (output and inout).
|
||||
for (auto const &chunk : sig.chunks())
|
||||
if (chunk.wire)
|
||||
wire_queue_entries(chunk.wire);
|
||||
|
||||
if (sig.is_wire()) {
|
||||
// If the full cell port is connected to a full wire, we might be
|
||||
// able to keep that connection if this is a unique output port driving that wire
|
||||
Wire *w = sig.as_wire();
|
||||
|
||||
// We try to store the current port as unique driver, if this
|
||||
// succeeds we're done with the port.
|
||||
auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port});
|
||||
if (inserted || (found->second.first == cell && found->second.second == port))
|
||||
return;
|
||||
|
||||
// When this failed, we store this port as a conflict. If we
|
||||
// had already stored a candidate for a unique driver, we also
|
||||
// move it to the conflicts, leaving a nullptr marker.
|
||||
|
||||
auto &conflicts = direct_driven_wires_conflicts[w];
|
||||
if (Cell *other_cell = found->second.first) {
|
||||
if (other_cell->type == ID($input_port)) {
|
||||
// Multiple input port cells
|
||||
log_assert(cell->type != ID($input_port));
|
||||
} else {
|
||||
pending_ports.insert(found->second);
|
||||
conflicts.emplace(found->second);
|
||||
found->second = {nullptr, {}};
|
||||
}
|
||||
}
|
||||
if (cell->type == ID($input_port)) {
|
||||
found->second = {cell, port};
|
||||
} else {
|
||||
conflicts.emplace(cell, port);
|
||||
if (!w->port_input || w->port_output) {
|
||||
// If the full cell port is connected to a full non-input-port wire, pick it as driver
|
||||
auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port});
|
||||
if (inserted || (found->second.first == cell && found->second.second == port))
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -256,16 +241,22 @@ void RTLIL::Module::bufNormalize()
|
|||
pending_ports.emplace(cell, port);
|
||||
};
|
||||
|
||||
// We enqueue all enqueued wires for `$buf`/`$connect` processing (clearing the module level queue).
|
||||
for (auto wire : buf_norm_wire_queue)
|
||||
wire_queue_entries(wire);
|
||||
buf_norm_wire_queue.clear();
|
||||
|
||||
// Only after clearing the `buf_norm_wire_queue` are we allowed to call
|
||||
// enqueue_cell_port, since we're using assertions to check against
|
||||
// unintended wires being enqueued into `buf_norm_wire_queue` that
|
||||
// would prevent us from restoring the bufnorm invariants in a single
|
||||
// pass.
|
||||
|
||||
// We process all explicitly enqueued cell ports (clearing the module level queue).
|
||||
for (auto const &[cell, port_name] : buf_norm_cell_port_queue)
|
||||
enqueue_cell_port(cell, port_name);
|
||||
buf_norm_cell_port_queue.clear();
|
||||
|
||||
// And enqueue all wires for `$buf`/`$connect` processing (clearing the module level queue).
|
||||
for (auto wire : buf_norm_wire_queue)
|
||||
wire_queue_entries(wire);
|
||||
buf_norm_wire_queue.clear();
|
||||
|
||||
// We also enqueue all wires that saw newly added module level connections.
|
||||
for (auto &[a, b] : connections_)
|
||||
for (auto &sig : {a, b})
|
||||
|
|
@ -302,8 +293,11 @@ void RTLIL::Module::bufNormalize()
|
|||
if (chunk.wire)
|
||||
wire_queue_entries(chunk.wire);
|
||||
connect(sig_a, sig_b);
|
||||
|
||||
buf_norm_cell_queue.insert(connect_cell);
|
||||
remove(connect_cell);
|
||||
log_assert(GetSize(buf_norm_wire_queue) <= 2);
|
||||
buf_norm_wire_queue.clear();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -315,6 +309,9 @@ void RTLIL::Module::bufNormalize()
|
|||
// As a first step for re-normalization we add all require intermediate
|
||||
// wires for cell output and inout ports.
|
||||
for (auto &[cell, port] : pending_ports) {
|
||||
log_assert(cell->type != ID($input_port));
|
||||
log_assert(!cell->type.empty());
|
||||
log_assert(!pending_deleted_cells.count(cell));
|
||||
SigSpec const &sig = cell->getPort(port);
|
||||
Wire *w = addWire(NEW_ID, GetSize(sig));
|
||||
|
||||
|
|
@ -323,16 +320,9 @@ void RTLIL::Module::bufNormalize()
|
|||
// correspond to what you would get if the intermediate wires had
|
||||
// been in place from the beginning.
|
||||
connect(sig, w);
|
||||
auto port_dir = cell->port_dir(port);
|
||||
if (port_dir == RTLIL::PD_INOUT || port_dir == RTLIL::PD_UNKNOWN) {
|
||||
direct_driven_wires.emplace(w, {nullptr, {}});
|
||||
direct_driven_wires_conflicts[w].emplace(cell, port);
|
||||
} else {
|
||||
direct_driven_wires.emplace(w, {cell, port});
|
||||
}
|
||||
|
||||
cell->setPort(port, w);
|
||||
wire_queue_entries(w);
|
||||
direct_driven_wires.emplace(w, {cell, port});
|
||||
cell->setPort(port, w); // Hits the fast path that doesn't enqueue w
|
||||
wire_queue_entries(w); // Needed so we pick up the sig <-> w connection
|
||||
}
|
||||
|
||||
// At this point we're done with creating wires and know which ones are
|
||||
|
|
@ -346,7 +336,7 @@ void RTLIL::Module::bufNormalize()
|
|||
wire->driverPort_.clear();
|
||||
}
|
||||
|
||||
// For the unique output cell ports fully connected to a full wire, we
|
||||
// For the unique driving cell ports fully connected to a full wire, we
|
||||
// can update the bufnorm data right away. For all other wires we will
|
||||
// have to create new `$buf` cells.
|
||||
for (auto const &[wire, cellport] : direct_driven_wires) {
|
||||
|
|
@ -373,54 +363,55 @@ void RTLIL::Module::bufNormalize()
|
|||
SigMap sigmap(this);
|
||||
new_connections({});
|
||||
|
||||
pool<SigBit> conflicted;
|
||||
pool<SigBit> driven;
|
||||
|
||||
// We iterate over all direct driven wires and try to make that wire's
|
||||
// sigbits the representative sigbit for the net. We do a second pass
|
||||
// to detect conflicts to then remove the conflicts from `driven`.
|
||||
for (bool check : {false, true}) {
|
||||
// We pick SigMap representatives by prioritizing input ports over
|
||||
// driven wires over other/unknown wires.
|
||||
for (bool input_ports : {false, true}) {
|
||||
for (auto const &[wire, cellport] : direct_driven_wires) {
|
||||
if (cellport.first == nullptr)
|
||||
continue;
|
||||
auto const &[cell, port] = cellport;
|
||||
|
||||
SigSpec z_mask;
|
||||
if (cell->type == ID($buf))
|
||||
z_mask = cell->getPort(ID::A);
|
||||
|
||||
for (int i = 0; i != GetSize(wire); ++i) {
|
||||
SigBit driver = SigBit(wire, i);
|
||||
if (!z_mask.empty() && z_mask[i] == State::Sz)
|
||||
continue;
|
||||
if (check) {
|
||||
SigBit repr = sigmap(driver);
|
||||
if (repr != driver)
|
||||
conflicted.insert(repr);
|
||||
else
|
||||
driven.insert(repr);
|
||||
} else {
|
||||
if ((wire->port_input && !wire->port_output) == input_ports) {
|
||||
for (int i = 0; i != GetSize(wire); ++i) {
|
||||
SigBit driver = SigBit(wire, i);
|
||||
sigmap.database.promote(driver);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Ensure that module level inout ports are directly driven or
|
||||
// connected using `$connect` cells and never `$buf`fered.
|
||||
for (auto wire : wire_queue_entries) {
|
||||
if (!wire->port_input || !wire->port_output)
|
||||
continue;
|
||||
// All three pool<SigBit> below are in terms of sigmapped bits
|
||||
// Bits that are known to have a unique driver that is an unconditional driver or one or more inout drivers
|
||||
pool<SigBit> driven;
|
||||
// Bits that have multiple unconditional drivers, this forces the use of `$connect`
|
||||
pool<SigBit> conflicted;
|
||||
// Bits that are driven by an inout driver
|
||||
pool<SigBit> weakly_driven;
|
||||
|
||||
for (auto const &[wire, cellport] : direct_driven_wires) {
|
||||
auto const &[cell, port] = cellport;
|
||||
for (int i = 0; i != GetSize(wire); ++i) {
|
||||
SigBit driver = SigBit(wire, i);
|
||||
SigBit repr = sigmap(driver);
|
||||
if (driver != repr)
|
||||
driven.erase(repr);
|
||||
SigBit driver = sigmap(SigBit(wire, i));
|
||||
if (cell->type == ID($tribuf) || cell->port_dir(port) == RTLIL::PD_INOUT) {
|
||||
// We add inout drivers to `driven` in a separate loop below
|
||||
weakly_driven.insert(driver);
|
||||
} else {
|
||||
// We remove driver conflicts from `driven` in a separate loop below
|
||||
bool inserted = driven.insert(driver).second;
|
||||
if (!inserted)
|
||||
conflicted.insert(driver);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
for (auto &bit : conflicted)
|
||||
driven.erase(bit);
|
||||
// If a wire has one or more inout drivers and an unconditional driver, that's still a conflict
|
||||
for (auto driver : weakly_driven)
|
||||
if (!driven.insert(driver).second)
|
||||
conflicted.insert(driver);
|
||||
|
||||
// This only leaves the drivers matching `driven`'s definition above
|
||||
for (auto driver : conflicted)
|
||||
driven.erase(driver);
|
||||
|
||||
// Having picked representatives and checked whether they are unique
|
||||
// drivers, we can turn the connecitivty of our sigmap back into $buf
|
||||
// and $connect cells.
|
||||
|
||||
// Module level bitwise connections not representable by `$buf` cells
|
||||
pool<pair<SigBit, SigBit>> undirected_connections;
|
||||
|
|
@ -561,6 +552,8 @@ void RTLIL::Cell::unsetPort(const RTLIL::IdString& portname)
|
|||
w->driverCell_ = nullptr;
|
||||
w->driverPort_ = IdString();
|
||||
module->buf_norm_wire_queue.insert(w);
|
||||
} else if (w->driverCell_) {
|
||||
log_assert(w->driverCell_->getPort(w->driverPort_) == w);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -630,7 +623,8 @@ void RTLIL::Cell::setPort(const RTLIL::IdString& portname, RTLIL::SigSpec signal
|
|||
// bufNormalize call
|
||||
if ((dir == RTLIL::PD_OUTPUT || dir == RTLIL::PD_INOUT) && signal.is_wire()) {
|
||||
Wire *w = signal.as_wire();
|
||||
if (w->driverCell_ == nullptr) {
|
||||
if (w->driverCell_ == nullptr && (
|
||||
(w->port_input && !w->port_output) == (type == ID($input_port)))) {
|
||||
w->driverCell_ = this;
|
||||
w->driverPort_ = portname;
|
||||
|
||||
|
|
|
|||
|
|
@ -124,7 +124,8 @@ struct PortarcsPass : Pass {
|
|||
TopoSort<SigBit> sort;
|
||||
|
||||
for (auto cell : m->cells())
|
||||
if (cell->type != ID($buf)) {
|
||||
// Ignore all bufnorm helper cells
|
||||
if (!cell->type.in(ID($buf), ID($input_port), ID($connect))) {
|
||||
auto tdata = tinfo.find(cell->type);
|
||||
if (tdata == tinfo.end())
|
||||
log_cmd_error("Missing timing data for module '%s'.\n", log_id(cell->type));
|
||||
|
|
|
|||
|
|
@ -1149,6 +1149,25 @@ struct HierarchyPass : public Pass {
|
|||
}
|
||||
}
|
||||
|
||||
if (flag_simcheck || flag_smtcheck) {
|
||||
for (auto mod : design->modules()) {
|
||||
for (auto cell : mod->cells()) {
|
||||
if (!cell->type.in(ID($check), ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
|
||||
continue;
|
||||
if (!cell->has_attribute(ID(unsupported_sva)))
|
||||
continue;
|
||||
|
||||
auto src = cell->get_src_attribute();
|
||||
|
||||
if (!src.empty())
|
||||
src += ": ";
|
||||
|
||||
log_error("%sProperty `%s' in module `%s' uses unsupported SVA constructs. See frontend warnings for details, run `chformal -remove a:unsupported_sva' to ignore.\n",
|
||||
src, log_id(cell->name), log_id(mod->name));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
if (!keep_positionals)
|
||||
{
|
||||
std::set<RTLIL::Module*> pos_mods;
|
||||
|
|
|
|||
|
|
@ -635,9 +635,17 @@ void rmunused_module(RTLIL::Module *module, bool purge_mode, bool unusedbitsattr
|
|||
}
|
||||
}
|
||||
for (auto cell : delcells) {
|
||||
if (verbose)
|
||||
log_debug(" removing buffer cell `%s': %s = %s\n", cell->name,
|
||||
log_signal(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::A)));
|
||||
if (verbose) {
|
||||
if (cell->type == ID($connect))
|
||||
log_debug(" removing connect cell `%s': %s <-> %s\n", cell->name,
|
||||
log_signal(cell->getPort(ID::A)), log_signal(cell->getPort(ID::B)));
|
||||
else if (cell->type == ID($input_port))
|
||||
log_debug(" removing input port marker cell `%s': %s\n", cell->name,
|
||||
log_signal(cell->getPort(ID::Y)));
|
||||
else
|
||||
log_debug(" removing buffer cell `%s': %s = %s\n", cell->name,
|
||||
log_signal(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::A)));
|
||||
}
|
||||
module->remove(cell);
|
||||
}
|
||||
if (!delcells.empty())
|
||||
|
|
|
|||
|
|
@ -144,12 +144,12 @@ struct ModuleIndex {
|
|||
}
|
||||
|
||||
if (nunused > 0) {
|
||||
log("Disconnected %d input bits of instance '%s' of '%s' in '%s'\n",
|
||||
log("Disconnected %d input bits of instance '%s' (type '%s') in '%s'\n",
|
||||
nunused, log_id(instantiation), log_id(instantiation->type), log_id(parent.module));
|
||||
changed = true;
|
||||
}
|
||||
if (nconstants > 0) {
|
||||
log("Substituting constant for %d output bits of instance '%s' of '%s' in '%s'\n",
|
||||
log("Substituting constant for %d output bits of instance '%s' (type '%s') in '%s'\n",
|
||||
nconstants, log_id(instantiation), log_id(instantiation->type), log_id(parent.module));
|
||||
changed = true;
|
||||
}
|
||||
|
|
@ -310,7 +310,7 @@ struct UsageData {
|
|||
refine_tie_togethers(inputs);
|
||||
}
|
||||
|
||||
bool apply_changes() {
|
||||
bool apply_changes(ModuleIndex &index) {
|
||||
bool did_something = false;
|
||||
|
||||
if (module->get_blackbox_attribute()) {
|
||||
|
|
@ -374,8 +374,16 @@ struct UsageData {
|
|||
// Propagate tied-together inputs
|
||||
dict<SigBit, SigBit> ties;
|
||||
for (auto group : tie_together_inputs) {
|
||||
for (int i = 1; i < group.size(); i++)
|
||||
ties[group[i]] = group[0];
|
||||
// Only consider used inputs for a tie-together group.
|
||||
// ModuleIndex::apply_changes might have disconnected
|
||||
// unused inputs.
|
||||
SigSpec filtered_group;
|
||||
for (auto bit : group) {
|
||||
if (index.used.check(bit))
|
||||
filtered_group.append(bit);
|
||||
}
|
||||
for (int i = 1; i < filtered_group.size(); i++)
|
||||
ties[filtered_group[i]] = filtered_group[0];
|
||||
}
|
||||
SigPool applied_ties;
|
||||
auto ties_rewrite = [&](SigSpec &signal) {
|
||||
|
|
@ -449,12 +457,13 @@ struct OptHierPass : Pass {
|
|||
|
||||
bool did_something = false;
|
||||
for (auto module : d->selected_modules(RTLIL::SELECT_WHOLE_ONLY, RTLIL::SB_UNBOXED_CMDERR)) {
|
||||
ModuleIndex &parent_index = indices.at(module->name);
|
||||
|
||||
if (usage_datas.count(module->name)) {
|
||||
log_debug("Applying usage data changes to %s\n", log_id(module));
|
||||
did_something |= usage_datas.at(module->name).apply_changes();
|
||||
did_something |= usage_datas.at(module->name).apply_changes(parent_index);
|
||||
}
|
||||
|
||||
ModuleIndex &parent_index = indices.at(module->name);
|
||||
for (auto cell : module->cells()) {
|
||||
if (indices.count(cell->type)) {
|
||||
log_debug("Applying changes to instance %s of %s in %s\n", log_id(cell), log_id(cell->type), log_id(module));
|
||||
|
|
|
|||
|
|
@ -246,10 +246,15 @@ struct OptMergeWorker
|
|||
// mem can have an excessively large parameter holding the init data
|
||||
continue;
|
||||
}
|
||||
if (cell->type == ID($scopeinfo))
|
||||
continue;
|
||||
if (mode_keepdc && has_dont_care_initval(cell))
|
||||
continue;
|
||||
if (ct.cell_known(cell->type) || (mode_share_all && cell->known()))
|
||||
cells.push_back(cell);
|
||||
if (!cell->known())
|
||||
continue;
|
||||
if (!mode_share_all && !ct.cell_known(cell->type))
|
||||
continue;
|
||||
cells.push_back(cell);
|
||||
}
|
||||
|
||||
did_something = false;
|
||||
|
|
@ -278,12 +283,6 @@ struct OptMergeWorker
|
|||
|
||||
for (auto cell : cells)
|
||||
{
|
||||
if ((!mode_share_all && !ct.cell_known(cell->type)) || !cell->known())
|
||||
continue;
|
||||
|
||||
if (cell->type == ID($scopeinfo))
|
||||
continue;
|
||||
|
||||
auto [cell_in_map, inserted] = known_cells.insert(cell);
|
||||
if (!inserted) {
|
||||
// We've failed to insert since we already have an equivalent cell
|
||||
|
|
|
|||
|
|
@ -0,0 +1,23 @@
|
|||
read_verilog <<EOF
|
||||
module tag_2x4(
|
||||
input R0_clk,
|
||||
input W0_clk,
|
||||
output x,
|
||||
);
|
||||
assign x = !W0_clk;
|
||||
endmodule
|
||||
|
||||
module top(input clock, output x, output flag);
|
||||
tag_2x4 tag_ext(
|
||||
.R0_clk (clock),
|
||||
.W0_clk (clock),
|
||||
.x (x)
|
||||
);
|
||||
assign flag = x ^ clock;
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
hierarchy -top top
|
||||
opt_hier
|
||||
flatten
|
||||
sat -verify -prove flag 1
|
||||
|
|
@ -0,0 +1,154 @@
|
|||
|
||||
read_aiger <<EOF
|
||||
aag 124 11 9 2 104
|
||||
2
|
||||
4
|
||||
6
|
||||
8
|
||||
10
|
||||
12
|
||||
14
|
||||
16
|
||||
18
|
||||
20
|
||||
22
|
||||
24 42
|
||||
26 57
|
||||
28 58
|
||||
30 68
|
||||
32 86
|
||||
34 113
|
||||
36 114
|
||||
38 105
|
||||
40 133
|
||||
228
|
||||
248
|
||||
42 26 5
|
||||
44 35 33
|
||||
46 36 3
|
||||
48 46 44
|
||||
50 36 31
|
||||
52 28 25
|
||||
54 53 50
|
||||
56 55 49
|
||||
58 38 25
|
||||
60 40 28
|
||||
62 60 25
|
||||
64 37 30
|
||||
66 64 24
|
||||
68 66 62
|
||||
70 29 7
|
||||
72 40 37
|
||||
74 7 2
|
||||
76 74 73
|
||||
78 76 12
|
||||
80 78 71
|
||||
82 76 13
|
||||
84 83 14
|
||||
86 84 80
|
||||
88 34 31
|
||||
90 89 58
|
||||
92 40 37
|
||||
94 39 26
|
||||
96 94 93
|
||||
98 96 91
|
||||
100 98 14
|
||||
102 39 6
|
||||
104 40 27
|
||||
106 104 103
|
||||
108 107 55
|
||||
110 109 98
|
||||
112 110 100
|
||||
114 24 10
|
||||
116 26 8
|
||||
118 7 5
|
||||
120 119 117
|
||||
122 5 3
|
||||
124 27 25
|
||||
126 125 123
|
||||
128 126 120
|
||||
130 129 83
|
||||
132 131 111
|
||||
134 48 12
|
||||
136 121 48
|
||||
138 137 135
|
||||
140 139 130
|
||||
142 138 81
|
||||
144 114 91
|
||||
146 145 57
|
||||
148 38 29
|
||||
150 148 25
|
||||
152 151 48
|
||||
154 153 69
|
||||
156 155 147
|
||||
158 157 143
|
||||
160 159 140
|
||||
162 147 81
|
||||
164 163 86
|
||||
166 165 21
|
||||
168 167 161
|
||||
170 169 22
|
||||
172 113 19
|
||||
174 133 113
|
||||
176 174 172
|
||||
178 108 83
|
||||
180 179 155
|
||||
182 181 19
|
||||
184 182 140
|
||||
186 185 177
|
||||
188 112 21
|
||||
190 189 176
|
||||
192 146 140
|
||||
194 192 164
|
||||
196 112 86
|
||||
198 196 165
|
||||
200 198 194
|
||||
202 181 156
|
||||
204 145 83
|
||||
206 205 17
|
||||
208 178 138
|
||||
210 209 206
|
||||
212 140 132
|
||||
214 212 210
|
||||
216 214 202
|
||||
218 194 161
|
||||
220 218 216
|
||||
222 220 201
|
||||
224 222 190
|
||||
226 224 186
|
||||
228 226 170
|
||||
230 167 157
|
||||
232 182 172
|
||||
234 193 21
|
||||
236 235 232
|
||||
238 202 197
|
||||
240 238 185
|
||||
242 238 188
|
||||
244 242 240
|
||||
246 244 237
|
||||
248 246 231
|
||||
c
|
||||
aigfuzz -s -1 1145242652
|
||||
seed 1145242652
|
||||
fuzzer layers
|
||||
depth 9
|
||||
width 19
|
||||
input fraction 13%
|
||||
latch fraction 84%
|
||||
lower fraction 20%
|
||||
monotonicity -1
|
||||
and closure
|
||||
EOF
|
||||
|
||||
bufnorm -update
|
||||
|
||||
delete -output o:* %R1
|
||||
opt_clean
|
||||
bufnorm -update
|
||||
|
||||
delete -output o:* %R1
|
||||
tee -q debug opt_clean
|
||||
bufnorm -update
|
||||
|
||||
bufnorm -reset
|
||||
opt_clean
|
||||
|
|
@ -0,0 +1,38 @@
|
|||
verific -sv <<EOF
|
||||
module top(input clk, input a, input b);
|
||||
|
||||
prop_supported: assert property (@(posedge clk) a ##1 b |=> b);
|
||||
prop_unsupported1: assert property (@(posedge clk) a ##1 b #=# b);
|
||||
prop_unsupported2: assert property (@(posedge clk) a ##1 @(posedge b) ##1 a);
|
||||
|
||||
sequence local_var_seq;
|
||||
logic v;
|
||||
(1, v = a) ##1 b ##1 (v == a);
|
||||
endsequence
|
||||
|
||||
prop_unsupported3: assert property (@(posedge clk) local_var_seq);
|
||||
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
logger -expect warning "Mixed clocking is currently not supported" 1
|
||||
logger -expect warning "Verific SVA primitive sva_non_overlapped_followed_by .* is currently unsupported in this context" 1
|
||||
logger -expect warning "SVA sequences with local variable assignments are currently not supported" 1
|
||||
logger -expect warning "Encountered 3 items containing unsupported SVA" 1
|
||||
verific -import -sva-continue-on-err top
|
||||
logger -check-expected
|
||||
|
||||
select -assert-count 4 top/t:$assert
|
||||
select -assert-count 4 top/a:unsupported_sva top/prop_supported %% top/t:$assert %i
|
||||
|
||||
select -assert-count 3 top/a:unsupported_sva
|
||||
select -assert-count 3 top/a:unsupported_sva top/prop_unsupported* %i
|
||||
select -assert-count 1 top/a:unsupported_sva top/prop_unsupported1 %i
|
||||
select -assert-count 1 top/a:unsupported_sva top/prop_unsupported2 %i
|
||||
select -assert-count 1 top/a:unsupported_sva top/prop_unsupported3 %i
|
||||
select -assert-count 0 top/a:unsupported_sva top/prop_supported %i
|
||||
select -assert-count 1 top/prop_supported
|
||||
|
||||
logger -expect error "uses unsupported SVA constructs." 1
|
||||
hierarchy -smtcheck -top top
|
||||
logger -check-expected
|
||||
|
|
@ -0,0 +1,31 @@
|
|||
verific -sv <<EOF
|
||||
module top(input clk, input a, input b);
|
||||
|
||||
prop_supported1: assert property (@(posedge clk) a ##1 b |=> b);
|
||||
|
||||
prop_exploding: assert property (@(posedge clk)
|
||||
((a [*7] ##1 b) [*11]) and
|
||||
((a [*11] ##1 b) [*7]) and
|
||||
((a [*13] ##1 b) [*5]) and
|
||||
((a [*5] ##1 b) [*13])
|
||||
);
|
||||
|
||||
prop_supported2: assert property (@(posedge clk) a [*5] ##1 b |=> b);
|
||||
|
||||
endmodule
|
||||
EOF
|
||||
|
||||
logger -expect warning "Stopping to prevent exponential design size explosion." 1
|
||||
verific -import -sva-continue-on-err top
|
||||
logger -check-expected
|
||||
|
||||
select -assert-count 3 top/t:$assert
|
||||
select -assert-count 1 top/a:unsupported_sva top/prop_exploding %% top/t:$assert %i
|
||||
|
||||
select -assert-count 0 top/a:unsupported_sva top/prop_supported1 %i
|
||||
select -assert-count 0 top/a:unsupported_sva top/prop_supported2 %i
|
||||
select -assert-count 2 top/prop_supported*
|
||||
|
||||
logger -expect error "uses unsupported SVA constructs." 1
|
||||
hierarchy -smtcheck -top top
|
||||
logger -check-expected
|
||||
|
|
@ -0,0 +1,9 @@
|
|||
|
||||
verific -sv <<EOF
|
||||
module top(input clk, input a, input b);
|
||||
prop_unsupported: assert property (@(posedge clk) a ##1 @(posedge b) ##1 a);
|
||||
endmodule;
|
||||
EOF
|
||||
|
||||
logger -expect error "Mixed clocking is currently not supported" 1
|
||||
verific -import top
|
||||
Loading…
Reference in New Issue