mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 12:28:44 +00:00
Code Activity

Add assert/assume support to verific front-end

Browse source
This commit is contained in:
Clifford Wolf 2017-02-04 13:36:00 +01:00
parent 249ddbc16c
commit 911c44d164
2 changed files with 769 additions and 707 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frontends/verific/build_amd64.txt
View file

@ -6,7 +6,7 @@ only have the i386 eval version of Verific:
1.) Use a Makefile.conf like the following one: 1.) Use a Makefile.conf like the following one:
--snip-- --snip--
CONFIG := clang CONFIG := gcc
ENABLE_TCL := 0 ENABLE_TCL := 0
ENABLE_PLUGINS := 0 ENABLE_PLUGINS := 0
ENABLE_VERIFIC := 1 ENABLE_VERIFIC := 1

122
frontends/verific/verific.cc
View file

@ -49,7 +49,13 @@ USING_YOSYS_NAMESPACE
using namespace Verific ; using namespace Verific ;
#endif #endif
static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args) #endif
PRIVATE_NAMESPACE_BEGIN
#ifdef YOSYS_ENABLE_VERIFIC
void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
{ {
log("VERIFIC-%s [%s] ", log("VERIFIC-%s [%s] ",
msg_type == VERIFIC_NONE ? "NONE" : msg_type == VERIFIC_NONE ? "NONE" :
@ -65,7 +71,13 @@ static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type
log("\n"); log("\n");
} }
static void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) struct VerificImporter
{
RTLIL::Module *module;
std::map<Net*, RTLIL::SigBit> net_map;
std::map<Net*, Net*> sva_posedge_map;
void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
{ {
MapIter mi; MapIter mi;
Att *attr; Att *attr;
@ -78,7 +90,7 @@ static void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, D
attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
} }
static RTLIL::SigSpec operatorInput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map) RTLIL::SigSpec operatorInput(Instance *inst)
{ {
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--)
@ -89,7 +101,7 @@ static RTLIL::SigSpec operatorInput(Instance *inst, std::map<Net*, RTLIL::SigBit
return sig; return sig;
} }
static RTLIL::SigSpec operatorInput1(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map) RTLIL::SigSpec operatorInput1(Instance *inst)
{ {
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--)
@ -100,7 +112,7 @@ static RTLIL::SigSpec operatorInput1(Instance *inst, std::map<Net*, RTLIL::SigBi
return sig; return sig;
} }
static RTLIL::SigSpec operatorInput2(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map) RTLIL::SigSpec operatorInput2(Instance *inst)
{ {
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--)
@ -111,7 +123,7 @@ static RTLIL::SigSpec operatorInput2(Instance *inst, std::map<Net*, RTLIL::SigBi
return sig; return sig;
} }
static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::map<Net*, RTLIL::SigBit> &net_map) RTLIL::SigSpec operatorInport(Instance *inst, const char *portname)
{ {
PortBus *portbus = inst->View()->GetPortBus(portname); PortBus *portbus = inst->View()->GetPortBus(portname);
if (portbus) { if (portbus) {
@ -137,7 +149,7 @@ static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::
} }
} }
static RTLIL::SigSpec operatorOutput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map, RTLIL::Module *module) RTLIL::SigSpec operatorOutput(Instance *inst)
{ {
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
RTLIL::Wire *dummy_wire = NULL; RTLIL::Wire *dummy_wire = NULL;
@ -155,7 +167,7 @@ static RTLIL::SigSpec operatorOutput(Instance *inst, std::map<Net*, RTLIL::SigBi
return sig; return sig;
} }
static bool import_netlist_instance_gates(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, 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()));
@ -246,7 +258,7 @@ static bool import_netlist_instance_gates(RTLIL::Module *module, std::map<Net*,
return false; return false;
} }
static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, 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()));
@ -334,10 +346,10 @@ static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*,
return true; return true;
} }
#define IN operatorInput(inst, net_map) #define IN operatorInput(inst)
#define IN1 operatorInput1(inst, net_map) #define IN1 operatorInput1(inst)
#define IN2 operatorInput2(inst, net_map) #define IN2 operatorInput2(inst)
#define OUT operatorOutput(inst, net_map, module) #define OUT operatorOutput(inst)
#define SIGNED inst->View()->IsSigned() #define SIGNED inst->View()->IsSigned()
if (inst->Type() == OPER_ADDER) { if (inst->Type() == OPER_ADDER) {
@ -503,8 +515,8 @@ static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*,
} }
if (inst->Type() == OPER_WIDE_DFFRS) { if (inst->Type() == OPER_WIDE_DFFRS) {
RTLIL::SigSpec sig_set = operatorInport(inst, "set", net_map); RTLIL::SigSpec sig_set = operatorInport(inst, "set");
RTLIL::SigSpec sig_reset = operatorInport(inst, "reset", net_map); 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
@ -521,7 +533,7 @@ static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*,
return false; return false;
} }
static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates) void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates)
{ {
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());
@ -531,14 +543,12 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
return; return;
} }
RTLIL::Module *module = new RTLIL::Module; module = new RTLIL::Module;
module->name = module_name; module->name = module_name;
design->add(module); design->add(module);
log("Importing module %s.\n", RTLIL::id2cstr(module->name)); log("Importing module %s.\n", RTLIL::id2cstr(module->name));
std::map<Net*, RTLIL::SigBit> net_map;
SetIter si; SetIter si;
MapIter mi, mi2; MapIter mi, mi2;
Port *port; Port *port;
@ -694,8 +704,59 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{ {
if (inst->Type() == PRIM_SVA_POSEDGE) {
Net *in_net = inst->GetInput();
Net *out_net = inst->GetOutput();
sva_posedge_map[out_net] = in_net;
continue;
}
}
FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{
if (inst->Type() == PRIM_SVA_POSEDGE)
continue;
// log(" importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name()); // log(" importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name());
if (inst->Type() == PRIM_SVA_AT)
{
Net *in1 = inst->GetInput1();
Net *in2 = inst->GetInput2();
Net *out = inst->GetOutput();
if (sva_posedge_map.count(in2))
std::swap(in1, in2);
log_assert(sva_posedge_map.count(in1));
Net *clk = sva_posedge_map.at(in1);
SigBit outsig = net_map.at(out);
log_assert(outsig.wire && GetSize(outsig.wire) == 1);
outsig.wire->attributes["\\init"] == Const(0, 1);
module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out));
continue;
}
if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_ASSERT) {
Net *in = inst->GetInput();
module->addAssert(NEW_ID, net_map.at(in), State::S1);
continue;
}
if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_ASSUME) {
Net *in = inst->GetInput();
module->addAssume(NEW_ID, net_map.at(in), State::S1);
continue;
}
if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) {
// Net *in = inst->GetInput();
// module->addCover(NEW_ID, net_map.at(in), State::S1);
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;
@ -727,8 +788,8 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
if (memory->width != int(inst->OutputSize())) if (memory->width != int(inst->OutputSize()))
log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name()); log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
RTLIL::SigSpec addr = operatorInput1(inst, net_map); RTLIL::SigSpec addr = operatorInput1(inst);
RTLIL::SigSpec data = operatorOutput(inst, net_map, module); RTLIL::SigSpec data = operatorOutput(inst);
RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd"); RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd");
cell->parameters["\\MEMID"] = memory->name.str(); cell->parameters["\\MEMID"] = memory->name.str();
@ -750,8 +811,8 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
if (memory->width != int(inst->Input2Size())) if (memory->width != int(inst->Input2Size()))
log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name()); log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
RTLIL::SigSpec addr = operatorInput1(inst, net_map); RTLIL::SigSpec addr = operatorInput1(inst);
RTLIL::SigSpec data = operatorInput2(inst, net_map); RTLIL::SigSpec data = operatorInput2(inst);
RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr"); RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr");
cell->parameters["\\MEMID"] = memory->name.str(); cell->parameters["\\MEMID"] = memory->name.str();
@ -773,12 +834,12 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
} }
if (!mode_gates) { if (!mode_gates) {
if (import_netlist_instance_cells(module, net_map, inst)) if (import_netlist_instance_cells(inst))
continue; continue;
if (inst->IsOperator()) if (inst->IsOperator())
log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name()); log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
} else { } else {
if (import_netlist_instance_gates(module, net_map, inst)) if (import_netlist_instance_gates(inst))
continue; continue;
} }
@ -817,11 +878,10 @@ static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*
} }
} }
} }
};
#endif /* YOSYS_ENABLE_VERIFIC */ #endif /* YOSYS_ENABLE_VERIFIC */
YOSYS_NAMESPACE_BEGIN
struct VerificPass : public Pass { struct VerificPass : public Pass {
VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { } VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
virtual void help() virtual void help()
@ -982,8 +1042,10 @@ struct VerificPass : public Pass {
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) {
import_netlist(design, nl, nl_todo, mode_gates); VerificImporter importer;
importer.import_netlist(design, nl, nl_todo, mode_gates);
}
nl_todo.erase(nl); nl_todo.erase(nl);
nl_done.insert(nl); nl_done.insert(nl);
} }
@ -1001,5 +1063,5 @@ struct VerificPass : public Pass {
#endif #endif
} VerificPass; } VerificPass;
YOSYS_NAMESPACE_END PRIVATE_NAMESPACE_END