riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add "verific -import -flatten" and "verific -import -v"

This commit is contained in:
Clifford Wolf 2017-07-24 11:29:06 +02:00
parent 84f15260b5
commit 92d3aad670
1 changed files with 164 additions and 107 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

271
frontends/verific/verific.cc
View File

@ -80,9 +80,27 @@ void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefil
struct VerificImporter struct VerificImporter
{ {
RTLIL::Module *module; RTLIL::Module *module;
Netlist *netlist;
std::map<Net*, RTLIL::SigBit> net_map; std::map<Net*, RTLIL::SigBit> net_map;
std::map<Net*, Net*> sva_posedge_map; std::map<Net*, Net*> sva_posedge_map;
bool mode_gates, mode_keep, verbose;
VerificImporter(bool mode_gates, bool mode_keep, bool verbose) :
mode_gates(mode_gates), mode_keep(mode_keep), verbose(verbose)
{
}
RTLIL::SigBit net_map_at(Net *net)
{
if (net->IsExternalTo(netlist))
log_error("Found unflattened external reference to net '%s' in netlist '%s' from netlist '%s'.\n",
net->Name(), net->Owner()->CellBaseName(), netlist->CellBaseName());
return net_map.at(net);
}
void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
{ {
MapIter mi; MapIter mi;
@ -101,7 +119,7 @@ struct VerificImporter
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
for (int i = int(inst->InputSize())-1; i >= 0; i--) for (int i = int(inst->InputSize())-1; i >= 0; i--)
if (inst->GetInputBit(i)) if (inst->GetInputBit(i))
sig.append(net_map.at(inst->GetInputBit(i))); sig.append(net_map_at(inst->GetInputBit(i)));
else else
sig.append(RTLIL::State::Sz); sig.append(RTLIL::State::Sz);
return sig; return sig;
@ -112,7 +130,7 @@ struct VerificImporter
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
for (int i = int(inst->Input1Size())-1; i >= 0; i--) for (int i = int(inst->Input1Size())-1; i >= 0; i--)
if (inst->GetInput1Bit(i)) if (inst->GetInput1Bit(i))
sig.append(net_map.at(inst->GetInput1Bit(i))); sig.append(net_map_at(inst->GetInput1Bit(i)));
else else
sig.append(RTLIL::State::Sz); sig.append(RTLIL::State::Sz);
return sig; return sig;
@ -123,7 +141,7 @@ struct VerificImporter
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
for (int i = int(inst->Input2Size())-1; i >= 0; i--) for (int i = int(inst->Input2Size())-1; i >= 0; i--)
if (inst->GetInput2Bit(i)) if (inst->GetInput2Bit(i))
sig.append(net_map.at(inst->GetInput2Bit(i))); sig.append(net_map_at(inst->GetInput2Bit(i)));
else else
sig.append(RTLIL::State::Sz); sig.append(RTLIL::State::Sz);
return sig; return sig;
@ -142,7 +160,7 @@ struct VerificImporter
else if (net->IsPwr()) else if (net->IsPwr())
sig.append(RTLIL::State::S1); sig.append(RTLIL::State::S1);
else else
sig.append(net_map.at(net)); sig.append(net_map_at(net));
} else } else
sig.append(RTLIL::State::Sz); sig.append(RTLIL::State::Sz);
} }
@ -151,7 +169,7 @@ struct VerificImporter
Port *port = inst->View()->GetPort(portname); Port *port = inst->View()->GetPort(portname);
log_assert(port != NULL); log_assert(port != NULL);
Net *net = inst->GetNet(port); Net *net = inst->GetNet(port);
return net_map.at(net); return net_map_at(net);
} }
} }
@ -161,7 +179,7 @@ struct VerificImporter
RTLIL::Wire *dummy_wire = NULL; RTLIL::Wire *dummy_wire = NULL;
for (int i = int(inst->OutputSize())-1; i >= 0; i--) for (int i = int(inst->OutputSize())-1; i >= 0; i--)
if (inst->GetOutputBit(i)) { if (inst->GetOutputBit(i)) {
sig.append(net_map.at(inst->GetOutputBit(i))); sig.append(net_map_at(inst->GetOutputBit(i)));
dummy_wire = NULL; dummy_wire = NULL;
} else { } else {
if (dummy_wire == NULL) if (dummy_wire == NULL)
@ -176,64 +194,64 @@ struct VerificImporter
bool import_netlist_instance_gates(Instance *inst) bool import_netlist_instance_gates(Instance *inst)
{ {
if (inst->Type() == PRIM_AND) { if (inst->Type() == PRIM_AND) {
module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addAndGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_NAND) { if (inst->Type() == PRIM_NAND) {
RTLIL::SigSpec tmp = module->addWire(NEW_ID); RTLIL::SigSpec tmp = module->addWire(NEW_ID);
module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); module->addAndGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_OR) { if (inst->Type() == PRIM_OR) {
module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addOrGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_NOR) { if (inst->Type() == PRIM_NOR) {
RTLIL::SigSpec tmp = module->addWire(NEW_ID); RTLIL::SigSpec tmp = module->addWire(NEW_ID);
module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); module->addOrGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_XOR) { if (inst->Type() == PRIM_XOR) {
module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addXorGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_XNOR) { if (inst->Type() == PRIM_XNOR) {
module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_BUF) { if (inst->Type() == PRIM_BUF) {
module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); module->addBufGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_INV) { if (inst->Type() == PRIM_INV) {
module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); module->addNotGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_MUX) { if (inst->Type() == PRIM_MUX) {
module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_TRI) { if (inst->Type() == PRIM_TRI) {
module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_FADD) if (inst->Type() == PRIM_FADD)
{ {
RTLIL::SigSpec a = net_map.at(inst->GetInput1()), b = net_map.at(inst->GetInput2()), c = net_map.at(inst->GetCin()); RTLIL::SigSpec a = net_map_at(inst->GetInput1()), b = net_map_at(inst->GetInput2()), c = net_map_at(inst->GetCin());
RTLIL::SigSpec x = inst->GetCout() ? net_map.at(inst->GetCout()) : module->addWire(NEW_ID); RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(NEW_ID);
RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID); RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
RTLIL::SigSpec tmp1 = module->addWire(NEW_ID); RTLIL::SigSpec tmp1 = module->addWire(NEW_ID);
RTLIL::SigSpec tmp2 = module->addWire(NEW_ID); RTLIL::SigSpec tmp2 = module->addWire(NEW_ID);
RTLIL::SigSpec tmp3 = module->addWire(NEW_ID); RTLIL::SigSpec tmp3 = module->addWire(NEW_ID);
@ -248,16 +266,16 @@ struct VerificImporter
if (inst->Type() == PRIM_DFFRS) if (inst->Type() == PRIM_DFFRS)
{ {
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); module->addDffGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else if (inst->GetSet()->IsGnd()) else if (inst->GetSet()->IsGnd())
module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()), module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false);
else if (inst->GetReset()->IsGnd()) else if (inst->GetReset()->IsGnd())
module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true);
else else
module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
@ -267,88 +285,88 @@ struct VerificImporter
bool import_netlist_instance_cells(Instance *inst) bool import_netlist_instance_cells(Instance *inst)
{ {
if (inst->Type() == PRIM_AND) { if (inst->Type() == PRIM_AND) {
module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addAnd(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_NAND) { if (inst->Type() == PRIM_NAND) {
RTLIL::SigSpec tmp = module->addWire(NEW_ID); RTLIL::SigSpec tmp = module->addWire(NEW_ID);
module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); module->addAnd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_OR) { if (inst->Type() == PRIM_OR) {
module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addOr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_NOR) { if (inst->Type() == PRIM_NOR) {
RTLIL::SigSpec tmp = module->addWire(NEW_ID); RTLIL::SigSpec tmp = module->addWire(NEW_ID);
module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp); module->addOr(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput())); module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_XOR) { if (inst->Type() == PRIM_XOR) {
module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addXor(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_XNOR) { if (inst->Type() == PRIM_XNOR) {
module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput())); module->addXnor(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_INV) { if (inst->Type() == PRIM_INV) {
module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); module->addNot(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_MUX) { if (inst->Type() == PRIM_MUX) {
module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); module->addMux(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_TRI) { if (inst->Type() == PRIM_TRI) {
module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput())); module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_FADD) if (inst->Type() == PRIM_FADD)
{ {
RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2); RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID); RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
if (inst->GetCout()) if (inst->GetCout())
y.append(net_map.at(inst->GetCout())); y.append(net_map_at(inst->GetCout()));
module->addAdd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), a_plus_b); module->addAdd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y); module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map_at(inst->GetCin()), y);
return true; return true;
} }
if (inst->Type() == PRIM_DFFRS) if (inst->Type() == PRIM_DFFRS)
{ {
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); module->addDff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else if (inst->GetSet()->IsGnd()) else if (inst->GetSet()->IsGnd())
module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()), module->addAdff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
else if (inst->GetReset()->IsGnd()) else if (inst->GetReset()->IsGnd())
module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), module->addAdff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
else else
module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), module->addDffsr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
if (inst->Type() == PRIM_DLATCHRS) if (inst->Type() == PRIM_DLATCHRS)
{ {
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); module->addDlatch(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else else
module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()), module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
@ -361,13 +379,13 @@ struct VerificImporter
if (inst->Type() == OPER_ADDER) { if (inst->Type() == OPER_ADDER) {
RTLIL::SigSpec out = OUT; RTLIL::SigSpec out = OUT;
if (inst->GetCout() != NULL) if (inst->GetCout() != NULL)
out.append(net_map.at(inst->GetCout())); out.append(net_map_at(inst->GetCout()));
if (inst->GetCin()->IsGnd()) { if (inst->GetCin()->IsGnd()) {
module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED); module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED);
} else { } else {
RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out)); RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED); module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false); module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetCin()), out, false);
} }
return true; return true;
} }
@ -399,7 +417,7 @@ struct VerificImporter
if (inst->Type() == OPER_ENABLED_DECODER) { if (inst->Type() == OPER_ENABLED_DECODER) {
RTLIL::SigSpec vec; RTLIL::SigSpec vec;
vec.append(net_map.at(inst->GetControl())); vec.append(net_map_at(inst->GetControl()));
for (unsigned i = 1; i < inst->OutputSize(); i++) { for (unsigned i = 1; i < inst->OutputSize(); i++) {
vec.append(RTLIL::State::S0); vec.append(RTLIL::State::S0);
} }
@ -430,31 +448,31 @@ struct VerificImporter
} }
if (inst->Type() == OPER_REDUCE_AND) { if (inst->Type() == OPER_REDUCE_AND) {
module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED);
return true; return true;
} }
if (inst->Type() == OPER_REDUCE_OR) { if (inst->Type() == OPER_REDUCE_OR) {
module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED);
return true; return true;
} }
if (inst->Type() == OPER_REDUCE_XOR) { if (inst->Type() == OPER_REDUCE_XOR) {
module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED);
return true; return true;
} }
if (inst->Type() == OPER_REDUCE_XNOR) { if (inst->Type() == OPER_REDUCE_XNOR) {
module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED); module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED);
return true; return true;
} }
if (inst->Type() == OPER_LESSTHAN) { if (inst->Type() == OPER_LESSTHAN) {
Net *net_cin = inst->GetCin(); Net *net_cin = inst->GetCin();
if (net_cin->IsGnd()) if (net_cin->IsGnd())
module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
else if (net_cin->IsPwr()) else if (net_cin->IsPwr())
module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
else else
log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name()); log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
return true; return true;
@ -501,22 +519,22 @@ struct VerificImporter
} }
if (inst->Type() == OPER_EQUAL) { if (inst->Type() == OPER_EQUAL) {
module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
return true; return true;
} }
if (inst->Type() == OPER_NEQUAL) { if (inst->Type() == OPER_NEQUAL) {
module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED); module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
return true; return true;
} }
if (inst->Type() == OPER_WIDE_MUX) { if (inst->Type() == OPER_WIDE_MUX) {
module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT); module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetControl()), OUT);
return true; return true;
} }
if (inst->Type() == OPER_WIDE_TRI) { if (inst->Type() == OPER_WIDE_TRI) {
module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT); module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
return true; return true;
} }
@ -524,9 +542,9 @@ struct VerificImporter
RTLIL::SigSpec sig_set = operatorInport(inst, "set"); RTLIL::SigSpec sig_set = operatorInport(inst, "set");
RTLIL::SigSpec sig_reset = operatorInport(inst, "reset"); RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool()) if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT); module->addDff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), IN, OUT);
else else
module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT); module->addDffsr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
return true; return true;
} }
@ -539,10 +557,12 @@ struct VerificImporter
return false; return false;
} }
void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates, bool mode_keep) void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
{ {
std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name()); std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
netlist = nl;
if (design->has(module_name)) { if (design->has(module_name)) {
if (!nl->IsOperator()) if (!nl->IsOperator())
log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name()); log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
@ -574,7 +594,8 @@ struct VerificImporter
if (port->Bus()) if (port->Bus())
continue; continue;
// log(" importing port %s.\n", port->Name()); if (verbose)
log(" importing port %s.\n", port->Name());
RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name())); RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
import_attributes(wire->attributes, port); import_attributes(wire->attributes, port);
@ -591,15 +612,16 @@ struct VerificImporter
if (net_map.count(net) == 0) if (net_map.count(net) == 0)
net_map[net] = wire; net_map[net] = wire;
else if (wire->port_input) else if (wire->port_input)
module->connect(net_map.at(net), wire); module->connect(net_map_at(net), wire);
else else
module->connect(wire, net_map.at(net)); module->connect(wire, net_map_at(net));
} }
} }
FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus) FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
{ {
// log(" importing portbus %s.\n", portbus->Name()); if (verbose)
log(" importing portbus %s.\n", portbus->Name());
RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size()); RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex()); wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
@ -617,9 +639,9 @@ struct VerificImporter
if (net_map.count(net) == 0) if (net_map.count(net) == 0)
net_map[net] = bit; net_map[net] = bit;
else if (wire->port_input) else if (wire->port_input)
module->connect(net_map.at(net), bit); module->connect(net_map_at(net), bit);
else else
module->connect(bit, net_map.at(net)); module->connect(bit, net_map_at(net));
} }
if (i == portbus->RightIndex()) if (i == portbus->RightIndex())
break; break;
@ -712,14 +734,16 @@ struct VerificImporter
anyseq_nets.insert(net); anyseq_nets.insert(net);
if (net_map.count(net)) { if (net_map.count(net)) {
// log(" skipping net %s.\n", net->Name()); if (verbose)
log(" skipping net %s.\n", net->Name());
continue; continue;
} }
if (net->Bus()) if (net->Bus())
continue; continue;
// log(" importing net %s.\n", net->Name()); if (verbose)
log(" importing net %s.\n", net->Name());
RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name())); RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
RTLIL::Wire *wire = module->addWire(wire_name); RTLIL::Wire *wire = module->addWire(wire_name);
@ -741,7 +765,8 @@ struct VerificImporter
if (found_new_net) if (found_new_net)
{ {
// log(" importing netbus %s.\n", netbus->Name()); if (verbose)
log(" importing netbus %s.\n", netbus->Name());
RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name())); RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name()));
RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size()); RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
@ -771,7 +796,7 @@ struct VerificImporter
if (net_map.count(net) == 0) if (net_map.count(net) == 0)
net_map[net] = bit; net_map[net] = bit;
else else
module->connect(bit, net_map.at(net)); module->connect(bit, net_map_at(net));
} }
if (i == netbus->RightIndex()) if (i == netbus->RightIndex())
@ -783,7 +808,8 @@ struct VerificImporter
} }
else else
{ {
// log(" skipping netbus %s.\n", netbus->Name()); if (verbose)
log(" skipping netbus %s.\n", netbus->Name());
} }
SigSpec anyconst_sig; SigSpec anyconst_sig;
@ -792,11 +818,11 @@ struct VerificImporter
for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) { for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
net = netbus->ElementAtIndex(i); net = netbus->ElementAtIndex(i);
if (net != nullptr && anyconst_nets.count(net)) { if (net != nullptr && anyconst_nets.count(net)) {
anyconst_sig.append(net_map.at(net)); anyconst_sig.append(net_map_at(net));
anyconst_nets.erase(net); anyconst_nets.erase(net);
} }
if (net != nullptr && anyseq_nets.count(net)) { if (net != nullptr && anyseq_nets.count(net)) {
anyseq_sig.append(net_map.at(net)); anyseq_sig.append(net_map_at(net));
anyseq_nets.erase(net); anyseq_nets.erase(net);
} }
if (i == netbus->LeftIndex()) if (i == netbus->LeftIndex())
@ -813,7 +839,7 @@ struct VerificImporter
for (auto it : init_nets) for (auto it : init_nets)
{ {
Const initval; Const initval;
SigBit bit = net_map.at(it.first); SigBit bit = net_map_at(it.first);
log_assert(bit.wire); log_assert(bit.wire);
if (bit.wire->attributes.count("\\init")) if (bit.wire->attributes.count("\\init"))
@ -831,10 +857,10 @@ struct VerificImporter
} }
for (auto net : anyconst_nets) for (auto net : anyconst_nets)
module->connect(net_map.at(net), module->Anyconst(NEW_ID)); module->connect(net_map_at(net), module->Anyconst(NEW_ID));
for (auto net : anyseq_nets) for (auto net : anyseq_nets)
module->connect(net_map.at(net), module->Anyseq(NEW_ID)); module->connect(net_map_at(net), module->Anyseq(NEW_ID));
FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{ {
@ -851,7 +877,9 @@ struct VerificImporter
if (inst->Type() == PRIM_SVA_POSEDGE) if (inst->Type() == PRIM_SVA_POSEDGE)
continue; continue;
// log(" importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name()); if (verbose)
log(" importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name());
if (inst->Type() == PRIM_SVA_AT) if (inst->Type() == PRIM_SVA_AT)
{ {
@ -865,54 +893,54 @@ struct VerificImporter
log_assert(sva_posedge_map.count(in1)); log_assert(sva_posedge_map.count(in1));
Net *clk = sva_posedge_map.at(in1); Net *clk = sva_posedge_map.at(in1);
SigBit outsig = net_map.at(out); SigBit outsig = net_map_at(out);
log_assert(outsig.wire && GetSize(outsig.wire) == 1); log_assert(outsig.wire && GetSize(outsig.wire) == 1);
outsig.wire->attributes["\\init"] = Const(1, 1); outsig.wire->attributes["\\init"] = Const(1, 1);
module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out)); module->addDff(NEW_ID, net_map_at(clk), net_map_at(in2), net_map_at(out));
continue; continue;
} }
if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_ASSERT) { if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_ASSERT) {
Net *in = inst->GetInput(); Net *in = inst->GetInput();
module->addAssert(NEW_ID, net_map.at(in), State::S1); module->addAssert(NEW_ID, net_map_at(in), State::S1);
continue; continue;
} }
if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_ASSUME) { if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_ASSUME) {
Net *in = inst->GetInput(); Net *in = inst->GetInput();
module->addAssume(NEW_ID, net_map.at(in), State::S1); module->addAssume(NEW_ID, net_map_at(in), State::S1);
continue; continue;
} }
if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) { if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) {
Net *in = inst->GetInput(); Net *in = inst->GetInput();
module->addCover(NEW_ID, net_map.at(in), State::S1); module->addCover(NEW_ID, net_map_at(in), State::S1);
continue; continue;
} }
if (inst->Type() == PRIM_PWR) { if (inst->Type() == PRIM_PWR) {
module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1); module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
continue; continue;
} }
if (inst->Type() == PRIM_GND) { if (inst->Type() == PRIM_GND) {
module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0); module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
continue; continue;
} }
if (inst->Type() == PRIM_BUF) { if (inst->Type() == PRIM_BUF) {
module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput())); module->addBufGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
continue; continue;
} }
if (inst->Type() == PRIM_X) { if (inst->Type() == PRIM_X) {
module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx); module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
continue; continue;
} }
if (inst->Type() == PRIM_Z) { if (inst->Type() == PRIM_Z) {
module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz); module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
continue; continue;
} }
@ -955,14 +983,14 @@ struct VerificImporter
cell->parameters["\\PRIORITY"] = 0; cell->parameters["\\PRIORITY"] = 0;
cell->parameters["\\ABITS"] = GetSize(addr); cell->parameters["\\ABITS"] = GetSize(addr);
cell->parameters["\\WIDTH"] = GetSize(data); cell->parameters["\\WIDTH"] = GetSize(data);
cell->setPort("\\EN", RTLIL::SigSpec(net_map.at(inst->GetControl())).repeat(GetSize(data))); cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
cell->setPort("\\CLK", RTLIL::State::S0); cell->setPort("\\CLK", RTLIL::State::S0);
cell->setPort("\\ADDR", addr); cell->setPort("\\ADDR", addr);
cell->setPort("\\DATA", data); cell->setPort("\\DATA", data);
if (inst->Type() == OPER_CLOCKED_WRITE_PORT) { if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
cell->parameters["\\CLK_ENABLE"] = true; cell->parameters["\\CLK_ENABLE"] = true;
cell->setPort("\\CLK", net_map.at(inst->GetClock())); cell->setPort("\\CLK", net_map_at(inst->GetClock()));
} }
continue; continue;
} }
@ -991,8 +1019,12 @@ struct VerificImporter
dict<IdString, vector<SigBit>> cell_port_conns; dict<IdString, vector<SigBit>> cell_port_conns;
if (verbose)
log(" ports in verific db:\n");
FOREACH_PORTREF_OF_INST(inst, mi2, pr) { FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
// log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name()); if (verbose)
log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
const char *port_name = pr->GetPort()->Name(); const char *port_name = pr->GetPort()->Name();
int port_offset = 0; int port_offset = 0;
if (pr->GetPort()->Bus()) { if (pr->GetPort()->Bus()) {
@ -1007,11 +1039,15 @@ struct VerificImporter
for (auto bit : zwires) for (auto bit : zwires)
sigvec.push_back(bit); sigvec.push_back(bit);
} }
sigvec[port_offset] = net_map.at(pr->GetNet()); sigvec[port_offset] = net_map_at(pr->GetNet());
} }
if (verbose)
log(" ports in yosys db:\n");
for (auto &it : cell_port_conns) { for (auto &it : cell_port_conns) {
// log(" .%s(%s)\n", log_id(it.first), log_signal(it.second)); if (verbose)
log(" .%s(%s)\n", log_id(it.first), log_signal(it.second));
cell->setPort(it.first, it.second); cell->setPort(it.first, it.second);
} }
} }
@ -1036,13 +1072,19 @@ struct VerificPass : public Pass {
log("Load the specified VHDL files into Verific.\n"); log("Load the specified VHDL files into Verific.\n");
log("\n"); log("\n");
log("\n"); log("\n");
log(" verific -import [-gates] [-k] {-all | <top-module>..}\n"); log(" verific -import [-gates] [-flatten] [-v] [-k] {-all | <top-module>..}\n");
log("\n"); log("\n");
log("Elaborate the design for the specified top modules, import to Yosys and\n"); log("Elaborate the design for the specified top modules, import to Yosys and\n");
log("reset the internal state of Verific. A gate-level netlist is created\n"); log("reset the internal state of Verific. A gate-level netlist is created\n");
log("when called with -gates. In -k mode unsupported verific primitives are\n"); log("when called with -gates.\n");
log("added as blockbox modules to the design instead of triggering a fatal\n"); log("\n");
log("error (only useful for debugging this command).\n"); log("In -flatten mode the import command flattens the netlist before importing it.\n");
log("\n");
log("In -v mode the import command produces more verbose log output.\n");
log("\n");
log("In -k mode unsupported verific primitives are added as blockbox modules\n");
log("to the design instead of triggering a fatal error (only useful for\n");
log("debugging/extending this command).\n");
log("\n"); log("\n");
log("Visit http://verific.com/ for more information on Verific.\n"); log("Visit http://verific.com/ for more information on Verific.\n");
log("\n"); log("\n");
@ -1054,6 +1096,7 @@ struct VerificPass : public Pass {
Message::SetConsoleOutput(0); Message::SetConsoleOutput(0);
Message::RegisterCallBackMsg(msg_func); Message::RegisterCallBackMsg(msg_func);
RuntimeFlags::SetVar("db_allow_external_nets", 1);
const char *release_str = Message::ReleaseString(); const char *release_str = Message::ReleaseString();
time_t release_time = Message::ReleaseDate(); time_t release_time = Message::ReleaseDate();
@ -1148,6 +1191,7 @@ struct VerificPass : public Pass {
{ {
std::set<Netlist*> nl_todo, nl_done; std::set<Netlist*> nl_todo, nl_done;
bool mode_all = false, mode_gates = false, mode_keep = false; bool mode_all = false, mode_gates = false, mode_keep = false;
bool verbose = false, flatten = false;
for (argidx++; argidx < GetSize(args); argidx++) { for (argidx++; argidx < GetSize(args); argidx++) {
if (args[argidx] == "-all") { if (args[argidx] == "-all") {
@ -1158,10 +1202,18 @@ struct VerificPass : public Pass {
mode_gates = true; mode_gates = true;
continue; continue;
} }
if (args[argidx] == "-flatten") {
flatten = true;
continue;
}
if (args[argidx] == "-k") { if (args[argidx] == "-k") {
mode_keep = true; mode_keep = true;
continue; continue;
} }
if (args[argidx] == "-v") {
verbose = true;
continue;
}
break; break;
} }
@ -1205,11 +1257,16 @@ struct VerificPass : public Pass {
} }
} }
if (flatten) {
for (auto nl : nl_todo)
nl->Flatten();
}
while (!nl_todo.empty()) { while (!nl_todo.empty()) {
Netlist *nl = *nl_todo.begin(); Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) { if (nl_done.count(nl) == 0) {
VerificImporter importer; VerificImporter importer(mode_gates, mode_keep, verbose);
importer.import_netlist(design, nl, nl_todo, mode_gates, mode_keep); importer.import_netlist(design, nl, nl_todo);
} }
nl_todo.erase(nl); nl_todo.erase(nl);
nl_done.insert(nl); nl_done.insert(nl);