mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-11 13:40:53 +00:00
Code Activity

Merge remote-tracking branch 'origin/master' into eddie/verific_help

Browse source
This commit is contained in:
Eddie Hung 2020-01-27 10:34:10 -08:00
commit f443695a38
208 changed files with 10136 additions and 4961 deletions
Download patch file Download diff file Expand all files Collapse all files

8
frontends/verific/README
View file

@ -1,7 +1,11 @@
This directory contains Verific bindings for Yosys.
See http://www.verific.com/ for details.
Use Symbiotic EDA Suite if you need Yosys+Verifc.
https://www.symbioticeda.com/seda-suite
Contact office@symbioticeda.com for free evaluation
binaries of Symbiotic EDA Suite.
Verific Features that should be enabled in your Verific library

40
frontends/verific/verific.cc
View file

@ -130,7 +130,7 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net)
bool is_blackbox(Netlist *nl)
{
if (nl->IsBlackBox())
if (nl->IsBlackBox() || nl->IsEmptyBox())
return true;
const char *attr = nl->GetAttValue("blackbox");
@ -784,15 +784,15 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
merge_past_ffs_clock(it.second, it.first.first, it.first.second);
}
void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename)
{
std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
std::string module_name = netlist_name;
if (nl->IsOperator()) {
if (nl->IsOperator() || nl->IsPrimitive()) {
module_name = "$verific$" + module_name;
} else {
if (*nl->Name()) {
if (!norename && *nl->Name()) {
module_name += "(";
module_name += nl->Name();
module_name += ")";
@ -1409,7 +1409,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
std::string inst_type = inst->View()->Owner()->Name();
if (inst->View()->IsOperator()) {
if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) {
inst_type = "$verific$" + inst_type;
} else {
if (*inst->View()->Name()) {
@ -1899,7 +1899,7 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) {
VerificImporter importer(false, false, false, false, false, false, false);
importer.import_netlist(design, nl, nl_todo);
importer.import_netlist(design, nl, nl_todo, nl->Owner()->Name() == top);
}
nl_todo.erase(nl);
nl_done.insert(nl);
@ -2065,7 +2065,12 @@ struct VerificPass : public Pass {
log(" -d <dump_file>\n");
log(" Dump the Verific netlist as a verilog file.\n");
log("\n");
log("Visit http://verific.com/ for more information on Verific.\n");
log("\n");
log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
log("https://www.symbioticeda.com/seda-suite\n");
log("\n");
log("Contact office@symbioticeda.com for free evaluation\n");
log("binaries of Symbiotic EDA Suite.\n");
log("\n");
}
#ifdef YOSYS_ENABLE_VERIFIC
@ -2074,7 +2079,13 @@ struct VerificPass : public Pass {
static bool set_verific_global_flags = true;
if (check_noverific_env())
log_cmd_error("This version of Yosys is built without Verific support.\n");
log_cmd_error("This version of Yosys is built without Verific support.\n"
"\n"
"Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
"https://www.symbioticeda.com/seda-suite\n"
"\n"
"Contact office@symbioticeda.com for free evaluation\n"
"binaries of Symbiotic EDA Suite.\n");
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
@ -2373,6 +2384,8 @@ struct VerificPass : public Pass {
if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
cmd_error(args, argidx, "unknown option");
std::set<std::string> top_mod_names;
if (mode_all)
{
log("Running hier_tree::ElaborateAll().\n");
@ -2401,6 +2414,7 @@ struct VerificPass : public Pass {
for (; argidx < GetSize(args); argidx++)
{
const char *name = args[argidx].c_str();
top_mod_names.insert(name);
VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
if (veri_lib) {
@ -2466,7 +2480,7 @@ struct VerificPass : public Pass {
if (nl_done.count(nl) == 0) {
VerificImporter importer(mode_gates, mode_keep, mode_nosva,
mode_names, mode_verific, mode_autocover, mode_fullinit);
importer.import_netlist(design, nl, nl_todo);
importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->Owner()->Name()));
}
nl_todo.erase(nl);
nl_done.insert(nl);
@ -2490,7 +2504,13 @@ struct VerificPass : public Pass {
}
#else /* YOSYS_ENABLE_VERIFIC */
void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
log_cmd_error("This version of Yosys is built without Verific support.\n");
log_cmd_error("This version of Yosys is built without Verific support.\n"
"\n"
"Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
"https://www.symbioticeda.com/seda-suite\n"
"\n"
"Contact office@symbioticeda.com for free evaluation\n"
"binaries of Symbiotic EDA Suite.\n");
}
#endif
} VerificPass;

2
frontends/verific/verific.h
View file

@ -93,7 +93,7 @@ struct VerificImporter
void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol);
void merge_past_ffs(pool<RTLIL::Cell*> &candidates);
void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo);
void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo, bool norename = false);
};
void verific_import_sva_assert(VerificImporter *importer, Verific::Instance *inst);

42
frontends/verific/verificsva.cc
View file

@ -36,6 +36,8 @@
// basic_property:
// sequence
// not basic_property
// nexttime basic_property
// nexttime[N] basic_property
// sequence #-# basic_property
// sequence #=# basic_property
// basic_property or basic_property (cover only)
@ -1264,6 +1266,26 @@ struct VerificSvaImporter
return node;
}
if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME)
{
const char *sva_low_s = inst->GetAttValue("sva:low");
const char *sva_high_s = inst->GetAttValue("sva:high");
int sva_low = atoi(sva_low_s);
int sva_high = atoi(sva_high_s);
log_assert(sva_low == sva_high);
int node = start_node;
for (int i = 0; i < sva_low; i++) {
int next_node = fsm.createNode();
fsm.createEdge(node, next_node);
node = next_node;
}
return parse_sequence(fsm, node, inst->GetInput());
}
if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
{
const char *sva_low_s = inst->GetAttValue("sva:low");
@ -1590,15 +1612,25 @@ struct VerificSvaImporter
Instance *consequent_inst = net_to_ast_driver(consequent_net);
if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH ||
consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS))
{
bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
Net *until_net = consequent_inst->GetInput2();
consequent_net = consequent_inst->GetInput1();
consequent_inst = net_to_ast_driver(consequent_net);
Net *until_net = nullptr;
if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)
{
consequent_net = consequent_inst->GetInput();
consequent_inst = net_to_ast_driver(consequent_net);
}
else
{
until_net = consequent_inst->GetInput2();
consequent_net = consequent_inst->GetInput1();
consequent_inst = net_to_ast_driver(consequent_net);
}
SigBit until_sig = parse_expression(until_net);
SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0;
SigBit not_until_sig = module->Not(NEW_ID, until_sig);
antecedent_fsm.createEdge(node, node, not_until_sig);