mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 11:42:30 +00:00
Code Activity

Merge pull request #3226 from YosysHQ/micko/btor2witness

Browse source 
Sim support for btor2 witness files
This commit is contained in:
Miodrag Milanović 2022-03-11 15:29:34 +01:00 • committed by GitHub
commit 2f44683f4f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 171 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

4
backends/btor/btor.cc
View file

@ -678,7 +678,7 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
btorf("%d state %d\n", nid, sid);
btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
if (cell->type == ID($anyconst)) {
int nid2 = next_nid++;
@ -699,7 +699,7 @@ struct BtorWorker
int one_nid = get_sig_nid(State::S1);
int zero_nid = get_sig_nid(State::S0);
initstate_nid = next_nid++;
btorf("%d state %d\n", initstate_nid, sid);
btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
}

175
passes/sat/sim.cc
View file

@ -326,6 +326,16 @@ struct SimInstance
return did_something;
}
void set_memory_state(IdString memid, Const addr, Const data)
{
auto &state = mem_database[memid];
int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
for (int i = 0; i < GetSize(data); i++)
if (0 <= i+offset && i+offset < GetSize(data))
state.data.bits[i+offset] = data.bits[i];
}
void update_cell(Cell *cell)
{
if (ff_database.count(cell))
@ -961,7 +971,7 @@ struct SimWorker : SimShared
}
}
void run_cosim(Module *topmod, int numcycles)
void run_cosim_fst(Module *topmod, int numcycles)
{
log_assert(top == nullptr);
fst = new FstData(sim_filename);
@ -1092,13 +1102,17 @@ struct SimWorker : SimShared
delete fst;
}
void run_cosim_witness(Module *topmod)
void run_cosim_aiger_witness(Module *topmod)
{
log_assert(top == nullptr);
if ((clock.size()+clockn.size())==0)
log_error("Clock signal must be specified.\n");
std::ifstream mf(map_filename);
std::string type, symbol;
int variable, index;
dict<int, std::pair<SigBit,bool>> inputs, inits, latches;
if (mf.fail())
log_cmd_error("Not able to read AIGER witness map file.\n");
while (mf >> type >> variable >> index >> symbol) {
RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
Wire *w = topmod->wire(escaped_s);
@ -1183,6 +1197,131 @@ struct SimWorker : SimShared
register_output_step(10*cycle);
write_output_files();
}
std::vector<std::string> split(std::string text, const char *delim)
{
std::vector<std::string> list;
char *p = strdup(text.c_str());
char *t = strtok(p, delim);
while (t != NULL) {
list.push_back(t);
t = strtok(NULL, delim);
}
free(p);
return list;
}
std::string signal_name(std::string const & name)
{
size_t pos = name.find_first_of("@");
if (pos==std::string::npos) {
pos = name.find_first_of("#");
if (pos==std::string::npos)
log_error("Line does not contain proper signal name `%s`\n", name.c_str());
}
return name.substr(0, pos);
}
void run_cosim_btor2_witness(Module *topmod)
{
log_assert(top == nullptr);
if ((clock.size()+clockn.size())==0)
log_error("Clock signal must be specified.\n");
std::ifstream f;
f.open(sim_filename.c_str());
if (f.fail() || GetSize(sim_filename) == 0)
log_error("Can not open file `%s`\n", sim_filename.c_str());
int state = 0;
int cycle = 0;
top = new SimInstance(this, scope, topmod);
register_signals();
int prev_cycle = 0;
int curr_cycle = 0;
std::vector<std::string> parts;
size_t len = 0;
while (!f.eof())
{
std::string line;
std::getline(f, line);
if (line.size()==0) continue;
if (line[0]=='#' || line[0]=='@' || line[0]=='.') {
if (line[0]!='.')
curr_cycle = atoi(line.c_str()+1);
else
curr_cycle = -1; // force detect change
if (curr_cycle != prev_cycle) {
log("Simulating cycle %d.\n", cycle);
set_inports(clock, State::S1);
set_inports(clockn, State::S0);
update();
register_output_step(10*cycle+0);
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
update();
register_output_step(10*cycle+5);
cycle++;
prev_cycle = curr_cycle;
}
if (line[0]=='.') break;
continue;
}
switch(state)
{
case 0:
if (line=="sat")
state = 1;
break;
case 1:
if (line[0]=='b' || line[0]=='j')
state = 2;
else
log_error("Line does not contain property.\n");
break;
default: // set state or inputs
parts = split(line, " ");
len = parts.size();
if (len<3 || len>4)
log_error("Invalid set state line content.\n");
RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[len-1]));
if (len==3) {
Wire *w = topmod->wire(escaped_s);
if (!w) {
Cell *c = topmod->cell(escaped_s);
if (!c)
log_warning("Wire/cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
else if (c->type.in(ID($anyconst), ID($anyseq))) {
SigSpec sig_y= c->getPort(ID::Y);
if ((int)parts[1].size() != GetSize(sig_y))
log_error("Size of wire %s is different than provided data.\n", log_signal(sig_y));
top->set_state(sig_y, Const::from_string(parts[1]));
}
} else {
if ((int)parts[1].size() != w->width)
log_error("Size of wire %s is different than provided data.\n", log_signal(w));
top->set_state(w, Const::from_string(parts[1]));
}
} else {
Cell *c = topmod->cell(escaped_s);
if (!c)
log_error("Cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
if (!c->is_mem_cell())
log_error("Cell %s is not memory cell in module %s\n",log_id(escaped_s),log_id(topmod));
Const addr = Const::from_string(parts[1].substr(1,parts[1].size()-2));
Const data = Const::from_string(parts[2]);
top->set_memory_state(c->parameters.at(ID::MEMID).decode_string(), addr, data);
}
break;
}
}
register_output_step(10*cycle);
write_output_files();
}
};
struct VCDWriter : public OutputWriter
@ -1311,14 +1450,19 @@ struct AIWWriter : public OutputWriter
void write(std::map<int, bool> &) override
{
if (!aiwfile.is_open()) return;
if (worker->map_filename.empty())
log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
std::ifstream mf(worker->map_filename);
std::string type, symbol;
int variable, index;
if (mf.fail())
log_cmd_error("Not able to read AIGER witness map file.\n");
while (mf >> type >> variable >> index >> symbol) {
RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
Wire *w = worker->top->module->wire(escaped_s);
if (!w)
log_error("Wire %s not present in module %s\n",log_signal(w),log_id(worker->top->module));
log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(worker->top->module));
if (index < w->start_offset || index > w->start_offset + w->width)
log_error("Index %d for wire %s is out of range\n", index, log_signal(w));
if (type == "input") {
@ -1483,6 +1627,13 @@ struct SimPass : public Pass {
log(" enable debug output\n");
log("\n");
}
static std::string file_base_name(std::string const & path)
{
return path.substr(path.find_last_of("/\\") + 1);
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
SimWorker worker;
@ -1632,11 +1783,21 @@ struct SimPass : public Pass {
if (worker.sim_filename.empty())
worker.run(top_mod, numcycles);
else
else {
std::string filename_trim = file_base_name(worker.sim_filename);
if (filename_trim.size() > 4 && ((filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) ||
filename_trim.compare(filename_trim.size()-4, std::string::npos, ".vcd") == 0)) {
worker.run_cosim_fst(top_mod, numcycles);
} else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".aiw") == 0) {
if (worker.map_filename.empty())
worker.run_cosim(top_mod, numcycles);
else
worker.run_cosim_witness(top_mod);
log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
worker.run_cosim_aiger_witness(top_mod);
} else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
worker.run_cosim_btor2_witness(top_mod);
} else {
log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
}
}
}
} SimPass;