mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 09:05:32 +00:00
Merge branch 'YosysHQ:master' into main/issue2525
This commit is contained in:
commit
693c609eec
18 changed files with 2505 additions and 57 deletions
|
@ -41,50 +41,70 @@ std::map<std::string, std::string> loaded_plugin_aliases;
|
|||
void load_plugin(std::string filename, std::vector<std::string> aliases)
|
||||
{
|
||||
std::string orig_filename = filename;
|
||||
rewrite_filename(filename);
|
||||
|
||||
if (filename.find('/') == std::string::npos)
|
||||
// Would something like this better be put in `rewrite_filename`?
|
||||
if (filename.find("/") == std::string::npos)
|
||||
filename = "./" + filename;
|
||||
|
||||
|
||||
#ifdef WITH_PYTHON
|
||||
if (!loaded_plugins.count(filename) && !loaded_python_plugins.count(filename)) {
|
||||
const bool is_loaded = loaded_plugins.count(orig_filename) && loaded_python_plugins.count(orig_filename);
|
||||
#else
|
||||
if (!loaded_plugins.count(filename)) {
|
||||
const bool is_loaded = loaded_plugins.count(orig_filename);
|
||||
#endif
|
||||
|
||||
#ifdef WITH_PYTHON
|
||||
|
||||
boost::filesystem::path full_path(filename);
|
||||
|
||||
if(strcmp(full_path.extension().c_str(), ".py") == 0)
|
||||
if (!is_loaded) {
|
||||
// Check if we're loading a python script
|
||||
if(filename.find(".py") != std::string::npos)
|
||||
{
|
||||
std::string path(full_path.parent_path().c_str());
|
||||
filename = full_path.filename().c_str();
|
||||
filename = filename.substr(0,filename.size()-3);
|
||||
PyRun_SimpleString(("sys.path.insert(0,\""+path+"\")").c_str());
|
||||
PyErr_Print();
|
||||
PyObject *module_p = PyImport_ImportModule(filename.c_str());
|
||||
if(module_p == NULL)
|
||||
{
|
||||
#ifdef WITH_PYTHON
|
||||
boost::filesystem::path full_path(filename);
|
||||
std::string path(full_path.parent_path().c_str());
|
||||
filename = full_path.filename().c_str();
|
||||
filename = filename.substr(0,filename.size()-3);
|
||||
PyRun_SimpleString(("sys.path.insert(0,\""+path+"\")").c_str());
|
||||
PyErr_Print();
|
||||
log_cmd_error("Can't load python module `%s'\n", full_path.filename().c_str());
|
||||
return;
|
||||
}
|
||||
loaded_python_plugins[orig_filename] = module_p;
|
||||
Pass::init_register();
|
||||
PyObject *module_p = PyImport_ImportModule(filename.c_str());
|
||||
if(module_p == NULL)
|
||||
{
|
||||
PyErr_Print();
|
||||
log_cmd_error("Can't load python module `%s'\n", full_path.filename().c_str());
|
||||
return;
|
||||
}
|
||||
loaded_python_plugins[orig_filename] = module_p;
|
||||
Pass::init_register();
|
||||
#else
|
||||
log_error(
|
||||
"\n This version of Yosys cannot load python plugins.\n"
|
||||
" Ensure Yosys is built with Python support to do so.\n"
|
||||
);
|
||||
#endif
|
||||
} else {
|
||||
#endif
|
||||
// Otherwise we assume it's a native plugin
|
||||
|
||||
void *hdl = dlopen(filename.c_str(), RTLD_LAZY|RTLD_LOCAL);
|
||||
if (hdl == NULL && orig_filename.find('/') == std::string::npos)
|
||||
hdl = dlopen((proc_share_dirname() + "plugins/" + orig_filename + ".so").c_str(), RTLD_LAZY|RTLD_LOCAL);
|
||||
if (hdl == NULL)
|
||||
log_cmd_error("Can't load module `%s': %s\n", filename.c_str(), dlerror());
|
||||
loaded_plugins[orig_filename] = hdl;
|
||||
Pass::init_register();
|
||||
void *hdl = dlopen(filename.c_str(), RTLD_LAZY|RTLD_LOCAL);
|
||||
|
||||
// We were unable to open the file, try to do so from the plugin directory
|
||||
if (hdl == NULL && orig_filename.find('/') == std::string::npos) {
|
||||
hdl = dlopen([orig_filename]() {
|
||||
std::string new_path = proc_share_dirname() + "plugins/" + orig_filename;
|
||||
|
||||
// Check if we need to append .so
|
||||
if (new_path.find(".so") == std::string::npos)
|
||||
new_path.append(".so");
|
||||
|
||||
return new_path;
|
||||
}().c_str(), RTLD_LAZY|RTLD_LOCAL);
|
||||
}
|
||||
|
||||
if (hdl == NULL)
|
||||
log_cmd_error("Can't load module `%s': %s\n", filename.c_str(), dlerror());
|
||||
|
||||
loaded_plugins[orig_filename] = hdl;
|
||||
Pass::init_register();
|
||||
|
||||
#ifdef WITH_PYTHON
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
for (auto &alias : aliases)
|
||||
|
@ -182,4 +202,3 @@ struct PluginPass : public Pass {
|
|||
} PluginPass;
|
||||
|
||||
YOSYS_NAMESPACE_END
|
||||
|
||||
|
|
|
@ -116,6 +116,8 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
|
|||
}
|
||||
cache.emplace(module, -1);
|
||||
|
||||
std::vector<std::pair<Cell *, IdString>> renames;
|
||||
|
||||
bool has_witness_signals = false;
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
|
@ -130,8 +132,9 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
|
|||
c = '_';
|
||||
auto new_id = module->uniquify("\\_witness_." + name);
|
||||
cell->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
|
||||
module->rename(cell, new_id);
|
||||
renames.emplace_back(cell, new_id);
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) {
|
||||
|
@ -155,6 +158,9 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
|
|||
}
|
||||
}
|
||||
}
|
||||
for (auto rename : renames) {
|
||||
module->rename(rename.first, rename.second);
|
||||
}
|
||||
|
||||
cache[module] = has_witness_signals;
|
||||
return has_witness_signals;
|
||||
|
|
|
@ -19,3 +19,4 @@ OBJS += passes/sat/fminit.o
|
|||
ifeq ($(DISABLE_SPAWN),0)
|
||||
OBJS += passes/sat/qbfsat.o
|
||||
endif
|
||||
OBJS += passes/sat/synthprop.o
|
||||
|
|
|
@ -1162,6 +1162,11 @@ struct SimWorker : SimShared
|
|||
}
|
||||
for(auto& writer : outputfiles)
|
||||
writer->write(use_signal);
|
||||
|
||||
if (writeback) {
|
||||
pool<Module*> wbmods;
|
||||
top->writeback(wbmods);
|
||||
}
|
||||
}
|
||||
|
||||
void update(bool gclk)
|
||||
|
@ -1265,11 +1270,6 @@ struct SimWorker : SimShared
|
|||
register_output_step(10*numcycles + 2);
|
||||
|
||||
write_output_files();
|
||||
|
||||
if (writeback) {
|
||||
pool<Module*> wbmods;
|
||||
top->writeback(wbmods);
|
||||
}
|
||||
}
|
||||
|
||||
void run_cosim_fst(Module *topmod, int numcycles)
|
||||
|
@ -1394,11 +1394,6 @@ struct SimWorker : SimShared
|
|||
}
|
||||
|
||||
write_output_files();
|
||||
|
||||
if (writeback) {
|
||||
pool<Module*> wbmods;
|
||||
top->writeback(wbmods);
|
||||
}
|
||||
delete fst;
|
||||
}
|
||||
|
||||
|
|
269
passes/sat/synthprop.cc
Normal file
269
passes/sat/synthprop.cc
Normal file
|
@ -0,0 +1,269 @@
|
|||
/*
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Copyright (C) 2023 Miodrag Milanovic <micko@yosyshq.com>
|
||||
* Copyright (C) 2023
|
||||
* National Technology & Engineering Solutions of Sandia, LLC (NTESS)
|
||||
*
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
*
|
||||
*/
|
||||
#include "kernel/yosys.h"
|
||||
|
||||
YOSYS_NAMESPACE_BEGIN
|
||||
|
||||
struct TrackingItem
|
||||
{
|
||||
pool<Cell*> assertion_cells;
|
||||
std::vector<std::string> names;
|
||||
};
|
||||
|
||||
typedef dict<RTLIL::Module*, TrackingItem> TrackingData;
|
||||
|
||||
struct SynthPropWorker
|
||||
{
|
||||
// pointer to main design
|
||||
RTLIL::Design *design;
|
||||
|
||||
RTLIL::IdString top_name;
|
||||
|
||||
RTLIL::Module *module;
|
||||
|
||||
std::string map_file;
|
||||
|
||||
bool or_outputs;
|
||||
|
||||
IdString port_name;
|
||||
|
||||
IdString reset_name;
|
||||
|
||||
bool reset_pol;
|
||||
|
||||
// basic contrcutor
|
||||
SynthPropWorker(RTLIL::Design *design) : design(design), or_outputs(false), port_name(RTLIL::escape_id("assertions")) {}
|
||||
|
||||
void tracing(RTLIL::Module *mod, int depth, TrackingData &tracing_data, std::string hier_path);
|
||||
void run();
|
||||
};
|
||||
|
||||
void SynthPropWorker::tracing(RTLIL::Module *mod, int depth, TrackingData &tracing_data, std::string hier_path)
|
||||
{
|
||||
log("%*sTracing in module %s..\n", 2*depth, "", log_id(mod));
|
||||
tracing_data[mod] = TrackingItem();
|
||||
int cnt = 0;
|
||||
for (auto cell : mod->cells()) {
|
||||
if (cell->type == ID($assert)) {
|
||||
log("%*sFound assert %s..\n", 2*(depth+1), "", log_id(cell));
|
||||
tracing_data[mod].assertion_cells.emplace(cell);
|
||||
if (!or_outputs) {
|
||||
tracing_data[mod].names.push_back(hier_path + "." + log_id(cell));
|
||||
}
|
||||
cnt++;
|
||||
}
|
||||
else if (RTLIL::Module *submod = design->module(cell->type)) {
|
||||
tracing(submod, depth+1, tracing_data, hier_path + "." + log_id(cell));
|
||||
if (!or_outputs) {
|
||||
for (size_t i = 0; i < tracing_data[submod].names.size(); i++)
|
||||
tracing_data[mod].names.push_back(tracing_data[submod].names[i]);
|
||||
} else {
|
||||
cnt += tracing_data[submod].names.size();
|
||||
}
|
||||
}
|
||||
}
|
||||
if (or_outputs && (cnt > 0)) {
|
||||
tracing_data[mod].names.push_back("merged_asserts");
|
||||
}
|
||||
}
|
||||
|
||||
void SynthPropWorker::run()
|
||||
{
|
||||
if (!module->get_bool_attribute(ID::top))
|
||||
log_error("Module is not TOP module\n");
|
||||
|
||||
TrackingData tracing_data;
|
||||
tracing(module, 0, tracing_data, log_id(module->name));
|
||||
|
||||
for (auto &data : tracing_data) {
|
||||
if (data.second.names.size() == 0) continue;
|
||||
RTLIL::Wire *wire = data.first->addWire(port_name, data.second.names.size());
|
||||
wire->port_output = true;
|
||||
data.first->fixup_ports();
|
||||
}
|
||||
|
||||
RTLIL::Wire *output = nullptr;
|
||||
for (auto &data : tracing_data) {
|
||||
int num = 0;
|
||||
RTLIL::Wire *port_wire = data.first->wire(port_name);
|
||||
if (!reset_name.empty() && data.first == module) {
|
||||
port_wire = data.first->addWire(NEW_ID, data.second.names.size());
|
||||
output = port_wire;
|
||||
}
|
||||
pool<Wire*> connected;
|
||||
for (auto cell : data.second.assertion_cells) {
|
||||
if (cell->type == ID($assert)) {
|
||||
RTLIL::Wire *neg_wire = data.first->addWire(NEW_ID);
|
||||
RTLIL::Wire *result_wire = data.first->addWire(NEW_ID);
|
||||
data.first->addNot(NEW_ID, cell->getPort(ID::A), neg_wire);
|
||||
data.first->addAnd(NEW_ID, cell->getPort(ID::EN), neg_wire, result_wire);
|
||||
if (!or_outputs) {
|
||||
data.first->connect(SigBit(port_wire,num), result_wire);
|
||||
} else {
|
||||
connected.emplace(result_wire);
|
||||
}
|
||||
num++;
|
||||
}
|
||||
}
|
||||
|
||||
for (auto cell : data.first->cells()) {
|
||||
if (RTLIL::Module *submod = design->module(cell->type)) {
|
||||
if (tracing_data[submod].names.size() > 0) {
|
||||
if (!or_outputs) {
|
||||
cell->setPort(port_name, SigChunk(port_wire, num, tracing_data[submod].names.size()));
|
||||
} else {
|
||||
RTLIL::Wire *result_wire = data.first->addWire(NEW_ID);
|
||||
cell->setPort(port_name, result_wire);
|
||||
connected.emplace(result_wire);
|
||||
}
|
||||
num += tracing_data[submod].names.size();
|
||||
}
|
||||
}
|
||||
}
|
||||
if (or_outputs && connected.size() > 0) {
|
||||
RTLIL::Wire *prev_wire = nullptr;
|
||||
for (auto wire : connected ) {
|
||||
if (!prev_wire) {
|
||||
prev_wire = wire;
|
||||
} else {
|
||||
RTLIL::Wire *result = data.first->addWire(NEW_ID);
|
||||
data.first->addOr(NEW_ID, prev_wire, wire, result);
|
||||
prev_wire = result;
|
||||
}
|
||||
}
|
||||
data.first->connect(port_wire, prev_wire);
|
||||
}
|
||||
}
|
||||
|
||||
// If no assertions found
|
||||
if (tracing_data[module].names.size() == 0) return;
|
||||
|
||||
if (!reset_name.empty()) {
|
||||
int width = tracing_data[module].names.size();
|
||||
SigSpec reset = module->wire(reset_name);
|
||||
reset.extend_u0(width, true);
|
||||
|
||||
module->addDlatchsr(NEW_ID, State::S1, Const(State::S0,width), reset, output, module->wire(port_name), true, true, reset_pol);
|
||||
}
|
||||
|
||||
if (!map_file.empty()) {
|
||||
std::ofstream fout;
|
||||
fout.open(map_file, std::ios::out | std::ios::trunc);
|
||||
if (!fout.is_open())
|
||||
log_error("Could not open file \"%s\" with write access.\n", map_file.c_str());
|
||||
|
||||
for (auto name : tracing_data[module].names) {
|
||||
fout << name << std::endl;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
struct SyntProperties : public Pass {
|
||||
SyntProperties() : Pass("synthprop", "synthesize SVA properties") { }
|
||||
|
||||
virtual void help()
|
||||
{
|
||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||
log("\n");
|
||||
log(" synthprop [options]\n");
|
||||
log("\n");
|
||||
log("This creates synthesizable properties for selected module.\n");
|
||||
log("\n");
|
||||
log("\n");
|
||||
log(" -name <portname>\n");
|
||||
log("\n");
|
||||
log("Name output port for assertions (default: assertions).\n");
|
||||
log("\n");
|
||||
log("\n");
|
||||
log(" -map <filename>\n");
|
||||
log("\n");
|
||||
log("Write port mapping for synthesizable properties.\n");
|
||||
log("\n");
|
||||
log("\n");
|
||||
log(" -or_outputs\n");
|
||||
log("\n");
|
||||
log("Or all outputs together to create a single output that goes high when any\n");
|
||||
log("property is violated, instead of generating individual output bits.\n");
|
||||
log("\n");
|
||||
log("\n");
|
||||
log(" -reset <portname>\n");
|
||||
log("\n");
|
||||
log("Name of top-level reset input. Latch a high state on the generated outputs\n");
|
||||
log("until an asynchronous top-level reset input is activated.\n");
|
||||
log("\n");
|
||||
log("\n");
|
||||
log(" -resetn <portname>\n");
|
||||
log("\n");
|
||||
log("Name of top-level reset input (inverse polarity). Latch a high state on the\n");
|
||||
log("generated outputs until an asynchronous top-level reset input is activated.\n");
|
||||
log("\n");
|
||||
log("\n");
|
||||
}
|
||||
|
||||
virtual void execute(std::vector<std::string> args, RTLIL::Design* design)
|
||||
{
|
||||
log_header(design, "Executing SYNTHPROP pass.\n");
|
||||
SynthPropWorker worker(design);
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++)
|
||||
{
|
||||
if (args[argidx] == "-name" && argidx+1 < args.size()) {
|
||||
worker.port_name = RTLIL::escape_id(args[++argidx]);
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-map" && argidx+1 < args.size()) {
|
||||
worker.map_file = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-reset" && argidx+1 < args.size()) {
|
||||
worker.reset_name = RTLIL::escape_id(args[++argidx]);
|
||||
worker.reset_pol = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-resetn" && argidx+1 < args.size()) {
|
||||
worker.reset_name = RTLIL::escape_id(args[++argidx]);
|
||||
worker.reset_pol = false;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-or_outputs") {
|
||||
worker.or_outputs = true;
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
||||
if (args.size() != argidx)
|
||||
cmd_error(args, argidx, "Extra argument.");
|
||||
|
||||
auto *top = design->top_module();
|
||||
if (top == nullptr)
|
||||
log_cmd_error("Can't find top module in current design!\n");
|
||||
|
||||
auto *reset = top->wire(worker.reset_name);
|
||||
if (!worker.reset_name.empty() && reset == nullptr)
|
||||
log_cmd_error("Can't find reset line in current design!\n");
|
||||
|
||||
worker.module = top;
|
||||
worker.run();
|
||||
}
|
||||
} SyntProperties;
|
||||
|
||||
YOSYS_NAMESPACE_END
|
|
@ -236,10 +236,10 @@ LibertyAst *LibertyParser::parse()
|
|||
|
||||
if (tok == ':' && ast->value.empty()) {
|
||||
tok = lexer(ast->value);
|
||||
if (tok != 'v')
|
||||
error();
|
||||
tok = lexer(str);
|
||||
while (tok == '+' || tok == '-' || tok == '*' || tok == '/') {
|
||||
if (tok == 'v') {
|
||||
tok = lexer(str);
|
||||
}
|
||||
while (tok == '+' || tok == '-' || tok == '*' || tok == '/' || tok == '!') {
|
||||
ast->value += tok;
|
||||
tok = lexer(str);
|
||||
if (tok != 'v')
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue