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

Merge pull request #2132 from YosysHQ/eddie/verific_initial 

verific: rewrite initial assume/asserts prior to elaboration
This commit is contained in:
clairexen 2020-07-02 17:50:22 +02:00 committed by GitHub
parent e4b9e64d1b 39fa1e160d
commit 3d8d98d709
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 36 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
frontends/verific/verific.cc
View File

@ -48,6 +48,7 @@ USING_YOSYS_NAMESPACE
#include "VeriWrite.h" #include "VeriWrite.h"
#include "VhdlUnits.h" #include "VhdlUnits.h"
#include "VeriLibrary.h" #include "VeriLibrary.h"
#include "VeriExtensions.h"
#ifndef SYMBIOTIC_VERIFIC_API_VERSION #ifndef SYMBIOTIC_VERIFIC_API_VERSION
# error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific." # error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
@ -1445,6 +1446,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue; continue;
} }
if (inst->Type() == PRIM_SEDA_INITSTATE)
{
SigBit initstate = module->Initstate(new_verific_id(inst));
SigBit sig_o = net_map_at(inst->GetOutput());
module->connect(sig_o, initstate);
if (!mode_keep)
continue;
}
if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (!mode_keep && verific_sva_prims.count(inst->Type())) {
if (verific_verbose) if (verific_verbose)
log(" skipping SVA cell in non k-mode\n"); log(" skipping SVA cell in non k-mode\n");
@ -1922,6 +1933,9 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par
for (const auto &i : parameters) for (const auto &i : parameters)
verific_params.Insert(i.first.c_str(), i.second.c_str()); verific_params.Insert(i.first.c_str(), i.second.c_str());
InitialAssertionRewriter rw;
rw.RegisterCallBack();
if (top.empty()) { if (top.empty()) {
netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params); netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
} }
@ -2467,6 +2481,9 @@ struct VerificPass : public Pass {
std::set<std::string> top_mod_names; std::set<std::string> top_mod_names;
InitialAssertionRewriter rw;
rw.RegisterCallBack();
if (mode_all) if (mode_all)
{ {
log("Running hier_tree::ElaborateAll().\n"); log("Running hier_tree::ElaborateAll().\n");
@ -2491,31 +2508,23 @@ struct VerificPass : public Pass {
if (argidx == GetSize(args)) if (argidx == GetSize(args))
cmd_error(args, argidx, "No top module specified.\n"); cmd_error(args, argidx, "No top module specified.\n");
VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
Array veri_modules, vhdl_units; Array veri_modules, vhdl_units;
for (; argidx < GetSize(args); argidx++) for (; argidx < GetSize(args); argidx++)
{ {
const char *name = args[argidx].c_str(); const char *name = args[argidx].c_str();
top_mod_names.insert(name); top_mod_names.insert(name);
VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
if (veri_lib) { VeriModule *veri_module = veri_lib ? veri_lib->GetModule(name, 1) : nullptr;
VeriModule *veri_module = veri_lib->GetModule(name, 1);
if (veri_module) { if (veri_module) {
log("Adding Verilog module '%s' to elaboration queue.\n", name); log("Adding Verilog module '%s' to elaboration queue.\n", name);
veri_modules.InsertLast(veri_module); veri_modules.InsertLast(veri_module);
continue; continue;
} }
// Also elaborate all root modules since they may contain bind statements VhdlDesignUnit *vhdl_unit = vhdl_lib ? vhdl_lib->GetPrimUnit(name) : nullptr;
MapIter mi;
FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
if (!veri_module->IsRootModule()) continue;
veri_modules.InsertLast(veri_module);
}
}
VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
if (vhdl_unit) { if (vhdl_unit) {
log("Adding VHDL unit '%s' to elaboration queue.\n", name); log("Adding VHDL unit '%s' to elaboration queue.\n", name);
vhdl_units.InsertLast(vhdl_unit); vhdl_units.InsertLast(vhdl_unit);
@ -2525,6 +2534,16 @@ struct VerificPass : public Pass {
log_error("Can't find module/unit '%s'.\n", name); log_error("Can't find module/unit '%s'.\n", name);
} }
if (veri_lib) {
// Also elaborate all root modules since they may contain bind statements
MapIter mi;
VeriModule *veri_module;
FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
if (!veri_module->IsRootModule()) continue;
veri_modules.InsertLast(veri_module);
}
}
log("Running hier_tree::Elaborate().\n"); log("Running hier_tree::Elaborate().\n");
Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters); Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
Netlist *nl; Netlist *nl;