mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-24 01:25:33 +00:00
Merge branch 'master' into xaig
This commit is contained in:
Eddie Hung
commit
bca3cf6843
115 changed files with 5852 additions and 720 deletions
|
|
@ -615,6 +615,7 @@ struct BtorWorker
|
|||
{
|
||||
int abits = cell->getParam("\\ABITS").as_int();
|
||||
int width = cell->getParam("\\WIDTH").as_int();
|
||||
int nwords = cell->getParam("\\SIZE").as_int();
|
||||
int rdports = cell->getParam("\\RD_PORTS").as_int();
|
||||
int wrports = cell->getParam("\\WR_PORTS").as_int();
|
||||
|
||||
|
|
@ -641,6 +642,52 @@ struct BtorWorker
|
|||
int data_sid = get_bv_sid(width);
|
||||
int bool_sid = get_bv_sid(1);
|
||||
int sid = get_mem_sid(abits, width);
|
||||
|
||||
Const initdata = cell->getParam("\\INIT");
|
||||
initdata.exts(nwords*width);
|
||||
int nid_init_val = -1;
|
||||
|
||||
if (!initdata.is_fully_undef())
|
||||
{
|
||||
bool constword = true;
|
||||
Const firstword = initdata.extract(0, width);
|
||||
|
||||
for (int i = 1; i < nwords; i++) {
|
||||
Const thisword = initdata.extract(i*width, width);
|
||||
if (thisword != firstword) {
|
||||
constword = false;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (constword)
|
||||
{
|
||||
if (verbose)
|
||||
btorf("; initval = %s\n", log_signal(firstword));
|
||||
nid_init_val = get_sig_nid(firstword);
|
||||
}
|
||||
else
|
||||
{
|
||||
int nid_init_val = next_nid++;
|
||||
btorf("%d state %d\n", nid_init_val, sid);
|
||||
|
||||
for (int i = 0; i < nwords; i++) {
|
||||
Const thisword = initdata.extract(i*width, width);
|
||||
if (thisword.is_fully_undef())
|
||||
continue;
|
||||
Const thisaddr(i, abits);
|
||||
int nid_thisword = get_sig_nid(thisword);
|
||||
int nid_thisaddr = get_sig_nid(thisaddr);
|
||||
int last_nid_init_val = nid_init_val;
|
||||
nid_init_val = next_nid++;
|
||||
if (verbose)
|
||||
btorf("; initval[%d] = %s\n", i, log_signal(thisword));
|
||||
btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
int nid = next_nid++;
|
||||
int nid_head = nid;
|
||||
|
||||
|
|
@ -649,6 +696,12 @@ struct BtorWorker
|
|||
else
|
||||
btorf("%d state %d %s\n", nid, sid, log_id(cell));
|
||||
|
||||
if (nid_init_val >= 0)
|
||||
{
|
||||
int nid_init = next_nid++;
|
||||
btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
|
||||
}
|
||||
|
||||
if (asyncwr)
|
||||
{
|
||||
for (int port = 0; port < wrports; port++)
|
||||
|
|
@ -932,9 +985,8 @@ struct BtorWorker
|
|||
|
||||
btorf_push(stringf("output %s", log_id(wire)));
|
||||
|
||||
int sid = get_bv_sid(GetSize(wire));
|
||||
int nid = get_sig_nid(wire);
|
||||
btorf("%d output %d %d %s\n", next_nid++, sid, nid, log_id(wire));
|
||||
btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
|
||||
|
||||
btorf_pop(stringf("output %s", log_id(wire)));
|
||||
}
|
||||
|
|
|
|||
|
|
@ -130,7 +130,7 @@ struct EdifBackend : public Backend {
|
|||
bool port_rename = false;
|
||||
bool attr_properties = false;
|
||||
std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
|
||||
bool nogndvcc = false, gndvccy = true;
|
||||
bool nogndvcc = false, gndvccy = false;
|
||||
CellTypes ct(design);
|
||||
EdifNames edif_names;
|
||||
|
||||
|
|
|
|||
|
|
@ -106,6 +106,95 @@ struct FirrtlWorker
|
|||
RTLIL::Design *design;
|
||||
std::string indent;
|
||||
|
||||
// Define read/write ports and memories.
|
||||
// We'll collect their definitions and emit the corresponding FIRRTL definitions at the appropriate point in module construction.
|
||||
// For the moment, we don't handle $readmemh or $readmemb.
|
||||
// These will be part of a subsequent PR.
|
||||
struct read_port {
|
||||
string name;
|
||||
bool clk_enable;
|
||||
bool clk_parity;
|
||||
bool transparent;
|
||||
RTLIL::SigSpec clk;
|
||||
RTLIL::SigSpec ena;
|
||||
RTLIL::SigSpec addr;
|
||||
read_port(string name, bool clk_enable, bool clk_parity, bool transparent, RTLIL::SigSpec clk, RTLIL::SigSpec ena, RTLIL::SigSpec addr) : name(name), clk_enable(clk_enable), clk_parity(clk_parity), transparent(transparent), clk(clk), ena(ena), addr(addr) {
|
||||
// Current (3/13/2019) conventions:
|
||||
// generate a constant 0 for clock and a constant 1 for enable if they are undefined.
|
||||
if (!clk.is_fully_def())
|
||||
this->clk = SigSpec(RTLIL::Const(0, 1));
|
||||
if (!ena.is_fully_def())
|
||||
this->ena = SigSpec(RTLIL::Const(1, 1));
|
||||
}
|
||||
string gen_read(const char * indent) {
|
||||
string addr_expr = make_expr(addr);
|
||||
string ena_expr = make_expr(ena);
|
||||
string clk_expr = make_expr(clk);
|
||||
string addr_str = stringf("%s%s.addr <= %s\n", indent, name.c_str(), addr_expr.c_str());
|
||||
string ena_str = stringf("%s%s.en <= %s\n", indent, name.c_str(), ena_expr.c_str());
|
||||
string clk_str = stringf("%s%s.clk <= asClock(%s)\n", indent, name.c_str(), clk_expr.c_str());
|
||||
return addr_str + ena_str + clk_str;
|
||||
}
|
||||
};
|
||||
struct write_port : read_port {
|
||||
RTLIL::SigSpec mask;
|
||||
write_port(string name, bool clk_enable, bool clk_parity, bool transparent, RTLIL::SigSpec clk, RTLIL::SigSpec ena, RTLIL::SigSpec addr, RTLIL::SigSpec mask) : read_port(name, clk_enable, clk_parity, transparent, clk, ena, addr), mask(mask) {
|
||||
if (!clk.is_fully_def())
|
||||
this->clk = SigSpec(RTLIL::Const(0));
|
||||
if (!ena.is_fully_def())
|
||||
this->ena = SigSpec(RTLIL::Const(0));
|
||||
if (!mask.is_fully_def())
|
||||
this->ena = SigSpec(RTLIL::Const(1));
|
||||
}
|
||||
string gen_read(const char * /* indent */) {
|
||||
log_error("gen_read called on write_port: %s\n", name.c_str());
|
||||
return stringf("gen_read called on write_port: %s\n", name.c_str());
|
||||
}
|
||||
string gen_write(const char * indent) {
|
||||
string addr_expr = make_expr(addr);
|
||||
string ena_expr = make_expr(ena);
|
||||
string clk_expr = make_expr(clk);
|
||||
string mask_expr = make_expr(mask);
|
||||
string mask_str = stringf("%s%s.mask <= %s\n", indent, name.c_str(), mask_expr.c_str());
|
||||
string addr_str = stringf("%s%s.addr <= %s\n", indent, name.c_str(), addr_expr.c_str());
|
||||
string ena_str = stringf("%s%s.en <= %s\n", indent, name.c_str(), ena_expr.c_str());
|
||||
string clk_str = stringf("%s%s.clk <= asClock(%s)\n", indent, name.c_str(), clk_expr.c_str());
|
||||
return addr_str + ena_str + clk_str + mask_str;
|
||||
}
|
||||
};
|
||||
/* Memories defined within this module. */
|
||||
struct memory {
|
||||
string name; // memory name
|
||||
int abits; // number of address bits
|
||||
int size; // size (in units) of the memory
|
||||
int width; // size (in bits) of each element
|
||||
int read_latency;
|
||||
int write_latency;
|
||||
vector<read_port> read_ports;
|
||||
vector<write_port> write_ports;
|
||||
std::string init_file;
|
||||
std::string init_file_srcFileSpec;
|
||||
memory(string name, int abits, int size, int width) : name(name), abits(abits), size(size), width(width), read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec("") {}
|
||||
memory() : read_latency(0), write_latency(1), init_file(""), init_file_srcFileSpec(""){}
|
||||
void add_memory_read_port(read_port &rp) {
|
||||
read_ports.push_back(rp);
|
||||
}
|
||||
void add_memory_write_port(write_port &wp) {
|
||||
write_ports.push_back(wp);
|
||||
}
|
||||
void add_memory_file(std::string init_file, std::string init_file_srcFileSpec) {
|
||||
this->init_file = init_file;
|
||||
this->init_file_srcFileSpec = init_file_srcFileSpec;
|
||||
}
|
||||
|
||||
};
|
||||
dict<string, memory> memories;
|
||||
|
||||
void register_memory(memory &m)
|
||||
{
|
||||
memories[m.name] = m;
|
||||
}
|
||||
|
||||
void register_reverse_wire_map(string id, SigSpec sig)
|
||||
{
|
||||
for (int i = 0; i < GetSize(sig); i++)
|
||||
|
|
@ -116,7 +205,7 @@ struct FirrtlWorker
|
|||
{
|
||||
}
|
||||
|
||||
string make_expr(const SigSpec &sig)
|
||||
static string make_expr(const SigSpec &sig)
|
||||
{
|
||||
string expr;
|
||||
|
||||
|
|
@ -165,11 +254,9 @@ struct FirrtlWorker
|
|||
|
||||
std::string fid(RTLIL::IdString internal_id)
|
||||
{
|
||||
const char *str = internal_id.c_str();
|
||||
return *str == '\\' ? str + 1 : str;
|
||||
return make_id(internal_id);
|
||||
}
|
||||
|
||||
|
||||
std::string cellname(RTLIL::Cell *cell)
|
||||
{
|
||||
return fid(cell->name).c_str();
|
||||
|
|
@ -219,29 +306,42 @@ struct FirrtlWorker
|
|||
if (it->second.size() > 0) {
|
||||
const SigSpec &secondSig = it->second;
|
||||
const std::string firstName = cell_name + "." + make_id(it->first);
|
||||
const std::string secondName = make_expr(secondSig);
|
||||
const std::string secondExpr = make_expr(secondSig);
|
||||
// Find the direction for this port.
|
||||
FDirection dir = getPortFDirection(it->first, instModule);
|
||||
std::string source, sink;
|
||||
std::string sourceExpr, sinkExpr;
|
||||
const SigSpec *sinkSig = nullptr;
|
||||
switch (dir) {
|
||||
case FD_INOUT:
|
||||
log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", cell_type.c_str(), log_signal(it->second));
|
||||
case FD_OUT:
|
||||
source = firstName;
|
||||
sink = secondName;
|
||||
sourceExpr = firstName;
|
||||
sinkExpr = secondExpr;
|
||||
sinkSig = &secondSig;
|
||||
break;
|
||||
case FD_NODIRECTION:
|
||||
log_warning("Instance port connection %s.%s is NODIRECTION; treating as IN\n", cell_type.c_str(), log_signal(it->second));
|
||||
/* FALL_THROUGH */
|
||||
case FD_IN:
|
||||
source = secondName;
|
||||
sink = firstName;
|
||||
sourceExpr = secondExpr;
|
||||
sinkExpr = firstName;
|
||||
break;
|
||||
default:
|
||||
log_error("Instance port %s.%s unrecognized connection direction 0x%x !\n", cell_type.c_str(), log_signal(it->second), dir);
|
||||
break;
|
||||
}
|
||||
wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sink.c_str(), source.c_str()));
|
||||
// Check for subfield assignment.
|
||||
std::string bitsString = "bits(";
|
||||
if (sinkExpr.substr(0, bitsString.length()) == bitsString ) {
|
||||
if (sinkSig == nullptr)
|
||||
log_error("Unknown subfield %s.%s\n", cell_type.c_str(), sinkExpr.c_str());
|
||||
// Don't generate the assignment here.
|
||||
// Add the source and sink to the "reverse_wire_map" and we'll output the assignment
|
||||
// as part of the coalesced subfield assignments for this wire.
|
||||
register_reverse_wire_map(sourceExpr, *sinkSig);
|
||||
} else {
|
||||
wire_exprs.push_back(stringf("\n%s%s <= %s", indent.c_str(), sinkExpr.c_str(), sourceExpr.c_str()));
|
||||
}
|
||||
}
|
||||
}
|
||||
wire_exprs.push_back(stringf("\n"));
|
||||
|
|
@ -504,6 +604,7 @@ struct FirrtlWorker
|
|||
int abits = cell->parameters.at("\\ABITS").as_int();
|
||||
int width = cell->parameters.at("\\WIDTH").as_int();
|
||||
int size = cell->parameters.at("\\SIZE").as_int();
|
||||
memory m(mem_id, abits, size, width);
|
||||
int rd_ports = cell->parameters.at("\\RD_PORTS").as_int();
|
||||
int wr_ports = cell->parameters.at("\\WR_PORTS").as_int();
|
||||
|
||||
|
|
@ -520,33 +621,24 @@ struct FirrtlWorker
|
|||
if (offset != 0)
|
||||
log_error("Memory with nonzero offset: %s.%s\n", log_id(module), log_id(cell));
|
||||
|
||||
cell_exprs.push_back(stringf(" mem %s:\n", mem_id.c_str()));
|
||||
cell_exprs.push_back(stringf(" data-type => UInt<%d>\n", width));
|
||||
cell_exprs.push_back(stringf(" depth => %d\n", size));
|
||||
|
||||
for (int i = 0; i < rd_ports; i++)
|
||||
cell_exprs.push_back(stringf(" reader => r%d\n", i));
|
||||
|
||||
for (int i = 0; i < wr_ports; i++)
|
||||
cell_exprs.push_back(stringf(" writer => w%d\n", i));
|
||||
|
||||
cell_exprs.push_back(stringf(" read-latency => 0\n"));
|
||||
cell_exprs.push_back(stringf(" write-latency => 1\n"));
|
||||
cell_exprs.push_back(stringf(" read-under-write => undefined\n"));
|
||||
|
||||
for (int i = 0; i < rd_ports; i++)
|
||||
{
|
||||
if (rd_clk_enable[i] != State::S0)
|
||||
log_error("Clocked read port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
|
||||
|
||||
SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(i*abits, abits);
|
||||
SigSpec data_sig = cell->getPort("\\RD_DATA").extract(i*width, width);
|
||||
string addr_expr = make_expr(cell->getPort("\\RD_ADDR").extract(i*abits, abits));
|
||||
|
||||
cell_exprs.push_back(stringf(" %s.r%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
|
||||
cell_exprs.push_back(stringf(" %s.r%d.en <= UInt<1>(1)\n", mem_id.c_str(), i));
|
||||
cell_exprs.push_back(stringf(" %s.r%d.clk <= asClock(UInt<1>(0))\n", mem_id.c_str(), i));
|
||||
|
||||
register_reverse_wire_map(stringf("%s.r%d.data", mem_id.c_str(), i), data_sig);
|
||||
string addr_expr = make_expr(addr_sig);
|
||||
string name(stringf("%s.r%d", m.name.c_str(), i));
|
||||
bool clk_enable = false;
|
||||
bool clk_parity = true;
|
||||
bool transparency = false;
|
||||
SigSpec ena_sig = RTLIL::SigSpec(RTLIL::State::S1, 1);
|
||||
SigSpec clk_sig = RTLIL::SigSpec(RTLIL::State::S0, 1);
|
||||
read_port rp(name, clk_enable, clk_parity, transparency, clk_sig, ena_sig, addr_sig);
|
||||
m.add_memory_read_port(rp);
|
||||
cell_exprs.push_back(rp.gen_read(indent.c_str()));
|
||||
register_reverse_wire_map(stringf("%s.data", name.c_str()), data_sig);
|
||||
}
|
||||
|
||||
for (int i = 0; i < wr_ports; i++)
|
||||
|
|
@ -557,9 +649,16 @@ struct FirrtlWorker
|
|||
if (wr_clk_polarity[i] != State::S1)
|
||||
log_error("Negedge write port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
|
||||
|
||||
string addr_expr = make_expr(cell->getPort("\\WR_ADDR").extract(i*abits, abits));
|
||||
string data_expr = make_expr(cell->getPort("\\WR_DATA").extract(i*width, width));
|
||||
string clk_expr = make_expr(cell->getPort("\\WR_CLK").extract(i));
|
||||
string name(stringf("%s.w%d", m.name.c_str(), i));
|
||||
bool clk_enable = true;
|
||||
bool clk_parity = true;
|
||||
bool transparency = false;
|
||||
SigSpec addr_sig =cell->getPort("\\WR_ADDR").extract(i*abits, abits);
|
||||
string addr_expr = make_expr(addr_sig);
|
||||
SigSpec data_sig =cell->getPort("\\WR_DATA").extract(i*width, width);
|
||||
string data_expr = make_expr(data_sig);
|
||||
SigSpec clk_sig = cell->getPort("\\WR_CLK").extract(i);
|
||||
string clk_expr = make_expr(clk_sig);
|
||||
|
||||
SigSpec wen_sig = cell->getPort("\\WR_EN").extract(i*width, width);
|
||||
string wen_expr = make_expr(wen_sig[0]);
|
||||
|
|
@ -568,13 +667,50 @@ struct FirrtlWorker
|
|||
if (wen_sig[0] != wen_sig[i])
|
||||
log_error("Complex write enable on port %d on memory %s.%s.\n", i, log_id(module), log_id(cell));
|
||||
|
||||
cell_exprs.push_back(stringf(" %s.w%d.addr <= %s\n", mem_id.c_str(), i, addr_expr.c_str()));
|
||||
cell_exprs.push_back(stringf(" %s.w%d.data <= %s\n", mem_id.c_str(), i, data_expr.c_str()));
|
||||
cell_exprs.push_back(stringf(" %s.w%d.en <= %s\n", mem_id.c_str(), i, wen_expr.c_str()));
|
||||
cell_exprs.push_back(stringf(" %s.w%d.mask <= UInt<1>(1)\n", mem_id.c_str(), i));
|
||||
cell_exprs.push_back(stringf(" %s.w%d.clk <= asClock(%s)\n", mem_id.c_str(), i, clk_expr.c_str()));
|
||||
SigSpec mask_sig = RTLIL::SigSpec(RTLIL::State::S1, 1);
|
||||
write_port wp(name, clk_enable, clk_parity, transparency, clk_sig, wen_sig[0], addr_sig, mask_sig);
|
||||
m.add_memory_write_port(wp);
|
||||
cell_exprs.push_back(stringf("%s%s.data <= %s\n", indent.c_str(), name.c_str(), data_expr.c_str()));
|
||||
cell_exprs.push_back(wp.gen_write(indent.c_str()));
|
||||
}
|
||||
register_memory(m);
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$memwr", "$memrd", "$meminit"))
|
||||
{
|
||||
std::string cell_type = fid(cell->type);
|
||||
std::string mem_id = make_id(cell->parameters["\\MEMID"].decode_string());
|
||||
memory *mp = nullptr;
|
||||
if (cell->type == "$meminit" ) {
|
||||
log_error("$meminit (%s.%s.%s) currently unsupported\n", log_id(module), log_id(cell), mem_id.c_str());
|
||||
} else {
|
||||
// It's a $memwr or $memrd. Remember the read/write port parameters for the eventual FIRRTL memory definition.
|
||||
auto addrSig = cell->getPort("\\ADDR");
|
||||
auto dataSig = cell->getPort("\\DATA");
|
||||
auto enableSig = cell->getPort("\\EN");
|
||||
auto clockSig = cell->getPort("\\CLK");
|
||||
Const clk_enable = cell->parameters.at("\\CLK_ENABLE");
|
||||
Const clk_polarity = cell->parameters.at("\\CLK_POLARITY");
|
||||
|
||||
mp = &memories.at(mem_id);
|
||||
int portNum = 0;
|
||||
bool transparency = false;
|
||||
string data_expr = make_expr(dataSig);
|
||||
if (cell->type.in("$memwr")) {
|
||||
portNum = (int) mp->write_ports.size();
|
||||
write_port wp(stringf("%s.w%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(), transparency, clockSig, enableSig, addrSig, dataSig);
|
||||
mp->add_memory_write_port(wp);
|
||||
cell_exprs.push_back(stringf("%s%s.data <= %s\n", indent.c_str(), wp.name.c_str(), data_expr.c_str()));
|
||||
cell_exprs.push_back(wp.gen_write(indent.c_str()));
|
||||
} else if (cell->type.in("$memrd")) {
|
||||
portNum = (int) mp->read_ports.size();
|
||||
read_port rp(stringf("%s.r%d", mem_id.c_str(), portNum), clk_enable.as_bool(), clk_polarity.as_bool(), transparency, clockSig, enableSig, addrSig);
|
||||
mp->add_memory_read_port(rp);
|
||||
cell_exprs.push_back(rp.gen_read(indent.c_str()));
|
||||
register_reverse_wire_map(stringf("%s.data", rp.name.c_str()), dataSig);
|
||||
}
|
||||
}
|
||||
continue;
|
||||
}
|
||||
|
||||
|
|
@ -752,6 +888,24 @@ struct FirrtlWorker
|
|||
|
||||
f << stringf("\n");
|
||||
|
||||
// If we have any memory definitions, output them.
|
||||
for (auto kv : memories) {
|
||||
memory m = kv.second;
|
||||
f << stringf(" mem %s:\n", m.name.c_str());
|
||||
f << stringf(" data-type => UInt<%d>\n", m.width);
|
||||
f << stringf(" depth => %d\n", m.size);
|
||||
for (int i = 0; i < (int) m.read_ports.size(); i += 1) {
|
||||
f << stringf(" reader => r%d\n", i);
|
||||
}
|
||||
for (int i = 0; i < (int) m.write_ports.size(); i += 1) {
|
||||
f << stringf(" writer => w%d\n", i);
|
||||
}
|
||||
f << stringf(" read-latency => %d\n", m.read_latency);
|
||||
f << stringf(" write-latency => %d\n", m.write_latency);
|
||||
f << stringf(" read-under-write => undefined\n");
|
||||
}
|
||||
f << stringf("\n");
|
||||
|
||||
for (auto str : cell_exprs)
|
||||
f << str;
|
||||
|
||||
|
|
|
|||
|
|
@ -204,7 +204,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const
|
|||
f << stringf("%s case ", indent.c_str());
|
||||
for (size_t i = 0; i < (*it)->compare.size(); i++) {
|
||||
if (i > 0)
|
||||
f << stringf(", ");
|
||||
f << stringf(" , ");
|
||||
dump_sigspec(f, (*it)->compare[i]);
|
||||
}
|
||||
f << stringf("\n");
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ struct ProtobufDesignSerializer
|
|||
|
||||
ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
|
||||
aig_mode_(aig_mode), use_selection_(use_selection) { }
|
||||
|
||||
|
||||
string get_name(IdString name)
|
||||
{
|
||||
return RTLIL::unescape_id(name);
|
||||
|
|
@ -60,7 +60,7 @@ struct ProtobufDesignSerializer
|
|||
{
|
||||
for (auto ¶m : parameters) {
|
||||
std::string key = get_name(param.first);
|
||||
|
||||
|
||||
|
||||
yosys::pb::Parameter pb_param;
|
||||
|
||||
|
|
@ -207,7 +207,7 @@ struct ProtobufDesignSerializer
|
|||
(*models)[aig.name] = pb_model;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void serialize_design(yosys::pb::Design *pb, Design *design)
|
||||
{
|
||||
GOOGLE_PROTOBUF_VERIFY_VERSION;
|
||||
|
|
|
|||
|
|
@ -3,14 +3,30 @@ OBJS += backends/smt2/smt2.o
|
|||
|
||||
ifneq ($(CONFIG),mxe)
|
||||
ifneq ($(CONFIG),emcc)
|
||||
|
||||
# MSYS targets support yosys-smtbmc, but require a launcher script
|
||||
ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
|
||||
TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py
|
||||
# Needed to find the Python interpreter for yosys-smtbmc scripts.
|
||||
# Override if necessary, it is only used for msys2 targets.
|
||||
PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
|
||||
|
||||
yosys-smtbmc-script.py: backends/smt2/smtbmc.py
|
||||
$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \
|
||||
-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
|
||||
|
||||
yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
|
||||
$(P) gcc -DGUI=0 -O -s -o $@ $<
|
||||
# Other targets
|
||||
else
|
||||
TARGETS += yosys-smtbmc
|
||||
|
||||
yosys-smtbmc: backends/smt2/smtbmc.py
|
||||
$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
|
||||
$(Q) chmod +x $@.new
|
||||
$(Q) mv $@.new $@
|
||||
endif
|
||||
|
||||
$(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
|
||||
endif
|
||||
endif
|
||||
|
||||
|
|
|
|||
|
|
@ -416,6 +416,7 @@ struct Smt2Worker
|
|||
for (char ch : expr) {
|
||||
if (ch == 'A') processed_expr += get_bv(sig_a);
|
||||
else if (ch == 'B') processed_expr += get_bv(sig_b);
|
||||
else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
|
||||
else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
|
||||
else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
|
||||
else processed_expr += ch;
|
||||
|
|
@ -554,7 +555,7 @@ struct Smt2Worker
|
|||
|
||||
if (cell->type.in("$shift", "$shiftx")) {
|
||||
if (cell->getParam("\\B_SIGNED").as_bool()) {
|
||||
return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
|
||||
return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
|
||||
"(bvlshr A B) (bvlshr A (bvneg B)))",
|
||||
GetSize(cell->getPort("\\B")), 0), 's');
|
||||
} else {
|
||||
|
|
@ -887,8 +888,8 @@ struct Smt2Worker
|
|||
|
||||
string name_a = get_bool(cell->getPort("\\A"));
|
||||
string name_en = get_bool(cell->getPort("\\EN"));
|
||||
decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
|
||||
cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
|
||||
string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
|
||||
decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
|
||||
|
||||
if (cell->type == "$cover")
|
||||
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
|
||||
|
|
@ -1103,20 +1104,27 @@ struct Smt2Worker
|
|||
break;
|
||||
|
||||
Const initword = init_data.extract(i*width, width, State::Sx);
|
||||
Const initmask = initword;
|
||||
bool gen_init_constr = false;
|
||||
|
||||
for (auto bit : initword.bits)
|
||||
if (bit == State::S0 || bit == State::S1)
|
||||
for (int k = 0; k < GetSize(initword); k++) {
|
||||
if (initword[k] == State::S0 || initword[k] == State::S1) {
|
||||
gen_init_constr = true;
|
||||
initmask[k] = State::S1;
|
||||
} else {
|
||||
initmask[k] = State::S0;
|
||||
initword[k] = State::S0;
|
||||
}
|
||||
}
|
||||
|
||||
if (gen_init_constr)
|
||||
{
|
||||
if (statebv)
|
||||
/* FIXME */;
|
||||
else
|
||||
init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
|
||||
init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
|
||||
get_id(module), arrayid, Const(i, abits).as_string().c_str(),
|
||||
initword.as_string().c_str(), get_id(cell), i));
|
||||
initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1484,11 +1484,11 @@ else: # not tempind, covermode
|
|||
smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
|
||||
smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
|
||||
smt_assert_consequent(get_constr_expr(constr_assumes, i))
|
||||
print_msg("Re-solving with appended steps..")
|
||||
if smt_check_sat() == "unsat":
|
||||
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
|
||||
retstatus = False
|
||||
break
|
||||
print_msg("Re-solving with appended steps..")
|
||||
if smt_check_sat() == "unsat":
|
||||
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
|
||||
retstatus = False
|
||||
break
|
||||
print_anyconsts(step)
|
||||
for i in range(step, last_check_step+1):
|
||||
print_failed_asserts(i)
|
||||
|
|
|
|||
|
|
@ -33,7 +33,7 @@
|
|||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal;
|
||||
bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, defparam, decimal, siminit;
|
||||
int auto_name_counter, auto_name_offset, auto_name_digits;
|
||||
std::map<RTLIL::IdString, int> auto_name_map;
|
||||
std::set<RTLIL::IdString> reg_wires, reg_ct;
|
||||
|
|
@ -1310,7 +1310,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
|
|||
}
|
||||
}
|
||||
|
||||
if (reg_ct.count(cell->type) && cell->hasPort("\\Q")) {
|
||||
if (siminit && reg_ct.count(cell->type) && cell->hasPort("\\Q")) {
|
||||
std::stringstream ss;
|
||||
dump_reg_init(ss, cell->getPort("\\Q"));
|
||||
if (!ss.str().empty()) {
|
||||
|
|
@ -1607,6 +1607,10 @@ struct VerilogBackend : public Backend {
|
|||
log(" without this option all internal cells are converted to Verilog\n");
|
||||
log(" expressions.\n");
|
||||
log("\n");
|
||||
log(" -siminit\n");
|
||||
log(" add initial statements with hierarchical refs to initialize FFs when\n");
|
||||
log(" in -noexpr mode.\n");
|
||||
log("\n");
|
||||
log(" -nodec\n");
|
||||
log(" 32-bit constant values are by default dumped as decimal numbers,\n");
|
||||
log(" not bit pattern. This option deactivates this feature and instead\n");
|
||||
|
|
@ -1663,11 +1667,14 @@ struct VerilogBackend : public Backend {
|
|||
nostr = false;
|
||||
defparam = false;
|
||||
decimal = false;
|
||||
siminit = false;
|
||||
auto_prefix = "";
|
||||
|
||||
bool blackboxes = false;
|
||||
bool selected = false;
|
||||
|
||||
auto_name_map.clear();
|
||||
reg_wires.clear();
|
||||
reg_ct.clear();
|
||||
|
||||
reg_ct.insert("$dff");
|
||||
|
|
@ -1739,6 +1746,10 @@ struct VerilogBackend : public Backend {
|
|||
decimal = true;
|
||||
continue;
|
||||
}
|
||||
if (arg == "-siminit") {
|
||||
siminit = true;
|
||||
continue;
|
||||
}
|
||||
if (arg == "-blackboxes") {
|
||||
blackboxes = true;
|
||||
continue;
|
||||
|
|
@ -1770,6 +1781,8 @@ struct VerilogBackend : public Backend {
|
|||
dump_module(*f, "", it->second);
|
||||
}
|
||||
|
||||
auto_name_map.clear();
|
||||
reg_wires.clear();
|
||||
reg_ct.clear();
|
||||
}
|
||||
} VerilogBackend;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue