mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-24 01:25:33 +00:00
Merge branch 'master' of github.com:YosysHQ/yosys into firrtl_backend_fileinfo
This commit is contained in:
commit
9edf8869c1
228 changed files with 8971 additions and 6952 deletions
|
@ -126,9 +126,9 @@ struct AigerWriter
|
|||
|
||||
for (auto wire : module->wires())
|
||||
{
|
||||
if (wire->attributes.count("\\init")) {
|
||||
if (wire->attributes.count(ID::init)) {
|
||||
SigSpec initsig = sigmap(wire);
|
||||
Const initval = wire->attributes.at("\\init");
|
||||
Const initval = wire->attributes.at(ID::init);
|
||||
for (int i = 0; i < GetSize(wire) && i < GetSize(initval); i++)
|
||||
if (initval[i] == State::S0 || initval[i] == State::S1)
|
||||
init_map[initsig[i]] = initval[i] == State::S1;
|
||||
|
@ -169,31 +169,31 @@ struct AigerWriter
|
|||
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
if (cell->type == "$_NOT_")
|
||||
if (cell->type == ID($_NOT_))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
|
||||
unused_bits.erase(A);
|
||||
undriven_bits.erase(Y);
|
||||
not_map[Y] = A;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_FF_", "$_DFF_N_", "$_DFF_P_"))
|
||||
if (cell->type.in(ID($_FF_), ID($_DFF_N_), ID($_DFF_P_)))
|
||||
{
|
||||
SigBit D = sigmap(cell->getPort("\\D").as_bit());
|
||||
SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
|
||||
SigBit D = sigmap(cell->getPort(ID::D).as_bit());
|
||||
SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
|
||||
unused_bits.erase(D);
|
||||
undriven_bits.erase(Q);
|
||||
ff_map[Q] = D;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_AND_")
|
||||
if (cell->type == ID($_AND_))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit B = sigmap(cell->getPort("\\B").as_bit());
|
||||
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit B = sigmap(cell->getPort(ID::B).as_bit());
|
||||
SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
|
||||
unused_bits.erase(A);
|
||||
unused_bits.erase(B);
|
||||
undriven_bits.erase(Y);
|
||||
|
@ -201,66 +201,66 @@ struct AigerWriter
|
|||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$initstate")
|
||||
if (cell->type == ID($initstate))
|
||||
{
|
||||
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
|
||||
SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
|
||||
undriven_bits.erase(Y);
|
||||
initstate_bits.insert(Y);
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$assert")
|
||||
if (cell->type == ID($assert))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
|
||||
unused_bits.erase(A);
|
||||
unused_bits.erase(EN);
|
||||
asserts.push_back(make_pair(A, EN));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$assume")
|
||||
if (cell->type == ID($assume))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
|
||||
unused_bits.erase(A);
|
||||
unused_bits.erase(EN);
|
||||
assumes.push_back(make_pair(A, EN));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$live")
|
||||
if (cell->type == ID($live))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
|
||||
unused_bits.erase(A);
|
||||
unused_bits.erase(EN);
|
||||
liveness.push_back(make_pair(A, EN));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$fair")
|
||||
if (cell->type == ID($fair))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit EN = sigmap(cell->getPort("\\EN").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit EN = sigmap(cell->getPort(ID::EN).as_bit());
|
||||
unused_bits.erase(A);
|
||||
unused_bits.erase(EN);
|
||||
fairness.push_back(make_pair(A, EN));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$anyconst")
|
||||
if (cell->type == ID($anyconst))
|
||||
{
|
||||
for (auto bit : sigmap(cell->getPort("\\Y"))) {
|
||||
for (auto bit : sigmap(cell->getPort(ID::Y))) {
|
||||
undriven_bits.erase(bit);
|
||||
ff_map[bit] = bit;
|
||||
}
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$anyseq")
|
||||
if (cell->type == ID($anyseq))
|
||||
{
|
||||
for (auto bit : sigmap(cell->getPort("\\Y"))) {
|
||||
for (auto bit : sigmap(cell->getPort(ID::Y))) {
|
||||
undriven_bits.erase(bit);
|
||||
input_bits.insert(bit);
|
||||
}
|
||||
|
|
|
@ -174,7 +174,7 @@ struct XAigerWriter
|
|||
undriven_bits.insert(bit);
|
||||
unused_bits.insert(bit);
|
||||
|
||||
bool scc = wire->attributes.count(ID(abc9_scc));
|
||||
bool scc = wire->attributes.count(ID::abc9_scc);
|
||||
if (wire->port_input || scc)
|
||||
input_bits.insert(bit);
|
||||
|
||||
|
@ -190,21 +190,21 @@ struct XAigerWriter
|
|||
|
||||
for (auto cell : module->cells()) {
|
||||
if (!cell->has_keep_attr()) {
|
||||
if (cell->type == "$_NOT_")
|
||||
if (cell->type == ID($_NOT_))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
|
||||
unused_bits.erase(A);
|
||||
undriven_bits.erase(Y);
|
||||
not_map[Y] = A;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_AND_")
|
||||
if (cell->type == ID($_AND_))
|
||||
{
|
||||
SigBit A = sigmap(cell->getPort("\\A").as_bit());
|
||||
SigBit B = sigmap(cell->getPort("\\B").as_bit());
|
||||
SigBit Y = sigmap(cell->getPort("\\Y").as_bit());
|
||||
SigBit A = sigmap(cell->getPort(ID::A).as_bit());
|
||||
SigBit B = sigmap(cell->getPort(ID::B).as_bit());
|
||||
SigBit Y = sigmap(cell->getPort(ID::Y).as_bit());
|
||||
unused_bits.erase(A);
|
||||
unused_bits.erase(B);
|
||||
undriven_bits.erase(Y);
|
||||
|
@ -212,13 +212,13 @@ struct XAigerWriter
|
|||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$__ABC9_FF_" &&
|
||||
if (cell->type == ID($__ABC9_FF_) &&
|
||||
// The presence of an abc9_mergeability attribute indicates
|
||||
// that we do want to pass this flop to ABC
|
||||
cell->attributes.count("\\abc9_mergeability"))
|
||||
cell->attributes.count(ID::abc9_mergeability))
|
||||
{
|
||||
SigBit D = sigmap(cell->getPort("\\D").as_bit());
|
||||
SigBit Q = sigmap(cell->getPort("\\Q").as_bit());
|
||||
SigBit D = sigmap(cell->getPort(ID::D).as_bit());
|
||||
SigBit Q = sigmap(cell->getPort(ID::Q).as_bit());
|
||||
unused_bits.erase(D);
|
||||
undriven_bits.erase(Q);
|
||||
alias_map[Q] = D;
|
||||
|
@ -227,7 +227,7 @@ struct XAigerWriter
|
|||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$specify2", "$specify3", "$specrule"))
|
||||
if (cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
|
||||
continue;
|
||||
}
|
||||
|
||||
|
@ -239,7 +239,7 @@ struct XAigerWriter
|
|||
|
||||
bool abc9_flop = false;
|
||||
if (!cell->has_keep_attr()) {
|
||||
auto it = cell->attributes.find("\\abc9_box_seq");
|
||||
auto it = cell->attributes.find(ID::abc9_box_seq);
|
||||
if (it != cell->attributes.end()) {
|
||||
int abc9_box_seq = it->second.as_int();
|
||||
if (GetSize(box_list) <= abc9_box_seq)
|
||||
|
@ -247,7 +247,7 @@ struct XAigerWriter
|
|||
box_list[abc9_box_seq] = cell;
|
||||
// Only flop boxes may have arrival times
|
||||
// (all others are combinatorial)
|
||||
abc9_flop = inst_module->get_bool_attribute("\\abc9_flop");
|
||||
abc9_flop = inst_module->get_bool_attribute(ID::abc9_flop);
|
||||
if (!abc9_flop)
|
||||
continue;
|
||||
}
|
||||
|
@ -315,7 +315,7 @@ struct XAigerWriter
|
|||
|
||||
RTLIL::Module* box_module = module->design->module(cell->type);
|
||||
log_assert(box_module);
|
||||
log_assert(box_module->attributes.count("\\abc9_box_id") || box_module->get_bool_attribute("\\abc9_flop"));
|
||||
log_assert(box_module->attributes.count(ID::abc9_box_id) || box_module->get_bool_attribute(ID::abc9_flop));
|
||||
|
||||
auto r = box_ports.insert(cell->type);
|
||||
if (r.second) {
|
||||
|
@ -325,7 +325,7 @@ struct XAigerWriter
|
|||
for (const auto &port_name : box_module->ports) {
|
||||
auto w = box_module->wire(port_name);
|
||||
log_assert(w);
|
||||
if (w->get_bool_attribute("\\abc9_carry")) {
|
||||
if (w->get_bool_attribute(ID::abc9_carry)) {
|
||||
if (w->port_input) {
|
||||
if (carry_in != IdString())
|
||||
log_error("Module '%s' contains more than one 'abc9_carry' input port.\n", log_id(box_module));
|
||||
|
@ -381,7 +381,7 @@ struct XAigerWriter
|
|||
}
|
||||
|
||||
// Connect <cell>.abc9_ff.Q (inserted by abc9_map.v) as the last input to the flop box
|
||||
if (box_module->get_bool_attribute("\\abc9_flop")) {
|
||||
if (box_module->get_bool_attribute(ID::abc9_flop)) {
|
||||
SigSpec rhs = module->wire(stringf("%s.abc9_ff.Q", cell->name.c_str()));
|
||||
if (rhs.empty())
|
||||
log_error("'%s.abc9_ff.Q' is not a wire present in module '%s'.\n", log_id(cell), log_id(module));
|
||||
|
@ -437,7 +437,7 @@ struct XAigerWriter
|
|||
|
||||
for (const auto &i : ff_bits) {
|
||||
const Cell *cell = i.second;
|
||||
const SigBit &q = sigmap(cell->getPort("\\Q"));
|
||||
const SigBit &q = sigmap(cell->getPort(ID::Q));
|
||||
aig_m++, aig_i++;
|
||||
log_assert(!aig_map.count(q));
|
||||
aig_map[q] = 2*aig_m;
|
||||
|
@ -608,12 +608,12 @@ struct XAigerWriter
|
|||
|
||||
// For flops only, create an extra 1-bit input that drives a new wire
|
||||
// called "<cell>.abc9_ff.Q" that is used below
|
||||
if (box_module->get_bool_attribute("\\abc9_flop"))
|
||||
if (box_module->get_bool_attribute(ID::abc9_flop))
|
||||
box_inputs++;
|
||||
|
||||
std::get<0>(v) = box_inputs;
|
||||
std::get<1>(v) = box_outputs;
|
||||
std::get<2>(v) = box_module->attributes.at("\\abc9_box_id").as_int();
|
||||
std::get<2>(v) = box_module->attributes.at(ID::abc9_box_id).as_int();
|
||||
}
|
||||
|
||||
write_h_buffer(std::get<0>(v));
|
||||
|
@ -635,11 +635,11 @@ struct XAigerWriter
|
|||
const SigBit &d = i.first;
|
||||
const Cell *cell = i.second;
|
||||
|
||||
int mergeability = cell->attributes.at(ID(abc9_mergeability)).as_int();
|
||||
int mergeability = cell->attributes.at(ID::abc9_mergeability).as_int();
|
||||
log_assert(mergeability > 0);
|
||||
write_r_buffer(mergeability);
|
||||
|
||||
Const init = cell->attributes.at(ID(abc9_init), State::Sx);
|
||||
Const init = cell->attributes.at(ID::abc9_init, State::Sx);
|
||||
log_assert(GetSize(init) == 1);
|
||||
if (init == State::S1)
|
||||
write_s_buffer(1);
|
||||
|
|
|
@ -69,9 +69,9 @@ struct BlifDumper
|
|||
f(f), module(module), design(design), config(config), ct(design), sigmap(module)
|
||||
{
|
||||
for (Wire *wire : module->wires())
|
||||
if (wire->attributes.count("\\init")) {
|
||||
if (wire->attributes.count(ID::init)) {
|
||||
SigSpec initsig = sigmap(wire);
|
||||
Const initval = wire->attributes.at("\\init");
|
||||
Const initval = wire->attributes.at(ID::init);
|
||||
for (int i = 0; i < GetSize(initsig) && i < GetSize(initval); i++)
|
||||
switch (initval[i]) {
|
||||
case State::S0:
|
||||
|
@ -138,9 +138,9 @@ struct BlifDumper
|
|||
{
|
||||
if (!config->gates_mode)
|
||||
return "subckt";
|
||||
if (!design->modules_.count(RTLIL::escape_id(cell_type)))
|
||||
if (design->module(RTLIL::escape_id(cell_type)) == nullptr)
|
||||
return "gate";
|
||||
if (design->modules_.at(RTLIL::escape_id(cell_type))->get_blackbox_attribute())
|
||||
if (design->module(RTLIL::escape_id(cell_type))->get_blackbox_attribute())
|
||||
return "gate";
|
||||
return "subckt";
|
||||
}
|
||||
|
@ -148,7 +148,7 @@ struct BlifDumper
|
|||
void dump_params(const char *command, dict<IdString, Const> ¶ms)
|
||||
{
|
||||
for (auto ¶m : params) {
|
||||
f << stringf("%s %s ", command, RTLIL::id2cstr(param.first));
|
||||
f << stringf("%s %s ", command, log_id(param.first));
|
||||
if (param.second.flags & RTLIL::CONST_FLAG_STRING) {
|
||||
std::string str = param.second.decode_string();
|
||||
f << stringf("\"");
|
||||
|
@ -172,8 +172,7 @@ struct BlifDumper
|
|||
|
||||
std::map<int, RTLIL::Wire*> inputs, outputs;
|
||||
|
||||
for (auto &wire_it : module->wires_) {
|
||||
RTLIL::Wire *wire = wire_it.second;
|
||||
for (auto wire : module->wires()) {
|
||||
if (wire->port_input)
|
||||
inputs[wire->port_id] = wire;
|
||||
if (wire->port_output)
|
||||
|
@ -229,10 +228,8 @@ struct BlifDumper
|
|||
f << stringf(".names $undef\n");
|
||||
}
|
||||
|
||||
for (auto &cell_it : module->cells_)
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
RTLIL::Cell *cell = cell_it.second;
|
||||
|
||||
if (config->unbuf_types.count(cell->type)) {
|
||||
auto portnames = config->unbuf_types.at(cell->type);
|
||||
f << stringf(".names %s %s\n1 1\n",
|
||||
|
@ -240,142 +237,142 @@ struct BlifDumper
|
|||
continue;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_NOT_") {
|
||||
if (!config->icells_mode && cell->type == ID($_NOT_)) {
|
||||
f << stringf(".names %s %s\n0 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_AND_") {
|
||||
if (!config->icells_mode && cell->type == ID($_AND_)) {
|
||||
f << stringf(".names %s %s %s\n11 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_OR_") {
|
||||
if (!config->icells_mode && cell->type == ID($_OR_)) {
|
||||
f << stringf(".names %s %s %s\n1- 1\n-1 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_XOR_") {
|
||||
if (!config->icells_mode && cell->type == ID($_XOR_)) {
|
||||
f << stringf(".names %s %s %s\n10 1\n01 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_NAND_") {
|
||||
if (!config->icells_mode && cell->type == ID($_NAND_)) {
|
||||
f << stringf(".names %s %s %s\n0- 1\n-0 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_NOR_") {
|
||||
if (!config->icells_mode && cell->type == ID($_NOR_)) {
|
||||
f << stringf(".names %s %s %s\n00 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_XNOR_") {
|
||||
if (!config->icells_mode && cell->type == ID($_XNOR_)) {
|
||||
f << stringf(".names %s %s %s\n11 1\n00 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_ANDNOT_") {
|
||||
if (!config->icells_mode && cell->type == ID($_ANDNOT_)) {
|
||||
f << stringf(".names %s %s %s\n10 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_ORNOT_") {
|
||||
if (!config->icells_mode && cell->type == ID($_ORNOT_)) {
|
||||
f << stringf(".names %s %s %s\n1- 1\n-0 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_AOI3_") {
|
||||
if (!config->icells_mode && cell->type == ID($_AOI3_)) {
|
||||
f << stringf(".names %s %s %s %s\n-00 1\n0-0 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\C")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_OAI3_") {
|
||||
if (!config->icells_mode && cell->type == ID($_OAI3_)) {
|
||||
f << stringf(".names %s %s %s %s\n00- 1\n--0 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")), cstr(cell->getPort("\\C")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_AOI4_") {
|
||||
if (!config->icells_mode && cell->type == ID($_AOI4_)) {
|
||||
f << stringf(".names %s %s %s %s %s\n-0-0 1\n-00- 1\n0--0 1\n0-0- 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
|
||||
cstr(cell->getPort("\\C")), cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
|
||||
cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_OAI4_") {
|
||||
if (!config->icells_mode && cell->type == ID($_OAI4_)) {
|
||||
f << stringf(".names %s %s %s %s %s\n00-- 1\n--00 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
|
||||
cstr(cell->getPort("\\C")), cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
|
||||
cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_MUX_") {
|
||||
if (!config->icells_mode && cell->type == ID($_MUX_)) {
|
||||
f << stringf(".names %s %s %s %s\n1-0 1\n-11 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
|
||||
cstr(cell->getPort("\\S")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
|
||||
cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_NMUX_") {
|
||||
if (!config->icells_mode && cell->type == ID($_NMUX_)) {
|
||||
f << stringf(".names %s %s %s %s\n0-0 1\n-01 1\n",
|
||||
cstr(cell->getPort("\\A")), cstr(cell->getPort("\\B")),
|
||||
cstr(cell->getPort("\\S")), cstr(cell->getPort("\\Y")));
|
||||
cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)),
|
||||
cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_FF_") {
|
||||
f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
|
||||
cstr_init(cell->getPort("\\Q")));
|
||||
if (!config->icells_mode && cell->type == ID($_FF_)) {
|
||||
f << stringf(".latch %s %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
|
||||
cstr_init(cell->getPort(ID::Q)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_DFF_N_") {
|
||||
f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
|
||||
cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
|
||||
if (!config->icells_mode && cell->type == ID($_DFF_N_)) {
|
||||
f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
|
||||
cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_DFF_P_") {
|
||||
f << stringf(".latch %s %s re %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
|
||||
cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q")));
|
||||
if (!config->icells_mode && cell->type == ID($_DFF_P_)) {
|
||||
f << stringf(".latch %s %s re %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
|
||||
cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_DLATCH_N_") {
|
||||
f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
|
||||
cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
|
||||
if (!config->icells_mode && cell->type == ID($_DLATCH_N_)) {
|
||||
f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
|
||||
cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$_DLATCH_P_") {
|
||||
f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")),
|
||||
cstr(cell->getPort("\\E")), cstr_init(cell->getPort("\\Q")));
|
||||
if (!config->icells_mode && cell->type == ID($_DLATCH_P_)) {
|
||||
f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)),
|
||||
cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q)));
|
||||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$lut") {
|
||||
if (!config->icells_mode && cell->type == ID($lut)) {
|
||||
f << stringf(".names");
|
||||
auto &inputs = cell->getPort("\\A");
|
||||
auto width = cell->parameters.at("\\WIDTH").as_int();
|
||||
auto &inputs = cell->getPort(ID::A);
|
||||
auto width = cell->parameters.at(ID::WIDTH).as_int();
|
||||
log_assert(inputs.size() == width);
|
||||
for (int i = width-1; i >= 0; i--)
|
||||
f << stringf(" %s", cstr(inputs.extract(i, 1)));
|
||||
auto &output = cell->getPort("\\Y");
|
||||
auto &output = cell->getPort(ID::Y);
|
||||
log_assert(output.size() == 1);
|
||||
f << stringf(" %s", cstr(output));
|
||||
f << stringf("\n");
|
||||
RTLIL::SigSpec mask = cell->parameters.at("\\LUT");
|
||||
RTLIL::SigSpec mask = cell->parameters.at(ID::LUT);
|
||||
for (int i = 0; i < (1 << width); i++)
|
||||
if (mask[i] == State::S1) {
|
||||
for (int j = width-1; j >= 0; j--) {
|
||||
|
@ -386,18 +383,18 @@ struct BlifDumper
|
|||
goto internal_cell;
|
||||
}
|
||||
|
||||
if (!config->icells_mode && cell->type == "$sop") {
|
||||
if (!config->icells_mode && cell->type == ID($sop)) {
|
||||
f << stringf(".names");
|
||||
auto &inputs = cell->getPort("\\A");
|
||||
auto width = cell->parameters.at("\\WIDTH").as_int();
|
||||
auto depth = cell->parameters.at("\\DEPTH").as_int();
|
||||
vector<State> table = cell->parameters.at("\\TABLE").bits;
|
||||
auto &inputs = cell->getPort(ID::A);
|
||||
auto width = cell->parameters.at(ID::WIDTH).as_int();
|
||||
auto depth = cell->parameters.at(ID::DEPTH).as_int();
|
||||
vector<State> table = cell->parameters.at(ID::TABLE).bits;
|
||||
while (GetSize(table) < 2*width*depth)
|
||||
table.push_back(State::S0);
|
||||
log_assert(inputs.size() == width);
|
||||
for (int i = 0; i < width; i++)
|
||||
f << stringf(" %s", cstr(inputs.extract(i, 1)));
|
||||
auto &output = cell->getPort("\\Y");
|
||||
auto &output = cell->getPort(ID::Y);
|
||||
log_assert(output.size() == 1);
|
||||
f << stringf(" %s", cstr(output));
|
||||
f << stringf("\n");
|
||||
|
@ -649,25 +646,24 @@ struct BlifBackend : public Backend {
|
|||
extra_args(f, filename, args, argidx);
|
||||
|
||||
if (top_module_name.empty())
|
||||
for (auto & mod_it:design->modules_)
|
||||
if (mod_it.second->get_bool_attribute("\\top"))
|
||||
top_module_name = mod_it.first.str();
|
||||
for (auto module : design->modules())
|
||||
if (module->get_bool_attribute(ID::top))
|
||||
top_module_name = module->name.str();
|
||||
|
||||
*f << stringf("# Generated by %s\n", yosys_version_str);
|
||||
|
||||
std::vector<RTLIL::Module*> mod_list;
|
||||
|
||||
design->sort();
|
||||
for (auto module_it : design->modules_)
|
||||
for (auto module : design->modules())
|
||||
{
|
||||
RTLIL::Module *module = module_it.second;
|
||||
if (module->get_blackbox_attribute() && !config.blackbox_mode)
|
||||
continue;
|
||||
|
||||
if (module->processes.size() != 0)
|
||||
log_error("Found unmapped processes in module %s: unmapped processes are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
|
||||
log_error("Found unmapped processes in module %s: unmapped processes are not supported in BLIF backend!\n", log_id(module->name));
|
||||
if (module->memories.size() != 0)
|
||||
log_error("Found unmapped memories in module %s: unmapped memories are not supported in BLIF backend!\n", RTLIL::id2cstr(module->name));
|
||||
log_error("Found unmapped memories in module %s: unmapped memories are not supported in BLIF backend!\n", log_id(module->name));
|
||||
|
||||
if (module->name == RTLIL::escape_id(top_module_name)) {
|
||||
BlifDumper::dump(*f, module, design, config);
|
||||
|
|
|
@ -39,6 +39,7 @@ struct BtorWorker
|
|||
RTLIL::Module *module;
|
||||
bool verbose;
|
||||
bool single_bad;
|
||||
bool cover_mode;
|
||||
|
||||
int next_nid = 1;
|
||||
int initstate_nid = -1;
|
||||
|
@ -71,7 +72,11 @@ struct BtorWorker
|
|||
vector<int> bad_properties;
|
||||
dict<SigBit, bool> initbits;
|
||||
pool<Wire*> statewires;
|
||||
string indent;
|
||||
pool<string> srcsymbols;
|
||||
|
||||
string indent, info_filename;
|
||||
vector<string> info_lines;
|
||||
dict<int, int> info_clocks;
|
||||
|
||||
void btorf(const char *fmt, ...)
|
||||
{
|
||||
|
@ -81,6 +86,40 @@ struct BtorWorker
|
|||
va_end(ap);
|
||||
}
|
||||
|
||||
void infof(const char *fmt, ...)
|
||||
{
|
||||
va_list ap;
|
||||
va_start(ap, fmt);
|
||||
info_lines.push_back(vstringf(fmt, ap));
|
||||
va_end(ap);
|
||||
}
|
||||
|
||||
template<typename T>
|
||||
string getinfo(T *obj, bool srcsym = false)
|
||||
{
|
||||
string infostr = log_id(obj);
|
||||
if (obj->attributes.count(ID::src)) {
|
||||
string src = obj->attributes.at(ID::src).decode_string().c_str();
|
||||
if (srcsym && infostr[0] == '$') {
|
||||
std::replace(src.begin(), src.end(), ' ', '_');
|
||||
if (srcsymbols.count(src) || module->count_id("\\" + src)) {
|
||||
for (int i = 1;; i++) {
|
||||
string s = stringf("%s-%d", src.c_str(), i);
|
||||
if (!srcsymbols.count(s) && !module->count_id("\\" + s)) {
|
||||
src = s;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
srcsymbols.insert(src);
|
||||
infostr = src;
|
||||
} else {
|
||||
infostr += " ; " + src;
|
||||
}
|
||||
}
|
||||
return infostr;
|
||||
}
|
||||
|
||||
void btorf_push(const string &id)
|
||||
{
|
||||
if (verbose) {
|
||||
|
@ -144,40 +183,40 @@ struct BtorWorker
|
|||
cell_recursion_guard.insert(cell);
|
||||
btorf_push(log_id(cell));
|
||||
|
||||
if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
|
||||
"$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
|
||||
if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor), ID($shl), ID($sshl), ID($shr), ID($sshr), ID($shift), ID($shiftx),
|
||||
ID($concat), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_)))
|
||||
{
|
||||
string btor_op;
|
||||
if (cell->type == "$add") btor_op = "add";
|
||||
if (cell->type == "$sub") btor_op = "sub";
|
||||
if (cell->type == "$mul") btor_op = "mul";
|
||||
if (cell->type.in("$shl", "$sshl")) btor_op = "sll";
|
||||
if (cell->type == "$shr") btor_op = "srl";
|
||||
if (cell->type == "$sshr") btor_op = "sra";
|
||||
if (cell->type.in("$shift", "$shiftx")) btor_op = "shift";
|
||||
if (cell->type.in("$and", "$_AND_")) btor_op = "and";
|
||||
if (cell->type.in("$or", "$_OR_")) btor_op = "or";
|
||||
if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor";
|
||||
if (cell->type == "$concat") btor_op = "concat";
|
||||
if (cell->type == "$_NAND_") btor_op = "nand";
|
||||
if (cell->type == "$_NOR_") btor_op = "nor";
|
||||
if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor";
|
||||
if (cell->type == ID($add)) btor_op = "add";
|
||||
if (cell->type == ID($sub)) btor_op = "sub";
|
||||
if (cell->type == ID($mul)) btor_op = "mul";
|
||||
if (cell->type.in(ID($shl), ID($sshl))) btor_op = "sll";
|
||||
if (cell->type == ID($shr)) btor_op = "srl";
|
||||
if (cell->type == ID($sshr)) btor_op = "sra";
|
||||
if (cell->type.in(ID($shift), ID($shiftx))) btor_op = "shift";
|
||||
if (cell->type.in(ID($and), ID($_AND_))) btor_op = "and";
|
||||
if (cell->type.in(ID($or), ID($_OR_))) btor_op = "or";
|
||||
if (cell->type.in(ID($xor), ID($_XOR_))) btor_op = "xor";
|
||||
if (cell->type == ID($concat)) btor_op = "concat";
|
||||
if (cell->type == ID($_NAND_)) btor_op = "nand";
|
||||
if (cell->type == ID($_NOR_)) btor_op = "nor";
|
||||
if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor";
|
||||
log_assert(!btor_op.empty());
|
||||
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
width = std::max(width, GetSize(cell->getPort("\\A")));
|
||||
width = std::max(width, GetSize(cell->getPort("\\B")));
|
||||
int width = GetSize(cell->getPort(ID::Y));
|
||||
width = std::max(width, GetSize(cell->getPort(ID::A)));
|
||||
width = std::max(width, GetSize(cell->getPort(ID::B)));
|
||||
|
||||
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
|
||||
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
|
||||
bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
|
||||
bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
|
||||
|
||||
if (btor_op == "shift" && !b_signed)
|
||||
btor_op = "srl";
|
||||
|
||||
if (cell->type.in("$shl", "$sshl", "$shr", "$sshr"))
|
||||
if (cell->type.in(ID($shl), ID($sshl), ID($shr), ID($sshr)))
|
||||
b_signed = false;
|
||||
|
||||
if (cell->type == "$sshr" && !a_signed)
|
||||
if (cell->type == ID($sshr) && !a_signed)
|
||||
btor_op = "srl";
|
||||
|
||||
int sid = get_bv_sid(width);
|
||||
|
@ -185,8 +224,8 @@ struct BtorWorker
|
|||
|
||||
if (btor_op == "shift")
|
||||
{
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"), width, false);
|
||||
int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A), width, false);
|
||||
int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
|
||||
|
||||
int nid_r = next_nid++;
|
||||
btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b);
|
||||
|
@ -203,18 +242,18 @@ struct BtorWorker
|
|||
btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero);
|
||||
|
||||
nid = next_nid++;
|
||||
btorf("%d ite %d %d %d %d\n", nid, sid, nid_b_ltz, nid_l, nid_r);
|
||||
btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_b_ltz, nid_l, nid_r, getinfo(cell).c_str());
|
||||
}
|
||||
else
|
||||
{
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
|
||||
int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
|
||||
int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
|
||||
|
||||
nid = next_nid++;
|
||||
btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
|
||||
btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
if (GetSize(sig) < width) {
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
|
@ -227,28 +266,28 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$div", "$mod"))
|
||||
if (cell->type.in(ID($div), ID($mod)))
|
||||
{
|
||||
string btor_op;
|
||||
if (cell->type == "$div") btor_op = "div";
|
||||
if (cell->type == "$mod") btor_op = "rem";
|
||||
if (cell->type == ID($div)) btor_op = "div";
|
||||
if (cell->type == ID($mod)) btor_op = "rem";
|
||||
log_assert(!btor_op.empty());
|
||||
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
width = std::max(width, GetSize(cell->getPort("\\A")));
|
||||
width = std::max(width, GetSize(cell->getPort("\\B")));
|
||||
int width = GetSize(cell->getPort(ID::Y));
|
||||
width = std::max(width, GetSize(cell->getPort(ID::A)));
|
||||
width = std::max(width, GetSize(cell->getPort(ID::B)));
|
||||
|
||||
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
|
||||
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
|
||||
bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
|
||||
bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
|
||||
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
|
||||
int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
|
||||
int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
|
||||
|
||||
int sid = get_bv_sid(width);
|
||||
int nid = next_nid++;
|
||||
btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
|
||||
btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
if (GetSize(sig) < width) {
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
|
@ -261,120 +300,120 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
|
||||
if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
|
||||
{
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"));
|
||||
int nid_b = get_sig_nid(cell->getPort("\\B"));
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
int nid_b = get_sig_nid(cell->getPort(ID::B));
|
||||
|
||||
int nid1 = next_nid++;
|
||||
int nid2 = next_nid++;
|
||||
|
||||
if (cell->type == "$_ANDNOT_") {
|
||||
if (cell->type == ID($_ANDNOT_)) {
|
||||
btorf("%d not %d %d\n", nid1, sid, nid_b);
|
||||
btorf("%d and %d %d %d\n", nid2, sid, nid_a, nid1);
|
||||
btorf("%d and %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
if (cell->type == "$_ORNOT_") {
|
||||
if (cell->type == ID($_ORNOT_)) {
|
||||
btorf("%d not %d %d\n", nid1, sid, nid_b);
|
||||
btorf("%d or %d %d %d\n", nid2, sid, nid_a, nid1);
|
||||
btorf("%d or %d %d %d %s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
add_nid_sig(nid2, sig);
|
||||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_OAI3_", "$_AOI3_"))
|
||||
if (cell->type.in(ID($_OAI3_), ID($_AOI3_)))
|
||||
{
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"));
|
||||
int nid_b = get_sig_nid(cell->getPort("\\B"));
|
||||
int nid_c = get_sig_nid(cell->getPort("\\C"));
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
int nid_b = get_sig_nid(cell->getPort(ID::B));
|
||||
int nid_c = get_sig_nid(cell->getPort(ID::C));
|
||||
|
||||
int nid1 = next_nid++;
|
||||
int nid2 = next_nid++;
|
||||
int nid3 = next_nid++;
|
||||
|
||||
if (cell->type == "$_OAI3_") {
|
||||
if (cell->type == ID($_OAI3_)) {
|
||||
btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
|
||||
btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c);
|
||||
btorf("%d not %d %d\n", nid3, sid, nid2);
|
||||
btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
if (cell->type == "$_AOI3_") {
|
||||
if (cell->type == ID($_AOI3_)) {
|
||||
btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
|
||||
btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c);
|
||||
btorf("%d not %d %d\n", nid3, sid, nid2);
|
||||
btorf("%d not %d %d %s\n", nid3, sid, nid2, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
add_nid_sig(nid3, sig);
|
||||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_OAI4_", "$_AOI4_"))
|
||||
if (cell->type.in(ID($_OAI4_), ID($_AOI4_)))
|
||||
{
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"));
|
||||
int nid_b = get_sig_nid(cell->getPort("\\B"));
|
||||
int nid_c = get_sig_nid(cell->getPort("\\C"));
|
||||
int nid_d = get_sig_nid(cell->getPort("\\D"));
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
int nid_b = get_sig_nid(cell->getPort(ID::B));
|
||||
int nid_c = get_sig_nid(cell->getPort(ID::C));
|
||||
int nid_d = get_sig_nid(cell->getPort(ID::D));
|
||||
|
||||
int nid1 = next_nid++;
|
||||
int nid2 = next_nid++;
|
||||
int nid3 = next_nid++;
|
||||
int nid4 = next_nid++;
|
||||
|
||||
if (cell->type == "$_OAI4_") {
|
||||
if (cell->type == ID($_OAI4_)) {
|
||||
btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b);
|
||||
btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d);
|
||||
btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2);
|
||||
btorf("%d not %d %d\n", nid4, sid, nid3);
|
||||
btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
if (cell->type == "$_AOI4_") {
|
||||
if (cell->type == ID($_AOI4_)) {
|
||||
btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b);
|
||||
btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d);
|
||||
btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2);
|
||||
btorf("%d not %d %d\n", nid4, sid, nid3);
|
||||
btorf("%d not %d %d %s\n", nid4, sid, nid3, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
add_nid_sig(nid4, sig);
|
||||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$lt", "$le", "$eq", "$eqx", "$ne", "$nex", "$ge", "$gt"))
|
||||
if (cell->type.in(ID($lt), ID($le), ID($eq), ID($eqx), ID($ne), ID($nex), ID($ge), ID($gt)))
|
||||
{
|
||||
string btor_op;
|
||||
if (cell->type == "$lt") btor_op = "lt";
|
||||
if (cell->type == "$le") btor_op = "lte";
|
||||
if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
|
||||
if (cell->type.in("$ne", "$nex")) btor_op = "neq";
|
||||
if (cell->type == "$ge") btor_op = "gte";
|
||||
if (cell->type == "$gt") btor_op = "gt";
|
||||
if (cell->type == ID($lt)) btor_op = "lt";
|
||||
if (cell->type == ID($le)) btor_op = "lte";
|
||||
if (cell->type.in(ID($eq), ID($eqx))) btor_op = "eq";
|
||||
if (cell->type.in(ID($ne), ID($nex))) btor_op = "neq";
|
||||
if (cell->type == ID($ge)) btor_op = "gte";
|
||||
if (cell->type == ID($gt)) btor_op = "gt";
|
||||
log_assert(!btor_op.empty());
|
||||
|
||||
int width = 1;
|
||||
width = std::max(width, GetSize(cell->getPort("\\A")));
|
||||
width = std::max(width, GetSize(cell->getPort("\\B")));
|
||||
width = std::max(width, GetSize(cell->getPort(ID::A)));
|
||||
width = std::max(width, GetSize(cell->getPort(ID::B)));
|
||||
|
||||
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
|
||||
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
|
||||
bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
|
||||
bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false;
|
||||
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
|
||||
int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
|
||||
int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed);
|
||||
|
||||
int nid = next_nid++;
|
||||
if (cell->type.in("$lt", "$le", "$ge", "$gt")) {
|
||||
btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
|
||||
if (cell->type.in(ID($lt), ID($le), ID($ge), ID($gt))) {
|
||||
btorf("%d %c%s %d %d %d %s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
|
||||
} else {
|
||||
btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
|
||||
btorf("%d %s %d %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
if (GetSize(sig) > 1) {
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
|
@ -387,25 +426,24 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$not", "$neg", "$_NOT_"))
|
||||
if (cell->type.in(ID($not), ID($neg), ID($_NOT_)))
|
||||
{
|
||||
string btor_op;
|
||||
if (cell->type.in("$not", "$_NOT_")) btor_op = "not";
|
||||
if (cell->type == "$neg") btor_op = "neg";
|
||||
if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
|
||||
if (cell->type == ID($neg)) btor_op = "neg";
|
||||
log_assert(!btor_op.empty());
|
||||
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
width = std::max(width, GetSize(cell->getPort("\\A")));
|
||||
int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
|
||||
|
||||
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
|
||||
bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
|
||||
|
||||
int sid = get_bv_sid(width);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
|
||||
|
||||
int nid = next_nid++;
|
||||
btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
|
||||
btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
if (GetSize(sig) < width) {
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
|
@ -418,25 +456,25 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$logic_and", "$logic_or", "$logic_not"))
|
||||
if (cell->type.in(ID($logic_and), ID($logic_or), ID($logic_not)))
|
||||
{
|
||||
string btor_op;
|
||||
if (cell->type == "$logic_and") btor_op = "and";
|
||||
if (cell->type == "$logic_or") btor_op = "or";
|
||||
if (cell->type == "$logic_not") btor_op = "not";
|
||||
if (cell->type == ID($logic_and)) btor_op = "and";
|
||||
if (cell->type == ID($logic_or)) btor_op = "or";
|
||||
if (cell->type == ID($logic_not)) btor_op = "not";
|
||||
log_assert(!btor_op.empty());
|
||||
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"));
|
||||
int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort("\\B")) : 0;
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort(ID::B)) : 0;
|
||||
|
||||
if (GetSize(cell->getPort("\\A")) > 1) {
|
||||
if (GetSize(cell->getPort(ID::A)) > 1) {
|
||||
int nid_red_a = next_nid++;
|
||||
btorf("%d redor %d %d\n", nid_red_a, sid, nid_a);
|
||||
nid_a = nid_red_a;
|
||||
}
|
||||
|
||||
if (btor_op != "not" && GetSize(cell->getPort("\\B")) > 1) {
|
||||
if (btor_op != "not" && GetSize(cell->getPort(ID::B)) > 1) {
|
||||
int nid_red_b = next_nid++;
|
||||
btorf("%d redor %d %d\n", nid_red_b, sid, nid_b);
|
||||
nid_b = nid_red_b;
|
||||
|
@ -444,11 +482,11 @@ struct BtorWorker
|
|||
|
||||
int nid = next_nid++;
|
||||
if (btor_op != "not")
|
||||
btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
|
||||
btorf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str());
|
||||
else
|
||||
btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
|
||||
btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
if (GetSize(sig) > 1) {
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
|
@ -462,27 +500,29 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool", "$reduce_xor", "$reduce_xnor"))
|
||||
if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool), ID($reduce_xor), ID($reduce_xnor)))
|
||||
{
|
||||
string btor_op;
|
||||
if (cell->type == "$reduce_and") btor_op = "redand";
|
||||
if (cell->type.in("$reduce_or", "$reduce_bool")) btor_op = "redor";
|
||||
if (cell->type.in("$reduce_xor", "$reduce_xnor")) btor_op = "redxor";
|
||||
if (cell->type == ID($reduce_and)) btor_op = "redand";
|
||||
if (cell->type.in(ID($reduce_or), ID($reduce_bool))) btor_op = "redor";
|
||||
if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) btor_op = "redxor";
|
||||
log_assert(!btor_op.empty());
|
||||
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"));
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
|
||||
int nid = next_nid++;
|
||||
btorf("%d %s %d %d\n", nid, btor_op.c_str(), sid, nid_a);
|
||||
|
||||
if (cell->type == "$reduce_xnor") {
|
||||
if (cell->type == ID($reduce_xnor)) {
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
|
||||
btorf("%d not %d %d %d\n", nid2, sid, nid);
|
||||
nid = nid2;
|
||||
} else {
|
||||
btorf("%d %s %d %d %s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
if (GetSize(sig) > 1) {
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
|
@ -496,12 +536,12 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$mux", "$_MUX_", "$_NMUX_"))
|
||||
if (cell->type.in(ID($mux), ID($_MUX_), ID($_NMUX_)))
|
||||
{
|
||||
SigSpec sig_a = sigmap(cell->getPort("\\A"));
|
||||
SigSpec sig_b = sigmap(cell->getPort("\\B"));
|
||||
SigSpec sig_s = sigmap(cell->getPort("\\S"));
|
||||
SigSpec sig_y = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig_a = sigmap(cell->getPort(ID::A));
|
||||
SigSpec sig_b = sigmap(cell->getPort(ID::B));
|
||||
SigSpec sig_s = sigmap(cell->getPort(ID::S));
|
||||
SigSpec sig_y = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
int nid_a = get_sig_nid(sig_a);
|
||||
int nid_b = get_sig_nid(sig_b);
|
||||
|
@ -509,24 +549,26 @@ struct BtorWorker
|
|||
|
||||
int sid = get_bv_sid(GetSize(sig_y));
|
||||
int nid = next_nid++;
|
||||
btorf("%d ite %d %d %d %d\n", nid, sid, nid_s, nid_b, nid_a);
|
||||
|
||||
if (cell->type == "$_NMUX_") {
|
||||
if (cell->type == ID($_NMUX_)) {
|
||||
int tmp = nid;
|
||||
nid = next_nid++;
|
||||
btorf("%d not %d %d\n", nid, sid, tmp);
|
||||
btorf("%d ite %d %d %d %d\n", tmp, sid, nid_s, nid_b, nid_a);
|
||||
btorf("%d not %d %d %s\n", nid, sid, tmp, getinfo(cell).c_str());
|
||||
} else {
|
||||
btorf("%d ite %d %d %d %d %s\n", nid, sid, nid_s, nid_b, nid_a, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
add_nid_sig(nid, sig_y);
|
||||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type == "$pmux")
|
||||
if (cell->type == ID($pmux))
|
||||
{
|
||||
SigSpec sig_a = sigmap(cell->getPort("\\A"));
|
||||
SigSpec sig_b = sigmap(cell->getPort("\\B"));
|
||||
SigSpec sig_s = sigmap(cell->getPort("\\S"));
|
||||
SigSpec sig_y = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig_a = sigmap(cell->getPort(ID::A));
|
||||
SigSpec sig_b = sigmap(cell->getPort(ID::B));
|
||||
SigSpec sig_s = sigmap(cell->getPort(ID::S));
|
||||
SigSpec sig_y = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
int width = GetSize(sig_a);
|
||||
int sid = get_bv_sid(width);
|
||||
|
@ -536,7 +578,10 @@ struct BtorWorker
|
|||
int nid_b = get_sig_nid(sig_b.extract(i*width, width));
|
||||
int nid_s = get_sig_nid(sig_s.extract(i));
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
|
||||
if (i == GetSize(sig_s)-1)
|
||||
btorf("%d ite %d %d %d %d %s\n", nid2, sid, nid_s, nid_b, nid, getinfo(cell).c_str());
|
||||
else
|
||||
btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid);
|
||||
nid = nid2;
|
||||
}
|
||||
|
||||
|
@ -544,10 +589,25 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$dff", "$ff", "$_DFF_P_", "$_DFF_N", "$_FF_"))
|
||||
if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
|
||||
{
|
||||
SigSpec sig_d = sigmap(cell->getPort("\\D"));
|
||||
SigSpec sig_q = sigmap(cell->getPort("\\Q"));
|
||||
SigSpec sig_d = sigmap(cell->getPort(ID::D));
|
||||
SigSpec sig_q = sigmap(cell->getPort(ID::Q));
|
||||
|
||||
if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
|
||||
{
|
||||
SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C));
|
||||
int nid = get_sig_nid(sig_c);
|
||||
bool negedge = false;
|
||||
|
||||
if (cell->type == ID($_DFF_N_))
|
||||
negedge = true;
|
||||
|
||||
if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool())
|
||||
negedge = true;
|
||||
|
||||
info_clocks[nid] |= negedge ? 2 : 1;
|
||||
}
|
||||
|
||||
IdString symbol;
|
||||
|
||||
|
@ -591,16 +651,16 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type.in("$anyconst", "$anyseq"))
|
||||
if (cell->type.in(ID($anyconst), ID($anyseq)))
|
||||
{
|
||||
SigSpec sig_y = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig_y = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
int sid = get_bv_sid(GetSize(sig_y));
|
||||
int nid = next_nid++;
|
||||
|
||||
btorf("%d state %d\n", nid, sid);
|
||||
|
||||
if (cell->type == "$anyconst") {
|
||||
if (cell->type == ID($anyconst)) {
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
|
||||
}
|
||||
|
@ -609,9 +669,9 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type == "$initstate")
|
||||
if (cell->type == ID($initstate))
|
||||
{
|
||||
SigSpec sig_y = sigmap(cell->getPort("\\Y"));
|
||||
SigSpec sig_y = sigmap(cell->getPort(ID::Y));
|
||||
|
||||
if (initstate_nid < 0)
|
||||
{
|
||||
|
@ -628,16 +688,16 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type == "$mem")
|
||||
if (cell->type == ID($mem))
|
||||
{
|
||||
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();
|
||||
int abits = cell->getParam(ID::ABITS).as_int();
|
||||
int width = cell->getParam(ID::WIDTH).as_int();
|
||||
int nwords = cell->getParam(ID::SIZE).as_int();
|
||||
int rdports = cell->getParam(ID::RD_PORTS).as_int();
|
||||
int wrports = cell->getParam(ID::WR_PORTS).as_int();
|
||||
|
||||
Const wr_clk_en = cell->getParam("\\WR_CLK_ENABLE");
|
||||
Const rd_clk_en = cell->getParam("\\RD_CLK_ENABLE");
|
||||
Const wr_clk_en = cell->getParam(ID::WR_CLK_ENABLE);
|
||||
Const rd_clk_en = cell->getParam(ID::RD_CLK_ENABLE);
|
||||
|
||||
bool asyncwr = wr_clk_en.is_fully_zero();
|
||||
|
||||
|
@ -649,18 +709,18 @@ struct BtorWorker
|
|||
log_error("Memory %s.%s has sync read ports.\n",
|
||||
log_id(module), log_id(cell));
|
||||
|
||||
SigSpec sig_rd_addr = sigmap(cell->getPort("\\RD_ADDR"));
|
||||
SigSpec sig_rd_data = sigmap(cell->getPort("\\RD_DATA"));
|
||||
SigSpec sig_rd_addr = sigmap(cell->getPort(ID::RD_ADDR));
|
||||
SigSpec sig_rd_data = sigmap(cell->getPort(ID::RD_DATA));
|
||||
|
||||
SigSpec sig_wr_addr = sigmap(cell->getPort("\\WR_ADDR"));
|
||||
SigSpec sig_wr_data = sigmap(cell->getPort("\\WR_DATA"));
|
||||
SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN"));
|
||||
SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR));
|
||||
SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA));
|
||||
SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN));
|
||||
|
||||
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");
|
||||
Const initdata = cell->getParam(ID::INIT);
|
||||
initdata.exts(nwords*width);
|
||||
int nid_init_val = -1;
|
||||
|
||||
|
@ -983,15 +1043,18 @@ struct BtorWorker
|
|||
return nid;
|
||||
}
|
||||
|
||||
BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad) :
|
||||
f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad)
|
||||
BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, string info_filename) :
|
||||
f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), info_filename(info_filename)
|
||||
{
|
||||
if (!info_filename.empty())
|
||||
infof("name %s\n", log_id(module));
|
||||
|
||||
btorf_push("inputs");
|
||||
|
||||
for (auto wire : module->wires())
|
||||
{
|
||||
if (wire->attributes.count("\\init")) {
|
||||
Const attrval = wire->attributes.at("\\init");
|
||||
if (wire->attributes.count(ID::init)) {
|
||||
Const attrval = wire->attributes.at(ID::init);
|
||||
for (int i = 0; i < GetSize(wire) && i < GetSize(attrval); i++)
|
||||
if (attrval[i] == State::S0 || attrval[i] == State::S1)
|
||||
initbits[sigmap(SigBit(wire, i))] = (attrval[i] == State::S1);
|
||||
|
@ -1004,7 +1067,7 @@ struct BtorWorker
|
|||
int sid = get_bv_sid(GetSize(sig));
|
||||
int nid = next_nid++;
|
||||
|
||||
btorf("%d input %d %s\n", nid, sid, log_id(wire));
|
||||
btorf("%d input %d %s\n", nid, sid, getinfo(wire).c_str());
|
||||
add_nid_sig(nid, sig);
|
||||
}
|
||||
|
||||
|
@ -1028,20 +1091,20 @@ struct BtorWorker
|
|||
btorf_push(stringf("output %s", log_id(wire)));
|
||||
|
||||
int nid = get_sig_nid(wire);
|
||||
btorf("%d output %d %s\n", next_nid++, nid, log_id(wire));
|
||||
btorf("%d output %d %s\n", next_nid++, nid, getinfo(wire).c_str());
|
||||
|
||||
btorf_pop(stringf("output %s", log_id(wire)));
|
||||
}
|
||||
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
if (cell->type == "$assume")
|
||||
if (cell->type == ID($assume))
|
||||
{
|
||||
btorf_push(log_id(cell));
|
||||
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"));
|
||||
int nid_en = get_sig_nid(cell->getPort("\\EN"));
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
int nid_en = get_sig_nid(cell->getPort(ID::EN));
|
||||
int nid_not_en = next_nid++;
|
||||
int nid_a_or_not_en = next_nid++;
|
||||
int nid = next_nid++;
|
||||
|
@ -1053,29 +1116,49 @@ struct BtorWorker
|
|||
btorf_pop(log_id(cell));
|
||||
}
|
||||
|
||||
if (cell->type == "$assert")
|
||||
if (cell->type == ID($assert))
|
||||
{
|
||||
btorf_push(log_id(cell));
|
||||
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort("\\A"));
|
||||
int nid_en = get_sig_nid(cell->getPort("\\EN"));
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
int nid_en = get_sig_nid(cell->getPort(ID::EN));
|
||||
int nid_not_a = next_nid++;
|
||||
int nid_en_and_not_a = next_nid++;
|
||||
|
||||
btorf("%d not %d %d\n", nid_not_a, sid, nid_a);
|
||||
btorf("%d and %d %d %d\n", nid_en_and_not_a, sid, nid_en, nid_not_a);
|
||||
|
||||
if (single_bad) {
|
||||
if (single_bad && !cover_mode) {
|
||||
bad_properties.push_back(nid_en_and_not_a);
|
||||
} else {
|
||||
int nid = next_nid++;
|
||||
string infostr = log_id(cell);
|
||||
if (infostr[0] == '$' && cell->attributes.count("\\src")) {
|
||||
infostr = cell->attributes.at("\\src").decode_string().c_str();
|
||||
std::replace(infostr.begin(), infostr.end(), ' ', '_');
|
||||
if (cover_mode) {
|
||||
infof("bad %d %s\n", nid_en_and_not_a, getinfo(cell, true).c_str());
|
||||
} else {
|
||||
int nid = next_nid++;
|
||||
btorf("%d bad %d %s\n", nid, nid_en_and_not_a, getinfo(cell, true).c_str());
|
||||
}
|
||||
btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str());
|
||||
}
|
||||
|
||||
btorf_pop(log_id(cell));
|
||||
}
|
||||
|
||||
if (cell->type == ID($cover) && cover_mode)
|
||||
{
|
||||
btorf_push(log_id(cell));
|
||||
|
||||
int sid = get_bv_sid(1);
|
||||
int nid_a = get_sig_nid(cell->getPort(ID::A));
|
||||
int nid_en = get_sig_nid(cell->getPort(ID::EN));
|
||||
int nid_en_and_a = next_nid++;
|
||||
|
||||
btorf("%d and %d %d %d\n", nid_en_and_a, sid, nid_en, nid_a);
|
||||
|
||||
if (single_bad) {
|
||||
bad_properties.push_back(nid_en_and_a);
|
||||
} else {
|
||||
int nid = next_nid++;
|
||||
btorf("%d bad %d %s\n", nid, nid_en_and_a, getinfo(cell, true).c_str());
|
||||
}
|
||||
|
||||
btorf_pop(log_id(cell));
|
||||
|
@ -1096,7 +1179,7 @@ struct BtorWorker
|
|||
continue;
|
||||
|
||||
int this_nid = next_nid++;
|
||||
btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, log_id(wire));
|
||||
btorf("%d uext %d %d %d %s\n", this_nid, sid, nid, 0, getinfo(wire).c_str());
|
||||
|
||||
btorf_pop(stringf("wire %s", log_id(wire)));
|
||||
continue;
|
||||
|
@ -1114,15 +1197,15 @@ struct BtorWorker
|
|||
|
||||
btorf_push(stringf("next %s", log_id(cell)));
|
||||
|
||||
if (cell->type == "$mem")
|
||||
if (cell->type == ID($mem))
|
||||
{
|
||||
int abits = cell->getParam("\\ABITS").as_int();
|
||||
int width = cell->getParam("\\WIDTH").as_int();
|
||||
int wrports = cell->getParam("\\WR_PORTS").as_int();
|
||||
int abits = cell->getParam(ID::ABITS).as_int();
|
||||
int width = cell->getParam(ID::WIDTH).as_int();
|
||||
int wrports = cell->getParam(ID::WR_PORTS).as_int();
|
||||
|
||||
SigSpec sig_wr_addr = sigmap(cell->getPort("\\WR_ADDR"));
|
||||
SigSpec sig_wr_data = sigmap(cell->getPort("\\WR_DATA"));
|
||||
SigSpec sig_wr_en = sigmap(cell->getPort("\\WR_EN"));
|
||||
SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR));
|
||||
SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA));
|
||||
SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN));
|
||||
|
||||
int data_sid = get_bv_sid(width);
|
||||
int bool_sid = get_bv_sid(1);
|
||||
|
@ -1167,14 +1250,14 @@ struct BtorWorker
|
|||
}
|
||||
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d next %d %d %d\n", nid2, sid, nid, nid_head);
|
||||
btorf("%d next %d %d %d %s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str());
|
||||
}
|
||||
else
|
||||
{
|
||||
SigSpec sig = sigmap(cell->getPort("\\D"));
|
||||
SigSpec sig = sigmap(cell->getPort(ID::D));
|
||||
int nid_q = get_sig_nid(sig);
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
btorf("%d next %d %d %d\n", next_nid++, sid, nid, nid_q);
|
||||
btorf("%d next %d %d %d %s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str());
|
||||
}
|
||||
|
||||
btorf_pop(stringf("next %s", log_id(cell)));
|
||||
|
@ -1210,6 +1293,35 @@ struct BtorWorker
|
|||
btorf("%d bad %d\n", nid, todo[cursor]);
|
||||
}
|
||||
}
|
||||
|
||||
if (!info_filename.empty())
|
||||
{
|
||||
for (auto &it : info_clocks)
|
||||
{
|
||||
switch (it.second)
|
||||
{
|
||||
case 1:
|
||||
infof("posedge %d\n", it.first);
|
||||
break;
|
||||
case 2:
|
||||
infof("negedge %d\n", it.first);
|
||||
break;
|
||||
case 3:
|
||||
infof("event %d\n", it.first);
|
||||
break;
|
||||
default:
|
||||
log_abort();
|
||||
}
|
||||
}
|
||||
|
||||
std::ofstream f;
|
||||
f.open(info_filename.c_str(), std::ofstream::trunc);
|
||||
if (f.fail())
|
||||
log_error("Can't open file `%s' for writing: %s\n", info_filename.c_str(), strerror(errno));
|
||||
for (auto &it : info_lines)
|
||||
f << it;
|
||||
f.close();
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -1229,10 +1341,17 @@ struct BtorBackend : public Backend {
|
|||
log(" -s\n");
|
||||
log(" Output only a single bad property for all asserts\n");
|
||||
log("\n");
|
||||
log(" -c\n");
|
||||
log(" Output cover properties using 'bad' statements instead of asserts\n");
|
||||
log("\n");
|
||||
log(" -i <filename>\n");
|
||||
log(" Create additional info file with auxiliary information\n");
|
||||
log("\n");
|
||||
}
|
||||
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
|
||||
{
|
||||
bool verbose = false, single_bad = false;
|
||||
bool verbose = false, single_bad = false, cover_mode = false;
|
||||
string info_filename;
|
||||
|
||||
log_header(design, "Executing BTOR backend.\n");
|
||||
|
||||
|
@ -1247,6 +1366,14 @@ struct BtorBackend : public Backend {
|
|||
single_bad = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-c") {
|
||||
cover_mode = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-i" && argidx+1 < args.size()) {
|
||||
info_filename = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
extra_args(f, filename, args, argidx);
|
||||
|
@ -1259,7 +1386,7 @@ struct BtorBackend : public Backend {
|
|||
*f << stringf("; BTOR description generated by %s for module %s.\n",
|
||||
yosys_version_str, log_id(topmod));
|
||||
|
||||
BtorWorker(*f, topmod, verbose, single_bad);
|
||||
BtorWorker(*f, topmod, verbose, single_bad, cover_mode, info_filename);
|
||||
|
||||
*f << stringf("; end of yosys output\n");
|
||||
}
|
||||
|
|
|
@ -171,13 +171,12 @@ struct EdifBackend : public Backend {
|
|||
extra_args(f, filename, args, argidx);
|
||||
|
||||
if (top_module_name.empty())
|
||||
for (auto & mod_it:design->modules_)
|
||||
if (mod_it.second->get_bool_attribute("\\top"))
|
||||
top_module_name = mod_it.first.str();
|
||||
for (auto module : design->modules())
|
||||
if (module->get_bool_attribute(ID::top))
|
||||
top_module_name = module->name.str();
|
||||
|
||||
for (auto module_it : design->modules_)
|
||||
for (auto module : design->modules())
|
||||
{
|
||||
RTLIL::Module *module = module_it.second;
|
||||
if (module->get_blackbox_attribute())
|
||||
continue;
|
||||
|
||||
|
@ -185,14 +184,13 @@ struct EdifBackend : public Backend {
|
|||
top_module_name = module->name.str();
|
||||
|
||||
if (module->processes.size() != 0)
|
||||
log_error("Found unmapped processes in module %s: unmapped processes are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
|
||||
log_error("Found unmapped processes in module %s: unmapped processes are not supported in EDIF backend!\n", log_id(module->name));
|
||||
if (module->memories.size() != 0)
|
||||
log_error("Found unmapped memories in module %s: unmapped memories are not supported in EDIF backend!\n", RTLIL::id2cstr(module->name));
|
||||
log_error("Found unmapped memories in module %s: unmapped memories are not supported in EDIF backend!\n", log_id(module->name));
|
||||
|
||||
for (auto cell_it : module->cells_)
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
RTLIL::Cell *cell = cell_it.second;
|
||||
if (!design->modules_.count(cell->type) || design->modules_.at(cell->type)->get_blackbox_attribute()) {
|
||||
if (design->module(cell->type) == nullptr || design->module(cell->type)->get_blackbox_attribute()) {
|
||||
lib_cell_ports[cell->type];
|
||||
for (auto p : cell->connections())
|
||||
lib_cell_ports[cell->type][p.first] = GetSize(p.second);
|
||||
|
@ -277,11 +275,11 @@ struct EdifBackend : public Backend {
|
|||
|
||||
// extract module dependencies
|
||||
std::map<RTLIL::Module*, std::set<RTLIL::Module*>> module_deps;
|
||||
for (auto &mod_it : design->modules_) {
|
||||
module_deps[mod_it.second] = std::set<RTLIL::Module*>();
|
||||
for (auto &cell_it : mod_it.second->cells_)
|
||||
if (design->modules_.count(cell_it.second->type) > 0)
|
||||
module_deps[mod_it.second].insert(design->modules_.at(cell_it.second->type));
|
||||
for (auto module : design->modules()) {
|
||||
module_deps[module] = std::set<RTLIL::Module*>();
|
||||
for (auto cell : module->cells())
|
||||
if (design->module(cell->type) != nullptr)
|
||||
module_deps[module].insert(design->module(cell->type));
|
||||
}
|
||||
|
||||
// simple good-enough topological sort
|
||||
|
@ -292,12 +290,12 @@ struct EdifBackend : public Backend {
|
|||
for (auto &dep : it.second)
|
||||
if (module_deps.count(dep) > 0)
|
||||
goto not_ready_yet;
|
||||
// log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name));
|
||||
// log("Next in topological sort: %s\n", log_id(it.first->name));
|
||||
sorted_modules.push_back(it.first);
|
||||
not_ready_yet:;
|
||||
}
|
||||
if (sorted_modules_idx == sorted_modules.size())
|
||||
log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name));
|
||||
log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", log_id(module_deps.begin()->first->name));
|
||||
while (sorted_modules_idx < sorted_modules.size())
|
||||
module_deps.erase(sorted_modules.at(sorted_modules_idx++));
|
||||
}
|
||||
|
@ -339,8 +337,7 @@ struct EdifBackend : public Backend {
|
|||
*f << stringf(" (view VIEW_NETLIST\n");
|
||||
*f << stringf(" (viewType NETLIST)\n");
|
||||
*f << stringf(" (interface\n");
|
||||
for (auto &wire_it : module->wires_) {
|
||||
RTLIL::Wire *wire = wire_it.second;
|
||||
for (auto wire : module->wires()) {
|
||||
if (wire->port_id == 0)
|
||||
continue;
|
||||
const char *dir = "INOUT";
|
||||
|
@ -378,8 +375,7 @@ struct EdifBackend : public Backend {
|
|||
*f << stringf(" (instance GND (viewRef VIEW_NETLIST (cellRef GND (libraryRef LIB))))\n");
|
||||
*f << stringf(" (instance VCC (viewRef VIEW_NETLIST (cellRef VCC (libraryRef LIB))))\n");
|
||||
}
|
||||
for (auto &cell_it : module->cells_) {
|
||||
RTLIL::Cell *cell = cell_it.second;
|
||||
for (auto cell : module->cells()) {
|
||||
*f << stringf(" (instance %s\n", EDIF_DEF(cell->name));
|
||||
*f << stringf(" (viewRef VIEW_NETLIST (cellRef %s%s))", EDIF_REF(cell->type),
|
||||
lib_cell_ports.count(cell->type) > 0 ? " (libraryRef LIB)" : "");
|
||||
|
@ -459,8 +455,7 @@ struct EdifBackend : public Backend {
|
|||
add_prop(p.first, p.second);
|
||||
*f << stringf("\n )\n");
|
||||
}
|
||||
for (auto &wire_it : module->wires_) {
|
||||
RTLIL::Wire *wire = wire_it.second;
|
||||
for (auto wire : module->wires()) {
|
||||
if (!wire->get_bool_attribute(ID::keep))
|
||||
continue;
|
||||
for(int i = 0; i < wire->width; i++) {
|
||||
|
|
|
@ -208,7 +208,7 @@ struct FirrtlWorker
|
|||
const char *atLine() {
|
||||
if (srcLine == "") {
|
||||
if (pCell) {
|
||||
auto p = pCell->attributes.find("\\src");
|
||||
auto p = pCell->attributes.find(ID::src);
|
||||
srcLine = " at " + p->second.decode_string();
|
||||
}
|
||||
}
|
||||
|
@ -414,9 +414,9 @@ struct FirrtlWorker
|
|||
std::string wireFileinfo = getFileinfo(wire);
|
||||
|
||||
// If a wire has initial data, issue a warning since FIRRTL doesn't currently support it.
|
||||
if (wire->attributes.count("\\init")) {
|
||||
if (wire->attributes.count(ID::init)) {
|
||||
log_warning("Initial value (%s) for (%s.%s) not supported\n",
|
||||
wire->attributes.at("\\init").as_string().c_str(),
|
||||
wire->attributes.at(ID::init).as_string().c_str(),
|
||||
log_id(module), log_id(wire));
|
||||
}
|
||||
if (wire->port_id)
|
||||
|
@ -444,11 +444,11 @@ struct FirrtlWorker
|
|||
}
|
||||
// Not a module instance. Set up cell properties
|
||||
bool extract_y_bits = false; // Assume no extraction of final bits will be required.
|
||||
int a_width = cell->parameters.at("\\A_WIDTH", ndef).as_int(); // The width of "A"
|
||||
int b_width = cell->parameters.at("\\B_WIDTH", ndef).as_int(); // The width of "A"
|
||||
const int y_width = cell->parameters.at("\\Y_WIDTH", ndef).as_int(); // The width of the result
|
||||
const bool a_signed = cell->parameters.at("\\A_SIGNED", ndef).as_bool();
|
||||
const bool b_signed = cell->parameters.at("\\B_SIGNED", ndef).as_bool();
|
||||
int a_width = cell->parameters.at(ID::A_WIDTH, ndef).as_int(); // The width of "A"
|
||||
int b_width = cell->parameters.at(ID::B_WIDTH, ndef).as_int(); // The width of "A"
|
||||
const int y_width = cell->parameters.at(ID::Y_WIDTH, ndef).as_int(); // The width of the result
|
||||
const bool a_signed = cell->parameters.at(ID::A_SIGNED, ndef).as_bool();
|
||||
const bool b_signed = cell->parameters.at(ID::B_SIGNED, ndef).as_bool();
|
||||
bool firrtl_is_signed = a_signed; // The result is signed (subsequent code may change this).
|
||||
int firrtl_width = 0;
|
||||
string primop;
|
||||
|
@ -456,9 +456,9 @@ struct FirrtlWorker
|
|||
string y_id = make_id(cell->name);
|
||||
std::string cellFileinfo = getFileinfo(cell);
|
||||
|
||||
if (cell->type.in("$not", "$logic_not", "$neg", "$reduce_and", "$reduce_or", "$reduce_xor", "$reduce_bool", "$reduce_xnor"))
|
||||
if (cell->type.in(ID($not), ID($logic_not), ID($neg), ID($reduce_and), ID($reduce_or), ID($reduce_xor), ID($reduce_bool), ID($reduce_xnor)))
|
||||
{
|
||||
string a_expr = make_expr(cell->getPort("\\A"));
|
||||
string a_expr = make_expr(cell->getPort(ID::A));
|
||||
wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
|
||||
|
||||
if (a_signed) {
|
||||
|
@ -466,29 +466,29 @@ struct FirrtlWorker
|
|||
}
|
||||
|
||||
// Don't use the results of logical operations (a single bit) to control padding
|
||||
if (!(cell->type.in("$eq", "$eqx", "$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$reduce_bool", "$logic_not") && y_width == 1) ) {
|
||||
if (!(cell->type.in(ID($eq), ID($eqx), ID($gt), ID($ge), ID($lt), ID($le), ID($ne), ID($nex), ID($reduce_bool), ID($logic_not)) && y_width == 1) ) {
|
||||
a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
|
||||
}
|
||||
|
||||
// Assume the FIRRTL width is a single bit.
|
||||
firrtl_width = 1;
|
||||
if (cell->type == "$not") primop = "not";
|
||||
else if (cell->type == "$neg") {
|
||||
if (cell->type == ID($not)) primop = "not";
|
||||
else if (cell->type == ID($neg)) {
|
||||
primop = "neg";
|
||||
firrtl_is_signed = true; // Result of "neg" is signed (an SInt).
|
||||
firrtl_width = a_width;
|
||||
} else if (cell->type == "$logic_not") {
|
||||
} else if (cell->type == ID($logic_not)) {
|
||||
primop = "eq";
|
||||
a_expr = stringf("%s, UInt(0)", a_expr.c_str());
|
||||
}
|
||||
else if (cell->type == "$reduce_and") primop = "andr";
|
||||
else if (cell->type == "$reduce_or") primop = "orr";
|
||||
else if (cell->type == "$reduce_xor") primop = "xorr";
|
||||
else if (cell->type == "$reduce_xnor") {
|
||||
else if (cell->type == ID($reduce_and)) primop = "andr";
|
||||
else if (cell->type == ID($reduce_or)) primop = "orr";
|
||||
else if (cell->type == ID($reduce_xor)) primop = "xorr";
|
||||
else if (cell->type == ID($reduce_xnor)) {
|
||||
primop = "not";
|
||||
a_expr = stringf("xorr(%s)", a_expr.c_str());
|
||||
}
|
||||
else if (cell->type == "$reduce_bool") {
|
||||
else if (cell->type == ID($reduce_bool)) {
|
||||
primop = "neq";
|
||||
// Use the sign of the a_expr and its width as the type (UInt/SInt) and width of the comparand.
|
||||
a_expr = stringf("%s, %cInt<%d>(0)", a_expr.c_str(), a_signed ? 'S' : 'U', a_width);
|
||||
|
@ -500,16 +500,16 @@ struct FirrtlWorker
|
|||
expr = stringf("asUInt(%s)", expr.c_str());
|
||||
|
||||
cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
|
||||
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
|
||||
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
|
||||
|
||||
continue;
|
||||
}
|
||||
if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or", "$eq", "$eqx",
|
||||
"$gt", "$ge", "$lt", "$le", "$ne", "$nex", "$shr", "$sshr", "$sshl", "$shl",
|
||||
"$logic_and", "$logic_or", "$pow"))
|
||||
if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or), ID($eq), ID($eqx),
|
||||
ID($gt), ID($ge), ID($lt), ID($le), ID($ne), ID($nex), ID($shr), ID($sshr), ID($sshl), ID($shl),
|
||||
ID($logic_and), ID($logic_or), ID($pow)))
|
||||
{
|
||||
string a_expr = make_expr(cell->getPort("\\A"));
|
||||
string b_expr = make_expr(cell->getPort("\\B"));
|
||||
string a_expr = make_expr(cell->getPort(ID::A));
|
||||
string b_expr = make_expr(cell->getPort(ID::B));
|
||||
std::string cellFileinfo = getFileinfo(cell);
|
||||
wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), y_width, cellFileinfo.c_str()));
|
||||
|
||||
|
@ -523,7 +523,7 @@ struct FirrtlWorker
|
|||
}
|
||||
// Shift amount is always unsigned, and needn't be padded to result width,
|
||||
// otherwise, we need to cast the b_expr appropriately
|
||||
if (b_signed && !cell->type.in("$shr", "$sshr", "$shl", "$sshl", "$pow")) {
|
||||
if (b_signed && !cell->type.in(ID($shr), ID($sshr), ID($shl), ID($sshl), ID($pow))) {
|
||||
b_expr = "asSInt(" + b_expr + ")";
|
||||
// Expand the "B" operand to the result width
|
||||
if (b_width < y_width) {
|
||||
|
@ -534,7 +534,7 @@ struct FirrtlWorker
|
|||
|
||||
// For the arithmetic ops, expand operand widths to result widths befor performing the operation.
|
||||
// This corresponds (according to iverilog) to what verilog compilers implement.
|
||||
if (cell->type.in("$add", "$sub", "$mul", "$div", "$mod", "$xor", "$xnor", "$and", "$or"))
|
||||
if (cell->type.in(ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($xor), ID($xnor), ID($and), ID($or)))
|
||||
{
|
||||
if (a_width < y_width) {
|
||||
a_expr = stringf("pad(%s, %d)", a_expr.c_str(), y_width);
|
||||
|
@ -547,85 +547,85 @@ struct FirrtlWorker
|
|||
}
|
||||
// Assume the FIRRTL width is the width of "A"
|
||||
firrtl_width = a_width;
|
||||
auto a_sig = cell->getPort("\\A");
|
||||
auto a_sig = cell->getPort(ID::A);
|
||||
|
||||
if (cell->type == "$add") {
|
||||
if (cell->type == ID($add)) {
|
||||
primop = "add";
|
||||
firrtl_is_signed = a_signed | b_signed;
|
||||
firrtl_width = max(a_width, b_width);
|
||||
} else if (cell->type == "$sub") {
|
||||
} else if (cell->type == ID($sub)) {
|
||||
primop = "sub";
|
||||
firrtl_is_signed = true;
|
||||
int a_widthInc = (!a_signed && b_signed) ? 2 : (a_signed && !b_signed) ? 1 : 0;
|
||||
int b_widthInc = (a_signed && !b_signed) ? 2 : (!a_signed && b_signed) ? 1 : 0;
|
||||
firrtl_width = max(a_width + a_widthInc, b_width + b_widthInc);
|
||||
} else if (cell->type == "$mul") {
|
||||
} else if (cell->type == ID($mul)) {
|
||||
primop = "mul";
|
||||
firrtl_is_signed = a_signed | b_signed;
|
||||
firrtl_width = a_width + b_width;
|
||||
} else if (cell->type == "$div") {
|
||||
} else if (cell->type == ID($div)) {
|
||||
primop = "div";
|
||||
firrtl_is_signed = a_signed | b_signed;
|
||||
firrtl_width = a_width;
|
||||
} else if (cell->type == "$mod") {
|
||||
} else if (cell->type == ID($mod)) {
|
||||
primop = "rem";
|
||||
firrtl_width = min(a_width, b_width);
|
||||
} else if (cell->type == "$and") {
|
||||
} else if (cell->type == ID($and)) {
|
||||
primop = "and";
|
||||
always_uint = true;
|
||||
firrtl_width = max(a_width, b_width);
|
||||
}
|
||||
else if (cell->type == "$or" ) {
|
||||
else if (cell->type == ID($or) ) {
|
||||
primop = "or";
|
||||
always_uint = true;
|
||||
firrtl_width = max(a_width, b_width);
|
||||
}
|
||||
else if (cell->type == "$xor") {
|
||||
else if (cell->type == ID($xor)) {
|
||||
primop = "xor";
|
||||
always_uint = true;
|
||||
firrtl_width = max(a_width, b_width);
|
||||
}
|
||||
else if (cell->type == "$xnor") {
|
||||
else if (cell->type == ID($xnor)) {
|
||||
primop = "xnor";
|
||||
always_uint = true;
|
||||
firrtl_width = max(a_width, b_width);
|
||||
}
|
||||
else if ((cell->type == "$eq") | (cell->type == "$eqx")) {
|
||||
else if ((cell->type == ID($eq)) | (cell->type == ID($eqx))) {
|
||||
primop = "eq";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if ((cell->type == "$ne") | (cell->type == "$nex")) {
|
||||
}
|
||||
else if ((cell->type == ID($ne)) | (cell->type == ID($nex))) {
|
||||
primop = "neq";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if (cell->type == "$gt") {
|
||||
else if (cell->type == ID($gt)) {
|
||||
primop = "gt";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if (cell->type == "$ge") {
|
||||
else if (cell->type == ID($ge)) {
|
||||
primop = "geq";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if (cell->type == "$lt") {
|
||||
else if (cell->type == ID($lt)) {
|
||||
primop = "lt";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if (cell->type == "$le") {
|
||||
else if (cell->type == ID($le)) {
|
||||
primop = "leq";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if ((cell->type == "$shl") | (cell->type == "$sshl")) {
|
||||
else if ((cell->type == ID($shl)) | (cell->type == ID($sshl))) {
|
||||
// FIRRTL will widen the result (y) by the amount of the shift.
|
||||
// We'll need to offset this by extracting the un-widened portion as Verilog would do.
|
||||
extract_y_bits = true;
|
||||
// Is the shift amount constant?
|
||||
auto b_sig = cell->getPort("\\B");
|
||||
auto b_sig = cell->getPort(ID::B);
|
||||
if (b_sig.is_fully_const()) {
|
||||
primop = "shl";
|
||||
int shift_amount = b_sig.as_int();
|
||||
|
@ -638,11 +638,11 @@ struct FirrtlWorker
|
|||
firrtl_width = a_width + (1 << b_width) - 1;
|
||||
}
|
||||
}
|
||||
else if ((cell->type == "$shr") | (cell->type == "$sshr")) {
|
||||
else if ((cell->type == ID($shr)) | (cell->type == ID($sshr))) {
|
||||
// We don't need to extract a specific range of bits.
|
||||
extract_y_bits = false;
|
||||
// Is the shift amount constant?
|
||||
auto b_sig = cell->getPort("\\B");
|
||||
auto b_sig = cell->getPort(ID::B);
|
||||
if (b_sig.is_fully_const()) {
|
||||
primop = "shr";
|
||||
int shift_amount = b_sig.as_int();
|
||||
|
@ -655,26 +655,26 @@ struct FirrtlWorker
|
|||
// We'll need to do some special fixups if the source (and thus result) is signed.
|
||||
if (firrtl_is_signed) {
|
||||
// If this is a "logical" shift right, pretend the source is unsigned.
|
||||
if (cell->type == "$shr") {
|
||||
if (cell->type == ID($shr)) {
|
||||
a_expr = "asUInt(" + a_expr + ")";
|
||||
}
|
||||
}
|
||||
}
|
||||
else if ((cell->type == "$logic_and")) {
|
||||
else if ((cell->type == ID($logic_and))) {
|
||||
primop = "and";
|
||||
a_expr = "neq(" + a_expr + ", UInt(0))";
|
||||
b_expr = "neq(" + b_expr + ", UInt(0))";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if ((cell->type == "$logic_or")) {
|
||||
else if ((cell->type == ID($logic_or))) {
|
||||
primop = "or";
|
||||
a_expr = "neq(" + a_expr + ", UInt(0))";
|
||||
b_expr = "neq(" + b_expr + ", UInt(0))";
|
||||
always_uint = true;
|
||||
firrtl_width = 1;
|
||||
}
|
||||
else if ((cell->type == "$pow")) {
|
||||
else if ((cell->type == ID($pow))) {
|
||||
if (a_sig.is_fully_const() && a_sig.as_int() == 2) {
|
||||
// We'll convert this to a shift. To simplify things, change the a_expr to "1"
|
||||
// so we can use b_expr directly as a shift amount.
|
||||
|
@ -684,7 +684,7 @@ struct FirrtlWorker
|
|||
a_expr = firrtl_is_signed ? "SInt(1)" : "UInt(1)";
|
||||
extract_y_bits = true;
|
||||
// Is the shift amount constant?
|
||||
auto b_sig = cell->getPort("\\B");
|
||||
auto b_sig = cell->getPort(ID::B);
|
||||
if (b_sig.is_fully_const()) {
|
||||
primop = "shl";
|
||||
int shiftAmount = b_sig.as_int();
|
||||
|
@ -704,7 +704,7 @@ struct FirrtlWorker
|
|||
}
|
||||
}
|
||||
|
||||
if (!cell->parameters.at("\\B_SIGNED").as_bool()) {
|
||||
if (!cell->parameters.at(ID::B_SIGNED).as_bool()) {
|
||||
b_expr = "asUInt(" + b_expr + ")";
|
||||
}
|
||||
|
||||
|
@ -728,47 +728,47 @@ struct FirrtlWorker
|
|||
expr = stringf("asUInt(%s)", expr.c_str());
|
||||
|
||||
cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
|
||||
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
|
||||
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$mux"))
|
||||
if (cell->type.in(ID($mux)))
|
||||
{
|
||||
int width = cell->parameters.at("\\WIDTH").as_int();
|
||||
string a_expr = make_expr(cell->getPort("\\A"));
|
||||
string b_expr = make_expr(cell->getPort("\\B"));
|
||||
string s_expr = make_expr(cell->getPort("\\S"));
|
||||
int width = cell->parameters.at(ID::WIDTH).as_int();
|
||||
string a_expr = make_expr(cell->getPort(ID::A));
|
||||
string b_expr = make_expr(cell->getPort(ID::B));
|
||||
string s_expr = make_expr(cell->getPort(ID::S));
|
||||
wire_decls.push_back(stringf(" wire %s: UInt<%d> %s\n", y_id.c_str(), width, cellFileinfo.c_str()));
|
||||
|
||||
string expr = stringf("mux(%s, %s, %s)", s_expr.c_str(), b_expr.c_str(), a_expr.c_str());
|
||||
|
||||
cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
|
||||
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
|
||||
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$mem"))
|
||||
if (cell->type.in(ID($mem)))
|
||||
{
|
||||
string mem_id = make_id(cell->name);
|
||||
int abits = cell->parameters.at("\\ABITS").as_int();
|
||||
int width = cell->parameters.at("\\WIDTH").as_int();
|
||||
int size = cell->parameters.at("\\SIZE").as_int();
|
||||
int abits = cell->parameters.at(ID::ABITS).as_int();
|
||||
int width = cell->parameters.at(ID::WIDTH).as_int();
|
||||
int size = cell->parameters.at(ID::SIZE).as_int();
|
||||
memory m(cell, 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();
|
||||
int rd_ports = cell->parameters.at(ID::RD_PORTS).as_int();
|
||||
int wr_ports = cell->parameters.at(ID::WR_PORTS).as_int();
|
||||
|
||||
Const initdata = cell->parameters.at("\\INIT");
|
||||
Const initdata = cell->parameters.at(ID::INIT);
|
||||
for (State bit : initdata.bits)
|
||||
if (bit != State::Sx)
|
||||
log_error("Memory with initialization data: %s.%s\n", log_id(module), log_id(cell));
|
||||
|
||||
Const rd_clk_enable = cell->parameters.at("\\RD_CLK_ENABLE");
|
||||
Const wr_clk_enable = cell->parameters.at("\\WR_CLK_ENABLE");
|
||||
Const wr_clk_polarity = cell->parameters.at("\\WR_CLK_POLARITY");
|
||||
Const rd_clk_enable = cell->parameters.at(ID::RD_CLK_ENABLE);
|
||||
Const wr_clk_enable = cell->parameters.at(ID::WR_CLK_ENABLE);
|
||||
Const wr_clk_polarity = cell->parameters.at(ID::WR_CLK_POLARITY);
|
||||
|
||||
int offset = cell->parameters.at("\\OFFSET").as_int();
|
||||
int offset = cell->parameters.at(ID::OFFSET).as_int();
|
||||
if (offset != 0)
|
||||
log_error("Memory with nonzero offset: %s.%s\n", log_id(module), log_id(cell));
|
||||
|
||||
|
@ -777,8 +777,8 @@ struct FirrtlWorker
|
|||
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);
|
||||
SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(i*abits, abits);
|
||||
SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(i*width, width);
|
||||
string addr_expr = make_expr(addr_sig);
|
||||
string name(stringf("%s.r%d", m.name.c_str(), i));
|
||||
bool clk_enable = false;
|
||||
|
@ -804,14 +804,14 @@ struct FirrtlWorker
|
|||
bool clk_enable = true;
|
||||
bool clk_parity = true;
|
||||
bool transparency = false;
|
||||
SigSpec addr_sig =cell->getPort("\\WR_ADDR").extract(i*abits, abits);
|
||||
SigSpec addr_sig =cell->getPort(ID::WR_ADDR).extract(i*abits, abits);
|
||||
string addr_expr = make_expr(addr_sig);
|
||||
SigSpec data_sig =cell->getPort("\\WR_DATA").extract(i*width, width);
|
||||
SigSpec data_sig =cell->getPort(ID::WR_DATA).extract(i*width, width);
|
||||
string data_expr = make_expr(data_sig);
|
||||
SigSpec clk_sig = cell->getPort("\\WR_CLK").extract(i);
|
||||
SigSpec clk_sig = cell->getPort(ID::WR_CLK).extract(i);
|
||||
string clk_expr = make_expr(clk_sig);
|
||||
|
||||
SigSpec wen_sig = cell->getPort("\\WR_EN").extract(i*width, width);
|
||||
SigSpec wen_sig = cell->getPort(ID::WR_EN).extract(i*width, width);
|
||||
string wen_expr = make_expr(wen_sig[0]);
|
||||
|
||||
for (int i = 1; i < GetSize(wen_sig); i++)
|
||||
|
@ -828,23 +828,23 @@ struct FirrtlWorker
|
|||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$memwr", "$memrd", "$meminit"))
|
||||
if (cell->type.in(ID($memwr), ID($memrd), ID($meminit)))
|
||||
{
|
||||
std::string cell_type = fid(cell->type);
|
||||
std::string mem_id = make_id(cell->parameters["\\MEMID"].decode_string());
|
||||
int abits = cell->parameters.at("\\ABITS").as_int();
|
||||
int width = cell->parameters.at("\\WIDTH").as_int();
|
||||
std::string mem_id = make_id(cell->parameters[ID::MEMID].decode_string());
|
||||
int abits = cell->parameters.at(ID::ABITS).as_int();
|
||||
int width = cell->parameters.at(ID::WIDTH).as_int();
|
||||
memory *mp = nullptr;
|
||||
if (cell->type == "$meminit" ) {
|
||||
if (cell->type == ID($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");
|
||||
auto addrSig = cell->getPort(ID::ADDR);
|
||||
auto dataSig = cell->getPort(ID::DATA);
|
||||
auto enableSig = cell->getPort(ID::EN);
|
||||
auto clockSig = cell->getPort(ID::CLK);
|
||||
Const clk_enable = cell->parameters.at(ID::CLK_ENABLE);
|
||||
Const clk_polarity = cell->parameters.at(ID::CLK_POLARITY);
|
||||
|
||||
// Do we already have an entry for this memory?
|
||||
if (memories.count(mem_id) == 0) {
|
||||
|
@ -855,13 +855,13 @@ struct FirrtlWorker
|
|||
int portNum = 0;
|
||||
bool transparency = false;
|
||||
string data_expr = make_expr(dataSig);
|
||||
if (cell->type.in("$memwr")) {
|
||||
if (cell->type.in(ID($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")) {
|
||||
} else if (cell->type.in(ID($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);
|
||||
|
@ -872,20 +872,20 @@ struct FirrtlWorker
|
|||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$dff"))
|
||||
if (cell->type.in(ID($dff)))
|
||||
{
|
||||
bool clkpol = cell->parameters.at("\\CLK_POLARITY").as_bool();
|
||||
bool clkpol = cell->parameters.at(ID::CLK_POLARITY).as_bool();
|
||||
if (clkpol == false)
|
||||
log_error("Negative edge clock on FF %s.%s.\n", log_id(module), log_id(cell));
|
||||
|
||||
int width = cell->parameters.at("\\WIDTH").as_int();
|
||||
string expr = make_expr(cell->getPort("\\D"));
|
||||
string clk_expr = "asClock(" + make_expr(cell->getPort("\\CLK")) + ")";
|
||||
int width = cell->parameters.at(ID::WIDTH).as_int();
|
||||
string expr = make_expr(cell->getPort(ID::D));
|
||||
string clk_expr = "asClock(" + make_expr(cell->getPort(ID::CLK)) + ")";
|
||||
|
||||
wire_decls.push_back(stringf(" reg %s: UInt<%d>, %s %s\n", y_id.c_str(), width, clk_expr.c_str(), cellFileinfo.c_str()));
|
||||
|
||||
cell_exprs.push_back(stringf(" %s <= %s %s\n", y_id.c_str(), expr.c_str(), cellFileinfo.c_str()));
|
||||
register_reverse_wire_map(y_id, cell->getPort("\\Q"));
|
||||
register_reverse_wire_map(y_id, cell->getPort(ID::Q));
|
||||
|
||||
continue;
|
||||
}
|
||||
|
@ -896,38 +896,38 @@ struct FirrtlWorker
|
|||
process_instance(cell, wire_exprs);
|
||||
continue;
|
||||
}
|
||||
if (cell->type == "$shiftx") {
|
||||
if (cell->type == ID($shiftx)) {
|
||||
// assign y = a[b +: y_width];
|
||||
// We'll extract the correct bits as part of the primop.
|
||||
|
||||
string a_expr = make_expr(cell->getPort("\\A"));
|
||||
string a_expr = make_expr(cell->getPort(ID::A));
|
||||
// Get the initial bit selector
|
||||
string b_expr = make_expr(cell->getPort("\\B"));
|
||||
string b_expr = make_expr(cell->getPort(ID::B));
|
||||
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
|
||||
|
||||
if (cell->getParam("\\B_SIGNED").as_bool()) {
|
||||
if (cell->getParam(ID::B_SIGNED).as_bool()) {
|
||||
// Use validif to constrain the selection (test the sign bit)
|
||||
auto b_string = b_expr.c_str();
|
||||
int b_sign = cell->parameters.at("\\B_WIDTH").as_int() - 1;
|
||||
int b_sign = cell->parameters.at(ID::B_WIDTH).as_int() - 1;
|
||||
b_expr = stringf("validif(not(bits(%s, %d, %d)), %s)", b_string, b_sign, b_sign, b_string);
|
||||
}
|
||||
string expr = stringf("dshr(%s, %s)", a_expr.c_str(), b_expr.c_str());
|
||||
|
||||
cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
|
||||
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
|
||||
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
|
||||
continue;
|
||||
}
|
||||
if (cell->type == "$shift") {
|
||||
if (cell->type == ID($shift)) {
|
||||
// assign y = a >> b;
|
||||
// where b may be negative
|
||||
|
||||
string a_expr = make_expr(cell->getPort("\\A"));
|
||||
string b_expr = make_expr(cell->getPort("\\B"));
|
||||
string a_expr = make_expr(cell->getPort(ID::A));
|
||||
string b_expr = make_expr(cell->getPort(ID::B));
|
||||
auto b_string = b_expr.c_str();
|
||||
string expr;
|
||||
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
|
||||
|
||||
if (cell->getParam("\\B_SIGNED").as_bool()) {
|
||||
if (cell->getParam(ID::B_SIGNED).as_bool()) {
|
||||
// We generate a left or right shift based on the sign of b.
|
||||
std::string dshl = stringf("bits(dshl(%s, %s), 0, %d)", a_expr.c_str(), gen_dshl(b_expr, b_width).c_str(), y_width);
|
||||
std::string dshr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
|
||||
|
@ -940,13 +940,13 @@ struct FirrtlWorker
|
|||
expr = stringf("dshr(%s, %s)", a_expr.c_str(), b_string);
|
||||
}
|
||||
cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), expr.c_str()));
|
||||
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
|
||||
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
|
||||
continue;
|
||||
}
|
||||
if (cell->type == "$pos") {
|
||||
if (cell->type == ID($pos)) {
|
||||
// assign y = a;
|
||||
// printCell(cell);
|
||||
string a_expr = make_expr(cell->getPort("\\A"));
|
||||
string a_expr = make_expr(cell->getPort(ID::A));
|
||||
// Verilog appears to treat the result as signed, so if the result is wider than "A",
|
||||
// we need to pad.
|
||||
if (a_width < y_width) {
|
||||
|
@ -954,7 +954,7 @@ struct FirrtlWorker
|
|||
}
|
||||
wire_decls.push_back(stringf(" wire %s: UInt<%d>\n", y_id.c_str(), y_width));
|
||||
cell_exprs.push_back(stringf(" %s <= %s\n", y_id.c_str(), a_expr.c_str()));
|
||||
register_reverse_wire_map(y_id, cell->getPort("\\Y"));
|
||||
register_reverse_wire_map(y_id, cell->getPort(ID::Y));
|
||||
continue;
|
||||
}
|
||||
log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
|
||||
|
@ -1134,7 +1134,7 @@ struct FirrtlBackend : public Backend {
|
|||
for (auto module : design->modules()) {
|
||||
make_id(module->name);
|
||||
last = module;
|
||||
if (top == nullptr && module->get_bool_attribute("\\top")) {
|
||||
if (top == nullptr && module->get_bool_attribute(ID::top)) {
|
||||
top = module;
|
||||
}
|
||||
for (auto wire : module->wires())
|
||||
|
|
|
@ -358,10 +358,10 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl
|
|||
|
||||
if (!flag_m) {
|
||||
int count_selected_mods = 0;
|
||||
for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
|
||||
if (design->selected_whole_module(it->first))
|
||||
for (auto module : design->modules()) {
|
||||
if (design->selected_whole_module(module->name))
|
||||
flag_m = true;
|
||||
if (design->selected(it->second))
|
||||
if (design->selected(module))
|
||||
count_selected_mods++;
|
||||
}
|
||||
if (count_selected_mods > 1)
|
||||
|
@ -374,11 +374,11 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl
|
|||
f << stringf("autoidx %d\n", autoidx);
|
||||
}
|
||||
|
||||
for (auto it = design->modules_.begin(); it != design->modules_.end(); ++it) {
|
||||
if (!only_selected || design->selected(it->second)) {
|
||||
for (auto module : design->modules()) {
|
||||
if (!only_selected || design->selected(module)) {
|
||||
if (only_selected)
|
||||
f << stringf("\n");
|
||||
dump_module(f, "", it->second, design, only_selected, flag_m, flag_n);
|
||||
dump_module(f, "", module, design, only_selected, flag_m, flag_n);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -122,70 +122,67 @@ struct IntersynthBackend : public Backend {
|
|||
for (auto lib : libs)
|
||||
ct.setup_design(lib);
|
||||
|
||||
for (auto module_it : design->modules_)
|
||||
for (auto module : design->modules())
|
||||
{
|
||||
RTLIL::Module *module = module_it.second;
|
||||
SigMap sigmap(module);
|
||||
|
||||
if (module->get_blackbox_attribute())
|
||||
continue;
|
||||
if (module->memories.size() == 0 && module->processes.size() == 0 && module->cells_.size() == 0)
|
||||
if (module->memories.size() == 0 && module->processes.size() == 0 && module->cells().size() == 0)
|
||||
continue;
|
||||
|
||||
if (selected && !design->selected_whole_module(module->name)) {
|
||||
if (design->selected_module(module->name))
|
||||
log_cmd_error("Can't handle partially selected module %s!\n", RTLIL::id2cstr(module->name));
|
||||
log_cmd_error("Can't handle partially selected module %s!\n", log_id(module->name));
|
||||
continue;
|
||||
}
|
||||
|
||||
log("Generating netlist %s.\n", RTLIL::id2cstr(module->name));
|
||||
log("Generating netlist %s.\n", log_id(module->name));
|
||||
|
||||
if (module->memories.size() != 0 || module->processes.size() != 0)
|
||||
log_error("Can't generate a netlist for a module with unprocessed memories or processes!\n");
|
||||
|
||||
std::set<std::string> constcells_code;
|
||||
netlists_code += stringf("# Netlist of module %s\n", RTLIL::id2cstr(module->name));
|
||||
netlists_code += stringf("netlist %s\n", RTLIL::id2cstr(module->name));
|
||||
netlists_code += stringf("# Netlist of module %s\n", log_id(module->name));
|
||||
netlists_code += stringf("netlist %s\n", log_id(module->name));
|
||||
|
||||
// Module Ports: "std::set<string> celltypes_code" prevents duplicate top level ports
|
||||
for (auto wire_it : module->wires_) {
|
||||
RTLIL::Wire *wire = wire_it.second;
|
||||
for (auto wire : module->wires()) {
|
||||
if (wire->port_input || wire->port_output) {
|
||||
celltypes_code.insert(stringf("celltype !%s b%d %sPORT\n" "%s %s %d %s PORT\n",
|
||||
RTLIL::id2cstr(wire->name), wire->width, wire->port_input ? "*" : "",
|
||||
wire->port_input ? "input" : "output", RTLIL::id2cstr(wire->name), wire->width, RTLIL::id2cstr(wire->name)));
|
||||
netlists_code += stringf("node %s %s PORT %s\n", RTLIL::id2cstr(wire->name), RTLIL::id2cstr(wire->name),
|
||||
log_id(wire->name), wire->width, wire->port_input ? "*" : "",
|
||||
wire->port_input ? "input" : "output", log_id(wire->name), wire->width, log_id(wire->name)));
|
||||
netlists_code += stringf("node %s %s PORT %s\n", log_id(wire->name), log_id(wire->name),
|
||||
netname(conntypes_code, celltypes_code, constcells_code, sigmap(wire)).c_str());
|
||||
}
|
||||
}
|
||||
|
||||
// Submodules: "std::set<string> celltypes_code" prevents duplicate cell types
|
||||
for (auto cell_it : module->cells_)
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
RTLIL::Cell *cell = cell_it.second;
|
||||
std::string celltype_code, node_code;
|
||||
|
||||
if (!ct.cell_known(cell->type))
|
||||
log_error("Found unknown cell type %s in module!\n", RTLIL::id2cstr(cell->type));
|
||||
log_error("Found unknown cell type %s in module!\n", log_id(cell->type));
|
||||
|
||||
celltype_code = stringf("celltype %s", RTLIL::id2cstr(cell->type));
|
||||
node_code = stringf("node %s %s", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
|
||||
celltype_code = stringf("celltype %s", log_id(cell->type));
|
||||
node_code = stringf("node %s %s", log_id(cell->name), log_id(cell->type));
|
||||
for (auto &port : cell->connections()) {
|
||||
RTLIL::SigSpec sig = sigmap(port.second);
|
||||
if (sig.size() != 0) {
|
||||
conntypes_code.insert(stringf("conntype b%d %d 2 %d\n", sig.size(), sig.size(), sig.size()));
|
||||
celltype_code += stringf(" b%d %s%s", sig.size(), ct.cell_output(cell->type, port.first) ? "*" : "", RTLIL::id2cstr(port.first));
|
||||
node_code += stringf(" %s %s", RTLIL::id2cstr(port.first), netname(conntypes_code, celltypes_code, constcells_code, sig).c_str());
|
||||
celltype_code += stringf(" b%d %s%s", sig.size(), ct.cell_output(cell->type, port.first) ? "*" : "", log_id(port.first));
|
||||
node_code += stringf(" %s %s", log_id(port.first), netname(conntypes_code, celltypes_code, constcells_code, sig).c_str());
|
||||
}
|
||||
}
|
||||
for (auto ¶m : cell->parameters) {
|
||||
celltype_code += stringf(" cfg:%d %s", int(param.second.bits.size()), RTLIL::id2cstr(param.first));
|
||||
celltype_code += stringf(" cfg:%d %s", int(param.second.bits.size()), log_id(param.first));
|
||||
if (param.second.bits.size() != 32) {
|
||||
node_code += stringf(" %s '", RTLIL::id2cstr(param.first));
|
||||
node_code += stringf(" %s '", log_id(param.first));
|
||||
for (int i = param.second.bits.size()-1; i >= 0; i--)
|
||||
node_code += param.second.bits[i] == State::S1 ? "1" : "0";
|
||||
} else
|
||||
node_code += stringf(" %s 0x%x", RTLIL::id2cstr(param.first), param.second.as_int());
|
||||
node_code += stringf(" %s 0x%x", log_id(param.first), param.second.as_int());
|
||||
}
|
||||
|
||||
celltypes_code.insert(celltype_code + "\n");
|
||||
|
|
|
@ -378,16 +378,16 @@ struct SimplecWorker
|
|||
|
||||
void eval_cell(HierDirtyFlags *work, Cell *cell)
|
||||
{
|
||||
if (cell->type.in("$_BUF_", "$_NOT_"))
|
||||
if (cell->type.in(ID($_BUF_), ID($_NOT_)))
|
||||
{
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
|
||||
|
||||
string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
|
||||
string expr;
|
||||
|
||||
if (cell->type == "$_BUF_") expr = a_expr;
|
||||
if (cell->type == "$_NOT_") expr = "!" + a_expr;
|
||||
if (cell->type == ID($_BUF_)) expr = a_expr;
|
||||
if (cell->type == ID($_NOT_)) expr = "!" + a_expr;
|
||||
|
||||
log_assert(y.wire);
|
||||
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
|
||||
|
@ -397,24 +397,24 @@ struct SimplecWorker
|
|||
return;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_", "$_ANDNOT_", "$_ORNOT_"))
|
||||
if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_)))
|
||||
{
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
|
||||
|
||||
string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
|
||||
string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
|
||||
string expr;
|
||||
|
||||
if (cell->type == "$_AND_") expr = stringf("%s & %s", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == "$_NAND_") expr = stringf("!(%s & %s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == "$_OR_") expr = stringf("%s | %s", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == "$_NOR_") expr = stringf("!(%s | %s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == "$_XOR_") expr = stringf("%s ^ %s", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == "$_XNOR_") expr = stringf("!(%s ^ %s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == "$_ANDNOT_") expr = stringf("%s & (!%s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == "$_ORNOT_") expr = stringf("%s | (!%s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_AND_)) expr = stringf("%s & %s", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_NAND_)) expr = stringf("!(%s & %s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_OR_)) expr = stringf("%s | %s", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_NOR_)) expr = stringf("!(%s | %s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_XOR_)) expr = stringf("%s ^ %s", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_XNOR_)) expr = stringf("!(%s ^ %s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_ANDNOT_)) expr = stringf("%s & (!%s)", a_expr.c_str(), b_expr.c_str());
|
||||
if (cell->type == ID($_ORNOT_)) expr = stringf("%s | (!%s)", a_expr.c_str(), b_expr.c_str());
|
||||
|
||||
log_assert(y.wire);
|
||||
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
|
||||
|
@ -424,20 +424,20 @@ struct SimplecWorker
|
|||
return;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_AOI3_", "$_OAI3_"))
|
||||
if (cell->type.in(ID($_AOI3_), ID($_OAI3_)))
|
||||
{
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
|
||||
SigBit c = sigmaps.at(work->module)(cell->getPort("\\C"));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
|
||||
SigBit c = sigmaps.at(work->module)(cell->getPort(ID::C));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
|
||||
|
||||
string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
|
||||
string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
|
||||
string c_expr = c.wire ? util_get_bit(work->prefix + cid(c.wire->name), c.wire->width, c.offset) : c.data ? "1" : "0";
|
||||
string expr;
|
||||
|
||||
if (cell->type == "$_AOI3_") expr = stringf("!((%s & %s) | %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
|
||||
if (cell->type == "$_OAI3_") expr = stringf("!((%s | %s) & %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
|
||||
if (cell->type == ID($_AOI3_)) expr = stringf("!((%s & %s) | %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
|
||||
if (cell->type == ID($_OAI3_)) expr = stringf("!((%s | %s) & %s)", a_expr.c_str(), b_expr.c_str(), c_expr.c_str());
|
||||
|
||||
log_assert(y.wire);
|
||||
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
|
||||
|
@ -447,13 +447,13 @@ struct SimplecWorker
|
|||
return;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_AOI4_", "$_OAI4_"))
|
||||
if (cell->type.in(ID($_AOI4_), ID($_OAI4_)))
|
||||
{
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
|
||||
SigBit c = sigmaps.at(work->module)(cell->getPort("\\C"));
|
||||
SigBit d = sigmaps.at(work->module)(cell->getPort("\\D"));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
|
||||
SigBit c = sigmaps.at(work->module)(cell->getPort(ID::C));
|
||||
SigBit d = sigmaps.at(work->module)(cell->getPort(ID::D));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
|
||||
|
||||
string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
|
||||
string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
|
||||
|
@ -461,8 +461,8 @@ struct SimplecWorker
|
|||
string d_expr = d.wire ? util_get_bit(work->prefix + cid(d.wire->name), d.wire->width, d.offset) : d.data ? "1" : "0";
|
||||
string expr;
|
||||
|
||||
if (cell->type == "$_AOI4_") expr = stringf("!((%s & %s) | (%s & %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
|
||||
if (cell->type == "$_OAI4_") expr = stringf("!((%s | %s) & (%s | %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
|
||||
if (cell->type == ID($_AOI4_)) expr = stringf("!((%s & %s) | (%s & %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
|
||||
if (cell->type == ID($_OAI4_)) expr = stringf("!((%s | %s) & (%s | %s))", a_expr.c_str(), b_expr.c_str(), c_expr.c_str(), d_expr.c_str());
|
||||
|
||||
log_assert(y.wire);
|
||||
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
|
||||
|
@ -472,12 +472,12 @@ struct SimplecWorker
|
|||
return;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_MUX_", "$_NMUX_"))
|
||||
if (cell->type.in(ID($_MUX_), ID($_NMUX_)))
|
||||
{
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort("\\A"));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort("\\B"));
|
||||
SigBit s = sigmaps.at(work->module)(cell->getPort("\\S"));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort("\\Y"));
|
||||
SigBit a = sigmaps.at(work->module)(cell->getPort(ID::A));
|
||||
SigBit b = sigmaps.at(work->module)(cell->getPort(ID::B));
|
||||
SigBit s = sigmaps.at(work->module)(cell->getPort(ID::S));
|
||||
SigBit y = sigmaps.at(work->module)(cell->getPort(ID::Y));
|
||||
|
||||
string a_expr = a.wire ? util_get_bit(work->prefix + cid(a.wire->name), a.wire->width, a.offset) : a.data ? "1" : "0";
|
||||
string b_expr = b.wire ? util_get_bit(work->prefix + cid(b.wire->name), b.wire->width, b.offset) : b.data ? "1" : "0";
|
||||
|
@ -485,8 +485,8 @@ struct SimplecWorker
|
|||
|
||||
// casts to bool are a workaround for CBMC bug (https://github.com/diffblue/cbmc/issues/933)
|
||||
string expr = stringf("%s ? %s(bool)%s : %s(bool)%s", s_expr.c_str(),
|
||||
cell->type == "$_NMUX_" ? "!" : "", b_expr.c_str(),
|
||||
cell->type == "$_NMUX_" ? "!" : "", a_expr.c_str());
|
||||
cell->type == ID($_NMUX_) ? "!" : "", b_expr.c_str(),
|
||||
cell->type == ID($_NMUX_) ? "!" : "", a_expr.c_str());
|
||||
|
||||
log_assert(y.wire);
|
||||
funct_declarations.push_back(util_set_bit(work->prefix + cid(y.wire->name), y.wire->width, y.offset, expr) +
|
||||
|
@ -653,10 +653,10 @@ struct SimplecWorker
|
|||
|
||||
for (Wire *w : module->wires())
|
||||
{
|
||||
if (w->attributes.count("\\init"))
|
||||
if (w->attributes.count(ID::init))
|
||||
{
|
||||
SigSpec sig = sigmaps.at(module)(w);
|
||||
Const val = w->attributes.at("\\init");
|
||||
Const val = w->attributes.at(ID::init);
|
||||
val.bits.resize(GetSize(sig), State::Sx);
|
||||
|
||||
for (int i = 0; i < GetSize(sig); i++)
|
||||
|
|
|
@ -135,7 +135,7 @@ struct Smt2Worker
|
|||
log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
|
||||
log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
|
||||
|
||||
if (cell->type.in("$mem") && conn.first.in("\\RD_CLK", "\\WR_CLK"))
|
||||
if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK))
|
||||
{
|
||||
SigSpec clk = sigmap(conn.second);
|
||||
for (int i = 0; i < GetSize(clk); i++)
|
||||
|
@ -143,19 +143,19 @@ struct Smt2Worker
|
|||
if (clk[i].wire == nullptr)
|
||||
continue;
|
||||
|
||||
if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_ENABLE" : "\\WR_CLK_ENABLE")[i] != State::S1)
|
||||
if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1)
|
||||
continue;
|
||||
|
||||
if (cell->getParam(conn.first == "\\RD_CLK" ? "\\RD_CLK_POLARITY" : "\\WR_CLK_POLARITY")[i] == State::S1)
|
||||
if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1)
|
||||
clock_posedge.insert(clk[i]);
|
||||
else
|
||||
clock_negedge.insert(clk[i]);
|
||||
}
|
||||
}
|
||||
else
|
||||
if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_") && conn.first.in("\\CLK", "\\C"))
|
||||
if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C))
|
||||
{
|
||||
bool posedge = (cell->type == "$_DFF_N_") || (cell->type == "$dff" && cell->getParam("\\CLK_POLARITY").as_bool());
|
||||
bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool());
|
||||
for (auto bit : sigmap(conn.second)) {
|
||||
if (posedge)
|
||||
clock_posedge.insert(bit);
|
||||
|
@ -367,15 +367,15 @@ struct Smt2Worker
|
|||
|
||||
void export_gate(RTLIL::Cell *cell, std::string expr)
|
||||
{
|
||||
RTLIL::SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
|
||||
RTLIL::SigBit bit = sigmap(cell->getPort(ID::Y).as_bit());
|
||||
std::string processed_expr;
|
||||
|
||||
for (char ch : expr) {
|
||||
if (ch == 'A') processed_expr += get_bool(cell->getPort("\\A"));
|
||||
else if (ch == 'B') processed_expr += get_bool(cell->getPort("\\B"));
|
||||
else if (ch == 'C') processed_expr += get_bool(cell->getPort("\\C"));
|
||||
else if (ch == 'D') processed_expr += get_bool(cell->getPort("\\D"));
|
||||
else if (ch == 'S') processed_expr += get_bool(cell->getPort("\\S"));
|
||||
if (ch == 'A') processed_expr += get_bool(cell->getPort(ID::A));
|
||||
else if (ch == 'B') processed_expr += get_bool(cell->getPort(ID::B));
|
||||
else if (ch == 'C') processed_expr += get_bool(cell->getPort(ID::C));
|
||||
else if (ch == 'D') processed_expr += get_bool(cell->getPort(ID::D));
|
||||
else if (ch == 'S') processed_expr += get_bool(cell->getPort(ID::S));
|
||||
else processed_expr += ch;
|
||||
}
|
||||
|
||||
|
@ -391,23 +391,23 @@ struct Smt2Worker
|
|||
void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
|
||||
{
|
||||
RTLIL::SigSpec sig_a, sig_b;
|
||||
RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
|
||||
bool is_signed = cell->getParam("\\A_SIGNED").as_bool();
|
||||
RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
|
||||
bool is_signed = cell->getParam(ID::A_SIGNED).as_bool();
|
||||
int width = GetSize(sig_y);
|
||||
|
||||
if (type == 's' || type == 'd' || type == 'b') {
|
||||
width = max(width, GetSize(cell->getPort("\\A")));
|
||||
if (cell->hasPort("\\B"))
|
||||
width = max(width, GetSize(cell->getPort("\\B")));
|
||||
width = max(width, GetSize(cell->getPort(ID::A)));
|
||||
if (cell->hasPort(ID::B))
|
||||
width = max(width, GetSize(cell->getPort(ID::B)));
|
||||
}
|
||||
|
||||
if (cell->hasPort("\\A")) {
|
||||
sig_a = cell->getPort("\\A");
|
||||
if (cell->hasPort(ID::A)) {
|
||||
sig_a = cell->getPort(ID::A);
|
||||
sig_a.extend_u0(width, is_signed);
|
||||
}
|
||||
|
||||
if (cell->hasPort("\\B")) {
|
||||
sig_b = cell->getPort("\\B");
|
||||
if (cell->hasPort(ID::B)) {
|
||||
sig_b = cell->getPort(ID::B);
|
||||
sig_b.extend_u0(width, is_signed && !(type == 's'));
|
||||
}
|
||||
|
||||
|
@ -416,7 +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 == 'P') processed_expr += get_bv(cell->getPort(ID::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;
|
||||
|
@ -443,7 +443,7 @@ struct Smt2Worker
|
|||
|
||||
void export_reduce(RTLIL::Cell *cell, std::string expr, bool identity_val)
|
||||
{
|
||||
RTLIL::SigSpec sig_y = sigmap(cell->getPort("\\Y"));
|
||||
RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
|
||||
std::string processed_expr;
|
||||
|
||||
for (char ch : expr)
|
||||
|
@ -480,9 +480,9 @@ struct Smt2Worker
|
|||
exported_cells.insert(cell);
|
||||
recursive_cells.insert(cell);
|
||||
|
||||
if (cell->type == "$initstate")
|
||||
if (cell->type == ID($initstate))
|
||||
{
|
||||
SigBit bit = sigmap(cell->getPort("\\Y").as_bit());
|
||||
SigBit bit = sigmap(cell->getPort(ID::Y).as_bit());
|
||||
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (|%s_is| state)) ; %s\n",
|
||||
get_id(module), idcounter, get_id(module), get_id(module), log_signal(bit)));
|
||||
register_bool(bit, idcounter++);
|
||||
|
@ -490,132 +490,132 @@ struct Smt2Worker
|
|||
return;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
|
||||
if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
|
||||
{
|
||||
registers.insert(cell);
|
||||
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort("\\Q")));
|
||||
register_bool(cell->getPort("\\Q"), idcounter++);
|
||||
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
|
||||
register_bool(cell->getPort(ID::Q), idcounter++);
|
||||
recursive_cells.erase(cell);
|
||||
return;
|
||||
}
|
||||
|
||||
if (cell->type == "$_BUF_") return export_gate(cell, "A");
|
||||
if (cell->type == "$_NOT_") return export_gate(cell, "(not A)");
|
||||
if (cell->type == "$_AND_") return export_gate(cell, "(and A B)");
|
||||
if (cell->type == "$_NAND_") return export_gate(cell, "(not (and A B))");
|
||||
if (cell->type == "$_OR_") return export_gate(cell, "(or A B)");
|
||||
if (cell->type == "$_NOR_") return export_gate(cell, "(not (or A B))");
|
||||
if (cell->type == "$_XOR_") return export_gate(cell, "(xor A B)");
|
||||
if (cell->type == "$_XNOR_") return export_gate(cell, "(not (xor A B))");
|
||||
if (cell->type == "$_ANDNOT_") return export_gate(cell, "(and A (not B))");
|
||||
if (cell->type == "$_ORNOT_") return export_gate(cell, "(or A (not B))");
|
||||
if (cell->type == "$_MUX_") return export_gate(cell, "(ite S B A)");
|
||||
if (cell->type == "$_NMUX_") return export_gate(cell, "(not (ite S B A))");
|
||||
if (cell->type == "$_AOI3_") return export_gate(cell, "(not (or (and A B) C))");
|
||||
if (cell->type == "$_OAI3_") return export_gate(cell, "(not (and (or A B) C))");
|
||||
if (cell->type == "$_AOI4_") return export_gate(cell, "(not (or (and A B) (and C D)))");
|
||||
if (cell->type == "$_OAI4_") return export_gate(cell, "(not (and (or A B) (or C D)))");
|
||||
if (cell->type == ID($_BUF_)) return export_gate(cell, "A");
|
||||
if (cell->type == ID($_NOT_)) return export_gate(cell, "(not A)");
|
||||
if (cell->type == ID($_AND_)) return export_gate(cell, "(and A B)");
|
||||
if (cell->type == ID($_NAND_)) return export_gate(cell, "(not (and A B))");
|
||||
if (cell->type == ID($_OR_)) return export_gate(cell, "(or A B)");
|
||||
if (cell->type == ID($_NOR_)) return export_gate(cell, "(not (or A B))");
|
||||
if (cell->type == ID($_XOR_)) return export_gate(cell, "(xor A B)");
|
||||
if (cell->type == ID($_XNOR_)) return export_gate(cell, "(not (xor A B))");
|
||||
if (cell->type == ID($_ANDNOT_)) return export_gate(cell, "(and A (not B))");
|
||||
if (cell->type == ID($_ORNOT_)) return export_gate(cell, "(or A (not B))");
|
||||
if (cell->type == ID($_MUX_)) return export_gate(cell, "(ite S B A)");
|
||||
if (cell->type == ID($_NMUX_)) return export_gate(cell, "(not (ite S B A))");
|
||||
if (cell->type == ID($_AOI3_)) return export_gate(cell, "(not (or (and A B) C))");
|
||||
if (cell->type == ID($_OAI3_)) return export_gate(cell, "(not (and (or A B) C))");
|
||||
if (cell->type == ID($_AOI4_)) return export_gate(cell, "(not (or (and A B) (and C D)))");
|
||||
if (cell->type == ID($_OAI4_)) return export_gate(cell, "(not (and (or A B) (or C D)))");
|
||||
|
||||
// FIXME: $lut
|
||||
|
||||
if (bvmode)
|
||||
{
|
||||
if (cell->type.in("$ff", "$dff"))
|
||||
if (cell->type.in(ID($ff), ID($dff)))
|
||||
{
|
||||
registers.insert(cell);
|
||||
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q")));
|
||||
register_bv(cell->getPort("\\Q"), idcounter++);
|
||||
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
|
||||
register_bv(cell->getPort(ID::Q), idcounter++);
|
||||
recursive_cells.erase(cell);
|
||||
return;
|
||||
}
|
||||
|
||||
if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq"))
|
||||
if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq)))
|
||||
{
|
||||
registers.insert(cell);
|
||||
string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
|
||||
if (cell->attributes.count("\\reg"))
|
||||
infostr += " " + cell->attributes.at("\\reg").decode_string();
|
||||
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
|
||||
if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\maximize")){
|
||||
string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell);
|
||||
if (cell->attributes.count(ID::reg))
|
||||
infostr += " " + cell->attributes.at(ID::reg).decode_string();
|
||||
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str()));
|
||||
if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){
|
||||
decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
|
||||
log("Wire %s is maximized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
|
||||
log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
|
||||
}
|
||||
else if (cell->getPort("\\Y").is_wire() && cell->getPort("\\Y").as_wire()->get_bool_attribute("\\minimize")){
|
||||
else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){
|
||||
decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
|
||||
log("Wire %s is minimized\n", cell->getPort("\\Y").as_wire()->name.str().c_str());
|
||||
log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
|
||||
}
|
||||
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
|
||||
if (cell->type == "$anyseq")
|
||||
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y)));
|
||||
if (cell->type == ID($anyseq))
|
||||
ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
|
||||
register_bv(cell->getPort("\\Y"), idcounter++);
|
||||
register_bv(cell->getPort(ID::Y), idcounter++);
|
||||
recursive_cells.erase(cell);
|
||||
return;
|
||||
}
|
||||
|
||||
if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
|
||||
if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
|
||||
if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
|
||||
if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
|
||||
if (cell->type == ID($and)) return export_bvop(cell, "(bvand A B)");
|
||||
if (cell->type == ID($or)) return export_bvop(cell, "(bvor A B)");
|
||||
if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)");
|
||||
if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)");
|
||||
|
||||
if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
|
||||
if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
|
||||
if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
|
||||
if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
|
||||
if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's');
|
||||
if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's');
|
||||
if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's');
|
||||
if (cell->type == ID($sshr)) return export_bvop(cell, "(bvLshr A B)", 's');
|
||||
|
||||
if (cell->type.in("$shift", "$shiftx")) {
|
||||
if (cell->getParam("\\B_SIGNED").as_bool()) {
|
||||
if (cell->type.in(ID($shift), ID($shiftx))) {
|
||||
if (cell->getParam(ID::B_SIGNED).as_bool()) {
|
||||
return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
|
||||
"(bvlshr A B) (bvlshr A (bvneg B)))",
|
||||
GetSize(cell->getPort("\\B")), 0), 's');
|
||||
GetSize(cell->getPort(ID::B)), 0), 's');
|
||||
} else {
|
||||
return export_bvop(cell, "(bvlshr A B)", 's');
|
||||
}
|
||||
}
|
||||
|
||||
if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
|
||||
if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
|
||||
if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
|
||||
if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
|
||||
if (cell->type == ID($lt)) return export_bvop(cell, "(bvUlt A B)", 'b');
|
||||
if (cell->type == ID($le)) return export_bvop(cell, "(bvUle A B)", 'b');
|
||||
if (cell->type == ID($ge)) return export_bvop(cell, "(bvUge A B)", 'b');
|
||||
if (cell->type == ID($gt)) return export_bvop(cell, "(bvUgt A B)", 'b');
|
||||
|
||||
if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
|
||||
if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
|
||||
if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
|
||||
if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
|
||||
if (cell->type == ID($ne)) return export_bvop(cell, "(distinct A B)", 'b');
|
||||
if (cell->type == ID($nex)) return export_bvop(cell, "(distinct A B)", 'b');
|
||||
if (cell->type == ID($eq)) return export_bvop(cell, "(= A B)", 'b');
|
||||
if (cell->type == ID($eqx)) return export_bvop(cell, "(= A B)", 'b');
|
||||
|
||||
if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
|
||||
if (cell->type == "$pos") return export_bvop(cell, "A");
|
||||
if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
|
||||
if (cell->type == ID($not)) return export_bvop(cell, "(bvnot A)");
|
||||
if (cell->type == ID($pos)) return export_bvop(cell, "A");
|
||||
if (cell->type == ID($neg)) return export_bvop(cell, "(bvneg A)");
|
||||
|
||||
if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
|
||||
if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
|
||||
if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
|
||||
if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
|
||||
if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
|
||||
if (cell->type == ID($add)) return export_bvop(cell, "(bvadd A B)");
|
||||
if (cell->type == ID($sub)) return export_bvop(cell, "(bvsub A B)");
|
||||
if (cell->type == ID($mul)) return export_bvop(cell, "(bvmul A B)");
|
||||
if (cell->type == ID($div)) return export_bvop(cell, "(bvUdiv A B)", 'd');
|
||||
if (cell->type == ID($mod)) return export_bvop(cell, "(bvUrem A B)", 'd');
|
||||
|
||||
if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool") &&
|
||||
2*GetSize(cell->getPort("\\A").chunks()) < GetSize(cell->getPort("\\A"))) {
|
||||
bool is_and = cell->type == "$reduce_and";
|
||||
string bits(GetSize(cell->getPort("\\A")), is_and ? '1' : '0');
|
||||
if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) &&
|
||||
2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) {
|
||||
bool is_and = cell->type == ID($reduce_and);
|
||||
string bits(GetSize(cell->getPort(ID::A)), is_and ? '1' : '0');
|
||||
return export_bvop(cell, stringf("(%s A #b%s)", is_and ? "=" : "distinct", bits.c_str()), 'b');
|
||||
}
|
||||
|
||||
if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
|
||||
if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
|
||||
if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
|
||||
if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
|
||||
if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
|
||||
if (cell->type == ID($reduce_and)) return export_reduce(cell, "(and A)", true);
|
||||
if (cell->type == ID($reduce_or)) return export_reduce(cell, "(or A)", false);
|
||||
if (cell->type == ID($reduce_xor)) return export_reduce(cell, "(xor A)", false);
|
||||
if (cell->type == ID($reduce_xnor)) return export_reduce(cell, "(not (xor A))", false);
|
||||
if (cell->type == ID($reduce_bool)) return export_reduce(cell, "(or A)", false);
|
||||
|
||||
if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
|
||||
if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
|
||||
if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
|
||||
if (cell->type == ID($logic_not)) return export_reduce(cell, "(not (or A))", false);
|
||||
if (cell->type == ID($logic_and)) return export_reduce(cell, "(and (or A) (or B))", false);
|
||||
if (cell->type == ID($logic_or)) return export_reduce(cell, "(or A B)", false);
|
||||
|
||||
if (cell->type.in("$mux", "$pmux"))
|
||||
if (cell->type.in(ID($mux), ID($pmux)))
|
||||
{
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
std::string processed_expr = get_bv(cell->getPort("\\A"));
|
||||
int width = GetSize(cell->getPort(ID::Y));
|
||||
std::string processed_expr = get_bv(cell->getPort(ID::A));
|
||||
|
||||
RTLIL::SigSpec sig_b = cell->getPort("\\B");
|
||||
RTLIL::SigSpec sig_s = cell->getPort("\\S");
|
||||
RTLIL::SigSpec sig_b = cell->getPort(ID::B);
|
||||
RTLIL::SigSpec sig_s = cell->getPort(ID::S);
|
||||
get_bv(sig_b);
|
||||
get_bv(sig_s);
|
||||
|
||||
|
@ -626,7 +626,7 @@ struct Smt2Worker
|
|||
if (verbose)
|
||||
log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "", log_id(cell));
|
||||
|
||||
RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
|
||||
RTLIL::SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
|
||||
get_id(module), idcounter, get_id(module), width, processed_expr.c_str(), log_signal(sig)));
|
||||
register_bv(sig, idcounter++);
|
||||
|
@ -637,19 +637,19 @@ struct Smt2Worker
|
|||
// FIXME: $slice $concat
|
||||
}
|
||||
|
||||
if (memmode && cell->type == "$mem")
|
||||
if (memmode && cell->type == ID($mem))
|
||||
{
|
||||
int arrayid = idcounter++;
|
||||
memarrays[cell] = arrayid;
|
||||
|
||||
int abits = cell->getParam("\\ABITS").as_int();
|
||||
int width = cell->getParam("\\WIDTH").as_int();
|
||||
int rd_ports = cell->getParam("\\RD_PORTS").as_int();
|
||||
int wr_ports = cell->getParam("\\WR_PORTS").as_int();
|
||||
int abits = cell->getParam(ID::ABITS).as_int();
|
||||
int width = cell->getParam(ID::WIDTH).as_int();
|
||||
int rd_ports = cell->getParam(ID::RD_PORTS).as_int();
|
||||
int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
|
||||
|
||||
bool async_read = false;
|
||||
if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
|
||||
if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero())
|
||||
if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
|
||||
if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero())
|
||||
log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
|
||||
async_read = true;
|
||||
}
|
||||
|
@ -665,8 +665,8 @@ struct Smt2Worker
|
|||
|
||||
if (statebv)
|
||||
{
|
||||
int mem_size = cell->getParam("\\SIZE").as_int();
|
||||
int mem_offset = cell->getParam("\\OFFSET").as_int();
|
||||
int mem_size = cell->getParam(ID::SIZE).as_int();
|
||||
int mem_offset = cell->getParam(ID::OFFSET).as_int();
|
||||
|
||||
makebits(memstate, width*mem_size, get_id(cell));
|
||||
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
|
||||
|
@ -674,11 +674,11 @@ struct Smt2Worker
|
|||
|
||||
for (int i = 0; i < rd_ports; i++)
|
||||
{
|
||||
SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
|
||||
SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
|
||||
std::string addr = get_bv(addr_sig);
|
||||
|
||||
if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
|
||||
if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
|
||||
log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
|
||||
"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
|
||||
|
||||
|
@ -717,11 +717,11 @@ struct Smt2Worker
|
|||
|
||||
for (int i = 0; i < rd_ports; i++)
|
||||
{
|
||||
SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
|
||||
SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
|
||||
std::string addr = get_bv(addr_sig);
|
||||
|
||||
if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
|
||||
if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
|
||||
log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
|
||||
"Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
|
||||
|
||||
|
@ -801,9 +801,9 @@ struct Smt2Worker
|
|||
|
||||
pool<SigBit> reg_bits;
|
||||
for (auto cell : module->cells())
|
||||
if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) {
|
||||
if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
|
||||
// not using sigmap -- we want the net directly at the dff output
|
||||
for (auto bit : cell->getPort("\\Q"))
|
||||
for (auto bit : cell->getPort(ID::Q))
|
||||
reg_bits.insert(bit);
|
||||
}
|
||||
|
||||
|
@ -812,7 +812,7 @@ struct Smt2Worker
|
|||
for (auto bit : SigSpec(wire))
|
||||
if (reg_bits.count(bit))
|
||||
is_register = true;
|
||||
if (wire->port_id || is_register || wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\')) {
|
||||
if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) {
|
||||
RTLIL::SigSpec sig = sigmap(wire);
|
||||
if (wire->port_input)
|
||||
decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
|
||||
|
@ -820,7 +820,7 @@ struct Smt2Worker
|
|||
decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
|
||||
if (is_register)
|
||||
decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
|
||||
if (wire->get_bool_attribute("\\keep") || (wiresmode && wire->name[0] == '\\'))
|
||||
if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\'))
|
||||
decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
|
||||
if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
|
||||
decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
|
||||
|
@ -854,9 +854,9 @@ struct Smt2Worker
|
|||
|
||||
vector<string> init_list;
|
||||
for (auto wire : module->wires())
|
||||
if (wire->attributes.count("\\init")) {
|
||||
if (wire->attributes.count(ID::init)) {
|
||||
RTLIL::SigSpec sig = sigmap(wire);
|
||||
Const val = wire->attributes.at("\\init");
|
||||
Const val = wire->attributes.at(ID::init);
|
||||
val.bits.resize(GetSize(sig), State::Sx);
|
||||
if (bvmode && GetSize(sig) > 1) {
|
||||
Const mask(State::S1, GetSize(sig));
|
||||
|
@ -885,31 +885,31 @@ struct Smt2Worker
|
|||
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
if (cell->type.in("$assert", "$assume", "$cover"))
|
||||
if (cell->type.in(ID($assert), ID($assume), ID($cover)))
|
||||
{
|
||||
int &id = cell->type == "$assert" ? assert_id :
|
||||
cell->type == "$assume" ? assume_id :
|
||||
cell->type == "$cover" ? cover_id : *(int*)nullptr;
|
||||
int &id = cell->type == ID($assert) ? assert_id :
|
||||
cell->type == ID($assume) ? assume_id :
|
||||
cell->type == ID($cover) ? cover_id : *(int*)nullptr;
|
||||
|
||||
char postfix = cell->type == "$assert" ? 'a' :
|
||||
cell->type == "$assume" ? 'u' :
|
||||
cell->type == "$cover" ? 'c' : 0;
|
||||
char postfix = cell->type == ID($assert) ? 'a' :
|
||||
cell->type == ID($assume) ? 'u' :
|
||||
cell->type == ID($cover) ? 'c' : 0;
|
||||
|
||||
string name_a = get_bool(cell->getPort("\\A"));
|
||||
string name_en = get_bool(cell->getPort("\\EN"));
|
||||
string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
|
||||
string name_a = get_bool(cell->getPort(ID::A));
|
||||
string name_en = get_bool(cell->getPort(ID::EN));
|
||||
string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::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")
|
||||
if (cell->type == ID($cover))
|
||||
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
|
||||
get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
|
||||
else
|
||||
decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
|
||||
get_id(module), postfix, id, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
|
||||
|
||||
if (cell->type == "$assert")
|
||||
if (cell->type == ID($assert))
|
||||
assert_list.push_back(stringf("(|%s_a %d| state)", get_id(module), id));
|
||||
else if (cell->type == "$assume")
|
||||
else if (cell->type == ID($assume))
|
||||
assume_list.push_back(stringf("(|%s_u %d| state)", get_id(module), id));
|
||||
|
||||
id++;
|
||||
|
@ -965,44 +965,44 @@ struct Smt2Worker
|
|||
|
||||
for (auto cell : this_regs)
|
||||
{
|
||||
if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_"))
|
||||
if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
|
||||
{
|
||||
std::string expr_d = get_bool(cell->getPort("\\D"));
|
||||
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
|
||||
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
|
||||
ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort("\\Q")).c_str(), get_bool(cell->getPort("\\Q"), "other_state").c_str()));
|
||||
std::string expr_d = get_bool(cell->getPort(ID::D));
|
||||
std::string expr_q = get_bool(cell->getPort(ID::Q), "next_state");
|
||||
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q))));
|
||||
ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str()));
|
||||
}
|
||||
|
||||
if (cell->type.in("$ff", "$dff"))
|
||||
if (cell->type.in(ID($ff), ID($dff)))
|
||||
{
|
||||
std::string expr_d = get_bv(cell->getPort("\\D"));
|
||||
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
|
||||
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
|
||||
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Q")).c_str(), get_bv(cell->getPort("\\Q"), "other_state").c_str()));
|
||||
std::string expr_d = get_bv(cell->getPort(ID::D));
|
||||
std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state");
|
||||
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Q))));
|
||||
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Q)).c_str(), get_bv(cell->getPort(ID::Q), "other_state").c_str()));
|
||||
}
|
||||
|
||||
if (cell->type.in("$anyconst", "$allconst"))
|
||||
if (cell->type.in(ID($anyconst), ID($allconst)))
|
||||
{
|
||||
std::string expr_d = get_bv(cell->getPort("\\Y"));
|
||||
std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
|
||||
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
|
||||
if (cell->type == "$anyconst")
|
||||
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Y")).c_str(), get_bv(cell->getPort("\\Y"), "other_state").c_str()));
|
||||
std::string expr_d = get_bv(cell->getPort(ID::Y));
|
||||
std::string expr_q = get_bv(cell->getPort(ID::Y), "next_state");
|
||||
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort(ID::Y))));
|
||||
if (cell->type == ID($anyconst))
|
||||
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str()));
|
||||
}
|
||||
|
||||
if (cell->type == "$mem")
|
||||
if (cell->type == ID($mem))
|
||||
{
|
||||
int arrayid = memarrays.at(cell);
|
||||
|
||||
int abits = cell->getParam("\\ABITS").as_int();
|
||||
int width = cell->getParam("\\WIDTH").as_int();
|
||||
int wr_ports = cell->getParam("\\WR_PORTS").as_int();
|
||||
int abits = cell->getParam(ID::ABITS).as_int();
|
||||
int width = cell->getParam(ID::WIDTH).as_int();
|
||||
int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
|
||||
|
||||
bool async_read = false;
|
||||
string initial_memstate, final_memstate;
|
||||
|
||||
if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
|
||||
log_assert(cell->getParam("\\WR_CLK_ENABLE").is_fully_zero());
|
||||
if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
|
||||
log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero());
|
||||
async_read = true;
|
||||
initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
|
||||
final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
|
||||
|
@ -1010,8 +1010,8 @@ struct Smt2Worker
|
|||
|
||||
if (statebv)
|
||||
{
|
||||
int mem_size = cell->getParam("\\SIZE").as_int();
|
||||
int mem_offset = cell->getParam("\\OFFSET").as_int();
|
||||
int mem_size = cell->getParam(ID::SIZE).as_int();
|
||||
int mem_offset = cell->getParam(ID::OFFSET).as_int();
|
||||
|
||||
if (async_read) {
|
||||
makebits(final_memstate, width*mem_size, get_id(cell));
|
||||
|
@ -1019,9 +1019,9 @@ struct Smt2Worker
|
|||
|
||||
for (int i = 0; i < wr_ports; i++)
|
||||
{
|
||||
SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
|
||||
SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
|
||||
SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
|
||||
SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
|
||||
|
||||
std::string addr = get_bv(addr_sig);
|
||||
std::string data = get_bv(data_sig);
|
||||
|
@ -1066,9 +1066,9 @@ struct Smt2Worker
|
|||
|
||||
for (int i = 0; i < wr_ports; i++)
|
||||
{
|
||||
SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort("\\WR_DATA").extract(width*i, width);
|
||||
SigSpec mask_sig = cell->getPort("\\WR_EN").extract(width*i, width);
|
||||
SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
|
||||
SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
|
||||
SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
|
||||
|
||||
std::string addr = get_bv(addr_sig);
|
||||
std::string data = get_bv(data_sig);
|
||||
|
@ -1104,8 +1104,8 @@ struct Smt2Worker
|
|||
if (async_read)
|
||||
hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
|
||||
|
||||
Const init_data = cell->getParam("\\INIT");
|
||||
int memsize = cell->getParam("\\SIZE").as_int();
|
||||
Const init_data = cell->getParam(ID::INIT);
|
||||
int memsize = cell->getParam(ID::SIZE).as_int();
|
||||
|
||||
for (int i = 0; i < memsize; i++)
|
||||
{
|
||||
|
@ -1394,7 +1394,7 @@ struct Smt2Backend : public Backend {
|
|||
log("\n");
|
||||
log("For this proof we create the following template (test.tpl).\n");
|
||||
log("\n");
|
||||
log(" ; we need QF_UFBV for this poof\n");
|
||||
log(" ; we need QF_UFBV for this proof\n");
|
||||
log(" (set-logic QF_UFBV)\n");
|
||||
log("\n");
|
||||
log(" ; insert the auto-generated code here\n");
|
||||
|
@ -1523,12 +1523,12 @@ struct Smt2Backend : public Backend {
|
|||
for (auto &dep : it.second)
|
||||
if (module_deps.count(dep) > 0)
|
||||
goto not_ready_yet;
|
||||
// log("Next in topological sort: %s\n", RTLIL::id2cstr(it.first->name));
|
||||
// log("Next in topological sort: %s\n", log_id(it.first->name));
|
||||
sorted_modules.push_back(it.first);
|
||||
not_ready_yet:;
|
||||
}
|
||||
if (sorted_modules_idx == sorted_modules.size())
|
||||
log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", RTLIL::id2cstr(module_deps.begin()->first->name));
|
||||
log_error("Cyclic dependency between modules found! Cycle includes module %s.\n", log_id(module_deps.begin()->first->name));
|
||||
while (sorted_modules_idx < sorted_modules.size())
|
||||
module_deps.erase(sorted_modules.at(sorted_modules_idx++));
|
||||
}
|
||||
|
@ -1540,7 +1540,7 @@ struct Smt2Backend : public Backend {
|
|||
|
||||
for (auto module : sorted_modules)
|
||||
for (auto cell : module->cells())
|
||||
if (cell->type.in("$allconst", "$allseq"))
|
||||
if (cell->type.in(ID($allconst), ID($allseq)))
|
||||
goto found_forall;
|
||||
if (0) {
|
||||
found_forall:
|
||||
|
|
|
@ -704,8 +704,12 @@ class SmtIo:
|
|||
if msg is not None:
|
||||
print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
|
||||
|
||||
result = ""
|
||||
while result not in ["sat", "unsat"]:
|
||||
if self.forall:
|
||||
result = self.read()
|
||||
while result not in ["sat", "unsat", "unknown"]:
|
||||
print("%s %s: %s" % (self.timestamp(), self.solver, result))
|
||||
result = self.read()
|
||||
else:
|
||||
result = self.read()
|
||||
|
||||
if self.debug_file:
|
||||
|
|
|
@ -219,30 +219,30 @@ struct SmvWorker
|
|||
if (wire->port_input)
|
||||
inputvars.push_back(stringf("%s : unsigned word[%d]; -- %s", cid(wire->name), wire->width, log_id(wire)));
|
||||
|
||||
if (wire->attributes.count("\\init"))
|
||||
assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at("\\init"))));
|
||||
if (wire->attributes.count(ID::init))
|
||||
assignments.push_back(stringf("init(%s) := %s;", lvalue(wire), rvalue(wire->attributes.at(ID::init))));
|
||||
}
|
||||
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
// FIXME: $slice, $concat, $mem
|
||||
|
||||
if (cell->type.in("$assert"))
|
||||
if (cell->type.in(ID($assert)))
|
||||
{
|
||||
SigSpec sig_a = cell->getPort("\\A");
|
||||
SigSpec sig_en = cell->getPort("\\EN");
|
||||
SigSpec sig_a = cell->getPort(ID::A);
|
||||
SigSpec sig_en = cell->getPort(ID::EN);
|
||||
|
||||
invarspecs.push_back(stringf("!bool(%s) | bool(%s);", rvalue(sig_en), rvalue(sig_a)));
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$shl", "$shr", "$sshl", "$sshr", "$shift", "$shiftx"))
|
||||
if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx)))
|
||||
{
|
||||
SigSpec sig_a = cell->getPort("\\A");
|
||||
SigSpec sig_b = cell->getPort("\\B");
|
||||
SigSpec sig_a = cell->getPort(ID::A);
|
||||
SigSpec sig_b = cell->getPort(ID::B);
|
||||
|
||||
int width_y = GetSize(cell->getPort("\\Y"));
|
||||
int width_y = GetSize(cell->getPort(ID::Y));
|
||||
int shift_b_width = GetSize(sig_b);
|
||||
int width_ay = max(GetSize(sig_a), width_y);
|
||||
int width = width_ay;
|
||||
|
@ -254,12 +254,12 @@ struct SmvWorker
|
|||
break;
|
||||
}
|
||||
|
||||
bool signed_a = cell->getParam("\\A_SIGNED").as_bool();
|
||||
bool signed_b = cell->getParam("\\B_SIGNED").as_bool();
|
||||
string op = cell->type.in("$shl", "$sshl") ? "<<" : ">>";
|
||||
bool signed_a = cell->getParam(ID::A_SIGNED).as_bool();
|
||||
bool signed_b = cell->getParam(ID::B_SIGNED).as_bool();
|
||||
string op = cell->type.in(ID($shl), ID($sshl)) ? "<<" : ">>";
|
||||
string expr, expr_a;
|
||||
|
||||
if (cell->type == "$sshr" && signed_a)
|
||||
if (cell->type == ID($sshr) && signed_a)
|
||||
{
|
||||
expr_a = rvalue_s(sig_a, width);
|
||||
expr = stringf("resize(unsigned(%s %s %s), %d)", expr_a.c_str(), op.c_str(), rvalue(sig_b.extract(0, shift_b_width)), width_y);
|
||||
|
@ -268,7 +268,7 @@ struct SmvWorker
|
|||
rvalue(sig_b.extract(shift_b_width, GetSize(sig_b) - shift_b_width)), GetSize(sig_b) - shift_b_width,
|
||||
rvalue(sig_a[GetSize(sig_a)-1]), width_y, width_y, expr.c_str());
|
||||
}
|
||||
else if (cell->type.in("$shift", "$shiftx") && signed_b)
|
||||
else if (cell->type.in(ID($shift), ID($shiftx)) && signed_b)
|
||||
{
|
||||
expr_a = rvalue_u(sig_a, width);
|
||||
|
||||
|
@ -292,7 +292,7 @@ struct SmvWorker
|
|||
}
|
||||
else
|
||||
{
|
||||
if (cell->type.in("$shift", "$shiftx") || !signed_a)
|
||||
if (cell->type.in(ID($shift), ID($shiftx)) || !signed_a)
|
||||
expr_a = rvalue_u(sig_a, width);
|
||||
else
|
||||
expr_a = stringf("resize(unsigned(%s), %d)", rvalue_s(sig_a, width_ay), width);
|
||||
|
@ -303,272 +303,272 @@ struct SmvWorker
|
|||
GetSize(sig_b)-shift_b_width, width_y, expr.c_str());
|
||||
}
|
||||
|
||||
definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
|
||||
definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$not", "$pos", "$neg"))
|
||||
if (cell->type.in(ID($not), ID($pos), ID($neg)))
|
||||
{
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
int width = GetSize(cell->getPort(ID::Y));
|
||||
string expr_a, op;
|
||||
|
||||
if (cell->type == "$not") op = "!";
|
||||
if (cell->type == "$pos") op = "";
|
||||
if (cell->type == "$neg") op = "-";
|
||||
if (cell->type == ID($not)) op = "!";
|
||||
if (cell->type == ID($pos)) op = "";
|
||||
if (cell->type == ID($neg)) op = "-";
|
||||
|
||||
if (cell->getParam("\\A_SIGNED").as_bool())
|
||||
if (cell->getParam(ID::A_SIGNED).as_bool())
|
||||
{
|
||||
definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort("\\Y")),
|
||||
op.c_str(), rvalue_s(cell->getPort("\\A"), width)));
|
||||
definitions.push_back(stringf("%s := unsigned(%s%s);", lvalue(cell->getPort(ID::Y)),
|
||||
op.c_str(), rvalue_s(cell->getPort(ID::A), width)));
|
||||
}
|
||||
else
|
||||
{
|
||||
definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")),
|
||||
op.c_str(), rvalue_u(cell->getPort("\\A"), width)));
|
||||
definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)),
|
||||
op.c_str(), rvalue_u(cell->getPort(ID::A), width)));
|
||||
}
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor"))
|
||||
if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor)))
|
||||
{
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
int width = GetSize(cell->getPort(ID::Y));
|
||||
string expr_a, expr_b, op;
|
||||
|
||||
if (cell->type == "$add") op = "+";
|
||||
if (cell->type == "$sub") op = "-";
|
||||
if (cell->type == "$mul") op = "*";
|
||||
if (cell->type == "$and") op = "&";
|
||||
if (cell->type == "$or") op = "|";
|
||||
if (cell->type == "$xor") op = "xor";
|
||||
if (cell->type == "$xnor") op = "xnor";
|
||||
if (cell->type == ID($add)) op = "+";
|
||||
if (cell->type == ID($sub)) op = "-";
|
||||
if (cell->type == ID($mul)) op = "*";
|
||||
if (cell->type == ID($and)) op = "&";
|
||||
if (cell->type == ID($or)) op = "|";
|
||||
if (cell->type == ID($xor)) op = "xor";
|
||||
if (cell->type == ID($xnor)) op = "xnor";
|
||||
|
||||
if (cell->getParam("\\A_SIGNED").as_bool())
|
||||
if (cell->getParam(ID::A_SIGNED).as_bool())
|
||||
{
|
||||
definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width)));
|
||||
definitions.push_back(stringf("%s := unsigned(%s %s %s);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width)));
|
||||
}
|
||||
else
|
||||
{
|
||||
definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
|
||||
rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width)));
|
||||
definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width)));
|
||||
}
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$div", "$mod"))
|
||||
if (cell->type.in(ID($div), ID($mod)))
|
||||
{
|
||||
int width_y = GetSize(cell->getPort("\\Y"));
|
||||
int width = max(width_y, GetSize(cell->getPort("\\A")));
|
||||
width = max(width, GetSize(cell->getPort("\\B")));
|
||||
int width_y = GetSize(cell->getPort(ID::Y));
|
||||
int width = max(width_y, GetSize(cell->getPort(ID::A)));
|
||||
width = max(width, GetSize(cell->getPort(ID::B)));
|
||||
string expr_a, expr_b, op;
|
||||
|
||||
if (cell->type == "$div") op = "/";
|
||||
if (cell->type == "$mod") op = "mod";
|
||||
if (cell->type == ID($div)) op = "/";
|
||||
if (cell->type == ID($mod)) op = "mod";
|
||||
|
||||
if (cell->getParam("\\A_SIGNED").as_bool())
|
||||
if (cell->getParam(ID::A_SIGNED).as_bool())
|
||||
{
|
||||
definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue_s(cell->getPort("\\A"), width), op.c_str(), rvalue_s(cell->getPort("\\B"), width), width_y));
|
||||
definitions.push_back(stringf("%s := resize(unsigned(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue_s(cell->getPort(ID::A), width), op.c_str(), rvalue_s(cell->getPort(ID::B), width), width_y));
|
||||
}
|
||||
else
|
||||
{
|
||||
definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue_u(cell->getPort("\\A"), width), op.c_str(), rvalue_u(cell->getPort("\\B"), width), width_y));
|
||||
definitions.push_back(stringf("%s := resize(%s %s %s, %d);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue_u(cell->getPort(ID::A), width), op.c_str(), rvalue_u(cell->getPort(ID::B), width), width_y));
|
||||
}
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$eq", "$ne", "$eqx", "$nex", "$lt", "$le", "$ge", "$gt"))
|
||||
if (cell->type.in(ID($eq), ID($ne), ID($eqx), ID($nex), ID($lt), ID($le), ID($ge), ID($gt)))
|
||||
{
|
||||
int width = max(GetSize(cell->getPort("\\A")), GetSize(cell->getPort("\\B")));
|
||||
int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B)));
|
||||
string expr_a, expr_b, op;
|
||||
|
||||
if (cell->type == "$eq") op = "=";
|
||||
if (cell->type == "$ne") op = "!=";
|
||||
if (cell->type == "$eqx") op = "=";
|
||||
if (cell->type == "$nex") op = "!=";
|
||||
if (cell->type == "$lt") op = "<";
|
||||
if (cell->type == "$le") op = "<=";
|
||||
if (cell->type == "$ge") op = ">=";
|
||||
if (cell->type == "$gt") op = ">";
|
||||
if (cell->type == ID($eq)) op = "=";
|
||||
if (cell->type == ID($ne)) op = "!=";
|
||||
if (cell->type == ID($eqx)) op = "=";
|
||||
if (cell->type == ID($nex)) op = "!=";
|
||||
if (cell->type == ID($lt)) op = "<";
|
||||
if (cell->type == ID($le)) op = "<=";
|
||||
if (cell->type == ID($ge)) op = ">=";
|
||||
if (cell->type == ID($gt)) op = ">";
|
||||
|
||||
if (cell->getParam("\\A_SIGNED").as_bool())
|
||||
if (cell->getParam(ID::A_SIGNED).as_bool())
|
||||
{
|
||||
expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\A")), width);
|
||||
expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort("\\B")), width);
|
||||
expr_a = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::A)), width);
|
||||
expr_b = stringf("resize(signed(%s), %d)", rvalue(cell->getPort(ID::B)), width);
|
||||
}
|
||||
else
|
||||
{
|
||||
expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort("\\A")), width);
|
||||
expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort("\\B")), width);
|
||||
expr_a = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::A)), width);
|
||||
expr_b = stringf("resize(%s, %d)", rvalue(cell->getPort(ID::B)), width);
|
||||
}
|
||||
|
||||
definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort("\\Y")),
|
||||
expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort("\\Y"))));
|
||||
definitions.push_back(stringf("%s := resize(word1(%s %s %s), %d);", lvalue(cell->getPort(ID::Y)),
|
||||
expr_a.c_str(), op.c_str(), expr_b.c_str(), GetSize(cell->getPort(ID::Y))));
|
||||
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$reduce_and", "$reduce_or", "$reduce_bool"))
|
||||
if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)))
|
||||
{
|
||||
int width_a = GetSize(cell->getPort("\\A"));
|
||||
int width_y = GetSize(cell->getPort("\\Y"));
|
||||
const char *expr_a = rvalue(cell->getPort("\\A"));
|
||||
const char *expr_y = lvalue(cell->getPort("\\Y"));
|
||||
int width_a = GetSize(cell->getPort(ID::A));
|
||||
int width_y = GetSize(cell->getPort(ID::Y));
|
||||
const char *expr_a = rvalue(cell->getPort(ID::A));
|
||||
const char *expr_y = lvalue(cell->getPort(ID::Y));
|
||||
string expr;
|
||||
|
||||
if (cell->type == "$reduce_and") expr = stringf("%s = !0ub%d_0", expr_a, width_a);
|
||||
if (cell->type == "$reduce_or") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
|
||||
if (cell->type == "$reduce_bool") expr = stringf("%s != 0ub%d_0", expr_a, width_a);
|
||||
if (cell->type == ID($reduce_and)) expr = stringf("%s = !0ub%d_0", expr_a, width_a);
|
||||
if (cell->type == ID($reduce_or)) expr = stringf("%s != 0ub%d_0", expr_a, width_a);
|
||||
if (cell->type == ID($reduce_bool)) expr = stringf("%s != 0ub%d_0", expr_a, width_a);
|
||||
|
||||
definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$reduce_xor", "$reduce_xnor"))
|
||||
if (cell->type.in(ID($reduce_xor), ID($reduce_xnor)))
|
||||
{
|
||||
int width_y = GetSize(cell->getPort("\\Y"));
|
||||
const char *expr_y = lvalue(cell->getPort("\\Y"));
|
||||
int width_y = GetSize(cell->getPort(ID::Y));
|
||||
const char *expr_y = lvalue(cell->getPort(ID::Y));
|
||||
string expr;
|
||||
|
||||
for (auto bit : cell->getPort("\\A")) {
|
||||
for (auto bit : cell->getPort(ID::A)) {
|
||||
if (!expr.empty())
|
||||
expr += " xor ";
|
||||
expr += rvalue(bit);
|
||||
}
|
||||
|
||||
if (cell->type == "$reduce_xnor")
|
||||
if (cell->type == ID($reduce_xnor))
|
||||
expr = "!(" + expr + ")";
|
||||
|
||||
definitions.push_back(stringf("%s := resize(%s, %d);", expr_y, expr.c_str(), width_y));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$logic_and", "$logic_or"))
|
||||
if (cell->type.in(ID($logic_and), ID($logic_or)))
|
||||
{
|
||||
int width_a = GetSize(cell->getPort("\\A"));
|
||||
int width_b = GetSize(cell->getPort("\\B"));
|
||||
int width_y = GetSize(cell->getPort("\\Y"));
|
||||
int width_a = GetSize(cell->getPort(ID::A));
|
||||
int width_b = GetSize(cell->getPort(ID::B));
|
||||
int width_y = GetSize(cell->getPort(ID::Y));
|
||||
|
||||
string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
|
||||
string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort("\\B")), width_b);
|
||||
const char *expr_y = lvalue(cell->getPort("\\Y"));
|
||||
string expr_a = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
|
||||
string expr_b = stringf("(%s != 0ub%d_0)", rvalue(cell->getPort(ID::B)), width_b);
|
||||
const char *expr_y = lvalue(cell->getPort(ID::Y));
|
||||
|
||||
string expr;
|
||||
if (cell->type == "$logic_and") expr = expr_a + " & " + expr_b;
|
||||
if (cell->type == "$logic_or") expr = expr_a + " | " + expr_b;
|
||||
if (cell->type == ID($logic_and)) expr = expr_a + " & " + expr_b;
|
||||
if (cell->type == ID($logic_or)) expr = expr_a + " | " + expr_b;
|
||||
|
||||
definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr.c_str(), width_y));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$logic_not"))
|
||||
if (cell->type.in(ID($logic_not)))
|
||||
{
|
||||
int width_a = GetSize(cell->getPort("\\A"));
|
||||
int width_y = GetSize(cell->getPort("\\Y"));
|
||||
int width_a = GetSize(cell->getPort(ID::A));
|
||||
int width_y = GetSize(cell->getPort(ID::Y));
|
||||
|
||||
string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort("\\A")), width_a);
|
||||
const char *expr_y = lvalue(cell->getPort("\\Y"));
|
||||
string expr_a = stringf("(%s = 0ub%d_0)", rvalue(cell->getPort(ID::A)), width_a);
|
||||
const char *expr_y = lvalue(cell->getPort(ID::Y));
|
||||
|
||||
definitions.push_back(stringf("%s := resize(word1(%s), %d);", expr_y, expr_a.c_str(), width_y));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$mux", "$pmux"))
|
||||
if (cell->type.in(ID($mux), ID($pmux)))
|
||||
{
|
||||
int width = GetSize(cell->getPort("\\Y"));
|
||||
SigSpec sig_a = cell->getPort("\\A");
|
||||
SigSpec sig_b = cell->getPort("\\B");
|
||||
SigSpec sig_s = cell->getPort("\\S");
|
||||
int width = GetSize(cell->getPort(ID::Y));
|
||||
SigSpec sig_a = cell->getPort(ID::A);
|
||||
SigSpec sig_b = cell->getPort(ID::B);
|
||||
SigSpec sig_s = cell->getPort(ID::S);
|
||||
|
||||
string expr;
|
||||
for (int i = 0; i < GetSize(sig_s); i++)
|
||||
expr += stringf("bool(%s) ? %s : ", rvalue(sig_s[i]), rvalue(sig_b.extract(i*width, width)));
|
||||
expr += rvalue(sig_a);
|
||||
|
||||
definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort("\\Y")), expr.c_str()));
|
||||
definitions.push_back(stringf("%s := %s;", lvalue(cell->getPort(ID::Y)), expr.c_str()));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$dff")
|
||||
if (cell->type == ID($dff))
|
||||
{
|
||||
vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort("\\Q")), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
|
||||
assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort("\\Q")), rvalue(cell->getPort("\\D"))));
|
||||
vars.push_back(stringf("%s : unsigned word[%d]; -- %s", lvalue(cell->getPort(ID::Q)), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))));
|
||||
assignments.push_back(stringf("next(%s) := %s;", lvalue(cell->getPort(ID::Q)), rvalue(cell->getPort(ID::D))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_BUF_", "$_NOT_"))
|
||||
if (cell->type.in(ID($_BUF_), ID($_NOT_)))
|
||||
{
|
||||
string op = cell->type == "$_NOT_" ? "!" : "";
|
||||
definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort("\\Y")), op.c_str(), rvalue(cell->getPort("\\A"))));
|
||||
string op = cell->type == ID($_NOT_) ? "!" : "";
|
||||
definitions.push_back(stringf("%s := %s%s;", lvalue(cell->getPort(ID::Y)), op.c_str(), rvalue(cell->getPort(ID::A))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type.in("$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_", "$_ANDNOT_", "$_ORNOT_"))
|
||||
if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_)))
|
||||
{
|
||||
string op;
|
||||
|
||||
if (cell->type.in("$_AND_", "$_NAND_", "$_ANDNOT_")) op = "&";
|
||||
if (cell->type.in("$_OR_", "$_NOR_", "$_ORNOT_")) op = "|";
|
||||
if (cell->type.in("$_XOR_")) op = "xor";
|
||||
if (cell->type.in("$_XNOR_")) op = "xnor";
|
||||
if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_ANDNOT_))) op = "&";
|
||||
if (cell->type.in(ID($_OR_), ID($_NOR_), ID($_ORNOT_))) op = "|";
|
||||
if (cell->type.in(ID($_XOR_))) op = "xor";
|
||||
if (cell->type.in(ID($_XNOR_))) op = "xnor";
|
||||
|
||||
if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
|
||||
definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
|
||||
if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_)))
|
||||
definitions.push_back(stringf("%s := %s %s (!%s);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
|
||||
else
|
||||
if (cell->type.in("$_NAND_", "$_NOR_"))
|
||||
definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
|
||||
if (cell->type.in(ID($_NAND_), ID($_NOR_)))
|
||||
definitions.push_back(stringf("%s := !(%s %s %s);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
|
||||
else
|
||||
definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), op.c_str(), rvalue(cell->getPort("\\B"))));
|
||||
definitions.push_back(stringf("%s := %s %s %s;", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::A)), op.c_str(), rvalue(cell->getPort(ID::B))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_MUX_")
|
||||
if (cell->type == ID($_MUX_))
|
||||
{
|
||||
definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
|
||||
definitions.push_back(stringf("%s := bool(%s) ? %s : %s;", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_NMUX_")
|
||||
if (cell->type == ID($_NMUX_))
|
||||
{
|
||||
definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\S")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\A"))));
|
||||
definitions.push_back(stringf("%s := !(bool(%s) ? %s : %s);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::S)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::A))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_AOI3_")
|
||||
if (cell->type == ID($_AOI3_))
|
||||
{
|
||||
definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
|
||||
definitions.push_back(stringf("%s := !((%s & %s) | %s);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_OAI3_")
|
||||
if (cell->type == ID($_OAI3_))
|
||||
{
|
||||
definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C"))));
|
||||
definitions.push_back(stringf("%s := !((%s | %s) & %s);", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_AOI4_")
|
||||
if (cell->type == ID($_AOI4_))
|
||||
{
|
||||
definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
|
||||
definitions.push_back(stringf("%s := !((%s & %s) | (%s & %s));", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
|
||||
continue;
|
||||
}
|
||||
|
||||
if (cell->type == "$_OAI4_")
|
||||
if (cell->type == ID($_OAI4_))
|
||||
{
|
||||
definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort("\\Y")),
|
||||
rvalue(cell->getPort("\\A")), rvalue(cell->getPort("\\B")), rvalue(cell->getPort("\\C")), rvalue(cell->getPort("\\D"))));
|
||||
definitions.push_back(stringf("%s := !((%s | %s) & (%s | %s));", lvalue(cell->getPort(ID::Y)),
|
||||
rvalue(cell->getPort(ID::A)), rvalue(cell->getPort(ID::B)), rvalue(cell->getPort(ID::C)), rvalue(cell->getPort(ID::D))));
|
||||
continue;
|
||||
}
|
||||
|
||||
|
|
|
@ -70,14 +70,13 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
|
|||
idict<IdString, 1> inums;
|
||||
int cell_counter = 0, conn_counter = 0, nc_counter = 0;
|
||||
|
||||
for (auto &cell_it : module->cells_)
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
RTLIL::Cell *cell = cell_it.second;
|
||||
f << stringf("X%d", cell_counter++);
|
||||
|
||||
std::vector<RTLIL::SigSpec> port_sigs;
|
||||
|
||||
if (design->modules_.count(cell->type) == 0)
|
||||
if (design->module(cell->type) == nullptr)
|
||||
{
|
||||
log_warning("no (blackbox) module for cell type `%s' (%s.%s) found! Guessing order of ports.\n",
|
||||
log_id(cell->type), log_id(module), log_id(cell));
|
||||
|
@ -88,11 +87,10 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
|
|||
}
|
||||
else
|
||||
{
|
||||
RTLIL::Module *mod = design->modules_.at(cell->type);
|
||||
RTLIL::Module *mod = design->module(cell->type);
|
||||
|
||||
std::vector<RTLIL::Wire*> ports;
|
||||
for (auto wire_it : mod->wires_) {
|
||||
RTLIL::Wire *wire = wire_it.second;
|
||||
for (auto wire : mod->wires()) {
|
||||
if (wire->port_id == 0)
|
||||
continue;
|
||||
while (int(ports.size()) < wire->port_id)
|
||||
|
@ -202,16 +200,15 @@ struct SpiceBackend : public Backend {
|
|||
extra_args(f, filename, args, argidx);
|
||||
|
||||
if (top_module_name.empty())
|
||||
for (auto & mod_it:design->modules_)
|
||||
if (mod_it.second->get_bool_attribute("\\top"))
|
||||
top_module_name = mod_it.first.str();
|
||||
for (auto module : design->modules())
|
||||
if (module->get_bool_attribute(ID::top))
|
||||
top_module_name = module->name.str();
|
||||
|
||||
*f << stringf("* SPICE netlist generated by %s\n", yosys_version_str);
|
||||
*f << stringf("\n");
|
||||
|
||||
for (auto module_it : design->modules_)
|
||||
for (auto module : design->modules())
|
||||
{
|
||||
RTLIL::Module *module = module_it.second;
|
||||
if (module->get_blackbox_attribute())
|
||||
continue;
|
||||
|
||||
|
@ -226,8 +223,7 @@ struct SpiceBackend : public Backend {
|
|||
}
|
||||
|
||||
std::vector<RTLIL::Wire*> ports;
|
||||
for (auto wire_it : module->wires_) {
|
||||
RTLIL::Wire *wire = wire_it.second;
|
||||
for (auto wire : module->wires()) {
|
||||
if (wire->port_id == 0)
|
||||
continue;
|
||||
while (int(ports.size()) < wire->port_id)
|
||||
|
|
File diff suppressed because it is too large
Load diff
Loading…
Add table
Add a link
Reference in a new issue