mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-08 10:25:19 +00:00
Merge pull request #893 from YosysHQ/clifford/btormeminit
Memory init support in write_btor
This commit is contained in:
commit
2cf71e2a7b
|
@ -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)));
|
||||
}
|
||||
|
|
|
@ -3237,7 +3237,7 @@ void RTLIL::SigSpec::extend_u0(int width, bool is_signed)
|
|||
remove(width, width_ - width);
|
||||
|
||||
if (width_ < width) {
|
||||
RTLIL::SigBit padding = width_ > 0 ? (*this)[width_ - 1] : RTLIL::State::S0;
|
||||
RTLIL::SigBit padding = width_ > 0 ? (*this)[width_ - 1] : RTLIL::State::Sx;
|
||||
if (!is_signed)
|
||||
padding = RTLIL::State::S0;
|
||||
while (width_ < width)
|
||||
|
|
|
@ -546,6 +546,14 @@ struct RTLIL::Const
|
|||
return ret;
|
||||
}
|
||||
|
||||
void extu(int width) {
|
||||
bits.resize(width, RTLIL::State::S0);
|
||||
}
|
||||
|
||||
void exts(int width) {
|
||||
bits.resize(width, bits.empty() ? RTLIL::State::Sx : bits.back());
|
||||
}
|
||||
|
||||
inline unsigned int hash() const {
|
||||
unsigned int h = mkhash_init;
|
||||
for (auto b : bits)
|
||||
|
|
Loading…
Reference in a new issue