Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve verific -chparam and add hierarchy -chparam #871

Merged
merged 7 commits into from
May 6, 2019
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
95 changes: 70 additions & 25 deletions frontends/verific/verific.cc
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ USING_YOSYS_NAMESPACE
#include "VeriModule.h"
#include "VeriWrite.h"
#include "VhdlUnits.h"
#include "Message.h"
#include "VeriLibrary.h"

#ifdef __clang__
#pragma clang diagnostic pop
Expand Down Expand Up @@ -776,13 +776,14 @@ void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)

void VerificImporter::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 netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
std::string module_name = nl->IsOperator() ? "$verific$" + netlist_name : RTLIL::escape_id(netlist_name);

netlist = nl;

if (design->has(module_name)) {
if (!nl->IsOperator() && !is_blackbox(nl))
log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
log_cmd_error("Re-definition of module `%s'.\n", netlist_name.c_str());
return;
}

Expand Down Expand Up @@ -1752,32 +1753,64 @@ struct VerificExtNets
}
};

void verific_import(Design *design, std::string top)
void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
{
verific_sva_fsm_limit = 16;

std::set<Netlist*> nl_todo, nl_done;

{
VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
Array *netlists = NULL;
Array veri_libs, vhdl_libs;
if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
if (veri_lib) veri_libs.InsertLast(veri_lib);

Array veri_libs, vhdl_libs;
if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
if (veri_lib) veri_libs.InsertLast(veri_lib);
Map verific_params(STRING_HASH);
for (const auto &i : parameters)
verific_params.Insert(i.first.c_str(), i.second.c_str());

Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
Netlist *nl;
int i;
if (top.empty()) {
netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
}
else {
Array veri_modules, vhdl_units;

FOREACH_ARRAY_ITEM(netlists, i, nl) {
if (top.empty() || nl->Owner()->Name() == top)
nl_todo.insert(nl);
if (veri_lib) {
VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
if (veri_module) {
veri_modules.InsertLast(veri_module);
}

// Also elaborate all root modules since they may contain bind statements
MapIter mi;
FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
if (!veri_module->IsRootModule()) continue;
veri_modules.InsertLast(veri_module);
}
}

delete netlists;
if (vhdl_lib) {
VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
if (vhdl_unit)
vhdl_units.InsertLast(vhdl_unit);
}

netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
}

Netlist *nl;
int i;

FOREACH_ARRAY_ITEM(netlists, i, nl) {
if (top.empty() && nl->CellBaseName() != top)
continue;
nl->AddAtt(new Att(" \\top", NULL));
nl_todo.insert(nl);
}

delete netlists;

if (!verific_error_msg.empty())
log_error("%s\n", verific_error_msg.c_str());

Expand Down Expand Up @@ -2212,8 +2245,8 @@ struct VerificPass : public Pass {
continue;
}
if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
const std::string &key = args[++argidx];
const std::string &value = args[++argidx];
const std::string &key = args[++argidx];
const std::string &value = args[++argidx];
unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
1 /* force_overwrite */);
if (!new_insertion)
Expand Down Expand Up @@ -2270,12 +2303,22 @@ struct VerificPass : public Pass {
for (; argidx < GetSize(args); argidx++)
{
const char *name = args[argidx].c_str();
VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);

if (veri_lib) {
VeriModule *veri_module = veri_lib->GetModule(name, 1);
if (veri_module) {
log("Adding Verilog module '%s' to elaboration queue.\n", name);
veri_modules.InsertLast(veri_module);
continue;
}

VeriModule *veri_module = veri_file::GetModule(name);
if (veri_module) {
log("Adding Verilog module '%s' to elaboration queue.\n", name);
veri_modules.InsertLast(veri_module);
continue;
// Also elaborate all root modules since they may contain bind statements
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);
Expand All @@ -2294,8 +2337,10 @@ struct VerificPass : public Pass {
Netlist *nl;
int i;

FOREACH_ARRAY_ITEM(netlists, i, nl)
FOREACH_ARRAY_ITEM(netlists, i, nl) {
nl->AddAtt(new Att(" \\top", NULL));
nl_todo.insert(nl);
}
delete netlists;
}

Expand Down
2 changes: 1 addition & 1 deletion frontends/verific/verific.h
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ YOSYS_NAMESPACE_BEGIN
extern int verific_verbose;

extern bool verific_import_pending;
extern void verific_import(Design *design, std::string top = std::string());
extern void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top = std::string());

extern pool<int> verific_sva_prims;

Expand Down
76 changes: 58 additions & 18 deletions passes/hierarchy/hierarchy.cc
Original file line number Diff line number Diff line change
Expand Up @@ -570,7 +570,7 @@ struct HierarchyPass : public Pass {
log("\n");
log(" -simcheck\n");
log(" like -check, but also throw an error if blackbox modules are\n");
log(" instantiated, and throw an error if the design has no top module\n");
log(" instantiated, and throw an error if the design has no top module.\n");
log("\n");
log(" -purge_lib\n");
log(" by default the hierarchy command will not remove library (blackbox)\n");
Expand All @@ -583,20 +583,20 @@ struct HierarchyPass : public Pass {
log("\n");
log(" -keep_positionals\n");
log(" per default this pass also converts positional arguments in cells\n");
log(" to arguments using port names. this option disables this behavior.\n");
log(" to arguments using port names. This option disables this behavior.\n");
log("\n");
log(" -keep_portwidths\n");
log(" per default this pass adjusts the port width on cells that are\n");
log(" module instances when the width does not match the module port. this\n");
log(" module instances when the width does not match the module port. This\n");
log(" option disables this behavior.\n");
log("\n");
log(" -nokeep_asserts\n");
log(" per default this pass sets the \"keep\" attribute on all modules\n");
log(" that directly or indirectly contain one or more $assert cells. this\n");
log(" option disables this behavior.\n");
log(" that directly or indirectly contain one or more formal properties.\n");
log(" This option disables this behavior.\n");
log("\n");
log(" -top <module>\n");
log(" use the specified top module to built a design hierarchy. modules\n");
log(" use the specified top module to build the design hierarchy. Modules\n");
log(" outside this tree (unused modules) are removed.\n");
log("\n");
log(" when the -top option is used, the 'top' attribute will be set on the\n");
Expand All @@ -606,6 +606,12 @@ struct HierarchyPass : public Pass {
log(" -auto-top\n");
log(" automatically determine the top of the design hierarchy and mark it.\n");
log("\n");
log(" -chparam name value \n");
log(" elaborate the top module using this parameter value. Modules on which\n");
log(" this parameter does not exist may cause a warning message to be output.\n");
log(" This option can be specified multiple times to override multiple\n");
log(" parameters. String values must be passed in double quotes (\").\n");
log("\n");
log("In -generate mode this pass generates blackbox modules for the given cell\n");
log("types (wildcards supported). For this the design is searched for cells that\n");
log("match the given types and then the given port declarations are used to\n");
Expand Down Expand Up @@ -641,6 +647,7 @@ struct HierarchyPass : public Pass {
bool nokeep_asserts = false;
std::vector<std::string> generate_cells;
std::vector<generate_port_decl_t> generate_ports;
std::map<std::string, std::string> parameters;

size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
Expand Down Expand Up @@ -715,28 +722,61 @@ struct HierarchyPass : public Pass {
if (args[argidx] == "-top") {
if (++argidx >= args.size())
log_cmd_error("Option -top requires an additional argument!\n");
top_mod = design->modules_.count(RTLIL::escape_id(args[argidx])) ? design->modules_.at(RTLIL::escape_id(args[argidx])) : NULL;
if (top_mod == NULL && design->modules_.count("$abstract" + RTLIL::escape_id(args[argidx]))) {
dict<RTLIL::IdString, RTLIL::Const> empty_parameters;
design->modules_.at("$abstract" + RTLIL::escape_id(args[argidx]))->derive(design, empty_parameters);
top_mod = design->modules_.count(RTLIL::escape_id(args[argidx])) ? design->modules_.at(RTLIL::escape_id(args[argidx])) : NULL;
}
if (top_mod == NULL)
load_top_mod = args[argidx];
load_top_mod = args[argidx];
continue;
}
if (args[argidx] == "-auto-top") {
auto_top_mode = true;
continue;
}
if (args[argidx] == "-chparam" && argidx+2 < args.size()) {
const std::string &key = args[++argidx];
const std::string &value = args[++argidx];
auto r = parameters.emplace(key, value);
if (!r.second) {
log_warning("-chparam %s already specified: overwriting.\n", key.c_str());
r.first->second = value;
}
continue;
}
break;
}
extra_args(args, argidx, design, false);

if (!load_top_mod.empty()) {
if (!load_top_mod.empty())
{
IdString top_name = RTLIL::escape_id(load_top_mod);
IdString abstract_id = "$abstract" + RTLIL::escape_id(load_top_mod);
top_mod = design->module(top_name);

dict<RTLIL::IdString, RTLIL::Const> top_parameters;
for (auto &para : parameters) {
SigSpec sig_value;
if (!RTLIL::SigSpec::parse(sig_value, NULL, para.second))
log_cmd_error("Can't decode value '%s'!\n", para.second.c_str());
top_parameters[RTLIL::escape_id(para.first)] = sig_value.as_const();
}

if (top_mod == nullptr && design->module(abstract_id))
top_mod = design->module(design->module(abstract_id)->derive(design, top_parameters));
else if (top_mod != nullptr && !top_parameters.empty())
top_mod = design->module(top_mod->derive(design, top_parameters));

if (top_mod != nullptr && top_mod->name != top_name) {
Module *m = top_mod->clone();
m->name = top_name;
Module *old_mod = design->module(top_name);
if (old_mod)
design->remove(old_mod);
design->add(m);
top_mod = m;
}
}

if (top_mod == nullptr && !load_top_mod.empty()) {
#ifdef YOSYS_ENABLE_VERIFIC
if (verific_import_pending) {
verific_import(design, load_top_mod);
verific_import(design, parameters, load_top_mod);
top_mod = design->module(RTLIL::escape_id(load_top_mod));
}
#endif
Expand All @@ -745,7 +785,7 @@ struct HierarchyPass : public Pass {
} else {
#ifdef YOSYS_ENABLE_VERIFIC
if (verific_import_pending)
verific_import(design);
verific_import(design, parameters);
#endif
}

Expand Down Expand Up @@ -846,7 +886,7 @@ struct HierarchyPass : public Pass {
std::map<RTLIL::Module*, bool> cache;
for (auto mod : design->modules())
if (set_keep_assert(cache, mod)) {
log("Module %s directly or indirectly contains $assert cells -> setting \"keep\" attribute.\n", log_id(mod));
log("Module %s directly or indirectly contains formal properties -> setting \"keep\" attribute.\n", log_id(mod));
mod->set_bool_attribute("\\keep");
}
}
Expand Down
52 changes: 52 additions & 0 deletions tests/various/chparam.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
#!/bin/bash

trap 'echo "ERROR in chparam.sh" >&2; exit 1' ERR

cat > chparam1.sv << "EOT"
module top #(
parameter [31:0] X = 0
) (
input [31:0] din,
output [31:0] dout
);
assign dout = X-din;
endmodule

module top_props #(
parameter [31:0] X = 0
) (
input [31:0] dout
);
always @* assert (dout != X);
endmodule

bind top top_props #(.X(123456789)) props (.*);
EOT

cat > chparam2.sv << "EOT"
module top #(
parameter [31:0] X = 0
) (
input [31:0] din,
output [31:0] dout
);
assign dout = X-din;
always @* assert (dout != 123456789);
endmodule
EOT

if ../../yosys -q -p 'verific -sv chparam1.sv'; then
../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'

../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
fi
../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'

rm chparam1.sv
rm chparam2.sv