mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-19 15:26:29 +00:00
Code Activity

Move rename logic to abc_ops_reintegrate

Browse source
This commit is contained in:
Lofty 2026-06-10 10:01:25 +01:00
parent c96d7bc998
commit 091d2a7814
11 changed files with 208 additions and 281 deletions
Download patch file Download diff file Expand all files Collapse all files

210
frontends/aiger/aigerparse.cc
View file

@ -55,17 +55,6 @@ inline int32_t from_big_endian(int32_t i32) {
#define log_debug2(...) ;
//#define log_debug2(...) log_debug(__VA_ARGS__)
static int decimal_digits(uint32_t n) {
static uint32_t digit_cutoff[9] = {
10, 100, 1000, 10000, 100000,
1000000, 10000000, 100000000, 1000000000
};
for (int i = 0; i < 9; ++i) {
if (n < digit_cutoff[i]) return i + 1;
}
return 10;
}
struct ConstEvalAig
{
RTLIL::Module *module;
@ -218,8 +207,8 @@ eval_end:
}
};
AigerReader::AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename, bool wideports)
: design(design), f(f), clk_name(clk_name), map_filename(map_filename), wideports(wideports), aiger_autoidx(autoidx++)
AigerReader::AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename)
: design(design), f(f), clk_name(clk_name), map_filename(map_filename), aiger_autoidx(autoidx++)
{
module = new RTLIL::Module;
module->name = module_name;
@ -257,6 +246,9 @@ end_of_header:
log_debug("M=%u I=%u L=%u O=%u A=%u B=%u C=%u J=%u F=%u\n", M, I, L, O, A, B, C, J, F);
design->scratchpad_set_int("read_aiger.inputs", I);
design->scratchpad_set_int("read_aiger.outputs", O);
line_count = 1;
piNum = 0;
flopNum = 0;
@ -390,6 +382,9 @@ void AigerReader::parse_xaiger()
log_debug("M=%u I=%u L=%u O=%u A=%u\n", M, I, L, O, A);
design->scratchpad_set_int("read_aiger.inputs", I);
design->scratchpad_set_int("read_aiger.outputs", O);
line_count = 1;
piNum = 0;
flopNum = 0;
@ -607,13 +602,12 @@ void AigerReader::parse_aiger_ascii()
unsigned l1, l2, l3;
// Parse inputs
int digits = decimal_digits(I);
for (unsigned i = 1; i <= I; ++i, ++line_count) {
if (!(f >> l1))
log_error("Line %u cannot be interpreted as an input!\n", line_count);
log_debug2("%d is an input\n", l1);
log_assert(!(l1 & 1)); // Inputs can't be inverted
RTLIL::Wire *wire = module->addWire(stringf("$i%0*d", digits, l1 >> 1));
RTLIL::Wire *wire = module->addWire(stringf("$aiger$i%d", l1 >> 1));
wire->port_input = true;
module->connect(createWireIfNotExists(module, l1), wire);
inputs.push_back(wire);
@ -629,13 +623,13 @@ void AigerReader::parse_aiger_ascii()
clk_wire->port_input = true;
clk_wire->port_output = false;
}
digits = decimal_digits(L);
for (unsigned i = 0; i < L; ++i, ++line_count) {
if (!(f >> l1 >> l2))
log_error("Line %u cannot be interpreted as a latch!\n", line_count);
log_debug2("%d %d is a latch\n", l1, l2);
log_assert(!(l1 & 1));
RTLIL::Wire *q_wire = module->addWire(stringf("$l%0*d", digits, l1 >> 1));
RTLIL::Wire *q_wire = module->addWire(stringf("$aiger$l%d", l1 >> 1));
module->connect(createWireIfNotExists(module, l1), q_wire);
RTLIL::Wire *d_wire = createWireIfNotExists(module, l2);
@ -667,14 +661,13 @@ void AigerReader::parse_aiger_ascii()
}
// Parse outputs
digits = decimal_digits(O);
for (unsigned i = 0; i < O; ++i, ++line_count) {
if (!(f >> l1))
log_error("Line %u cannot be interpreted as an output!\n", line_count);
std::getline(f, line); // Ignore up to start of next line
log_debug2("%d is an output\n", l1);
RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
RTLIL::Wire *wire = module->addWire(stringf("$aiger$o%d", i));
wire->port_output = true;
module->connect(wire, createWireIfNotExists(module, l1));
outputs.push_back(wire);
@ -737,10 +730,9 @@ void AigerReader::parse_aiger_binary()
log_error("Binary AIGER input is malformed: maximum variable index M is %u, but number of inputs, latches and AND gates adds up to %u.\n", M, I + L + A);
// Parse inputs
int digits = decimal_digits(I);
for (unsigned i = 1; i <= I; ++i) {
log_debug2("%d is an input\n", i);
RTLIL::Wire *wire = module->addWire(stringf("$i%0*d", digits, i));
RTLIL::Wire *wire = module->addWire(stringf("$aiger$i%d", i));
wire->port_input = true;
module->connect(createWireIfNotExists(module, i << 1), wire);
inputs.push_back(wire);
@ -756,13 +748,13 @@ void AigerReader::parse_aiger_binary()
clk_wire->port_input = true;
clk_wire->port_output = false;
}
digits = decimal_digits(L);
l1 = (I+1) * 2;
for (unsigned i = 0; i < L; ++i, ++line_count, l1 += 2) {
if (!(f >> l2))
log_error("Line %u cannot be interpreted as a latch!\n", line_count);
log_debug("%d %d is a latch\n", l1, l2);
RTLIL::Wire *q_wire = module->addWire(stringf("$l%0*d", digits, l1 >> 1));
RTLIL::Wire *q_wire = module->addWire(stringf("$aiger$l%d", l1 >> 1));
module->connect(createWireIfNotExists(module, l1), q_wire);
RTLIL::Wire *d_wire = createWireIfNotExists(module, l2);
@ -794,14 +786,13 @@ void AigerReader::parse_aiger_binary()
}
// Parse outputs
digits = decimal_digits(O);
for (unsigned i = 0; i < O; ++i, ++line_count) {
if (!(f >> l1))
log_error("Line %u cannot be interpreted as an output!\n", line_count);
std::getline(f, line); // Ignore up to start of next line
log_debug2("%d is an output\n", l1);
RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
RTLIL::Wire *wire = module->addWire(stringf("$aiger$o%d", i));
wire->port_output = true;
module->connect(wire, createWireIfNotExists(module, l1));
outputs.push_back(wire);
@ -884,163 +875,10 @@ void AigerReader::post_process()
q->attributes[ID::init] = initial_state[i];
}
dict<RTLIL::IdString, std::pair<int,int>> wideports_cache;
if (!map_filename.empty()) {
std::ifstream mf(map_filename);
std::string type, symbol;
int variable, index;
while (mf >> type >> variable >> index >> symbol) {
RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
if (type == "input") {
log_assert(static_cast<unsigned>(variable) < inputs.size());
RTLIL::Wire* wire = inputs[variable];
log_assert(wire);
log_assert(wire->port_input);
log_debug("Renaming input %s", wire);
RTLIL::Wire *existing = nullptr;
if (index == 0) {
// Cope with the fact that a CI might be identical
// to a PI (necessary due to ABC); in those cases
// simply connect the latter to the former
existing = module->wire(escaped_s);
if (!existing)
module->rename(wire, escaped_s);
else {
wire->port_input = false;
module->connect(wire, existing);
}
log_debug(" -> %s\n", escaped_s.unescape());
}
else {
RTLIL::IdString indexed_name = stringf("%s[%d]", escaped_s, index);
existing = module->wire(indexed_name);
if (!existing)
module->rename(wire, indexed_name);
else {
module->connect(wire, existing);
wire->port_input = false;
}
log_debug(" -> %s\n", indexed_name.unescape());
}
if (wideports && !existing) {
auto r = wideports_cache.insert(escaped_s);
if (r.second) {
r.first->second.first = index;
r.first->second.second = index;
}
else {
r.first->second.first = std::min(r.first->second.first, index);
r.first->second.second = std::max(r.first->second.second, index);
}
}
}
else if (type == "output") {
log_assert(static_cast<unsigned>(variable + co_count) < outputs.size());
RTLIL::Wire* wire = outputs[variable + co_count];
log_assert(wire);
log_assert(wire->port_output);
log_debug("Renaming output %s", wire);
RTLIL::Wire *existing;
if (index == 0) {
// Cope with the fact that a CO might be identical
// to a PO (necessary due to ABC); in those cases
// simply connect the latter to the former
existing = module->wire(escaped_s);
if (!existing)
module->rename(wire, escaped_s);
else {
wire->port_output = false;
existing->port_output = true;
module->connect(wire, existing);
wire = existing;
}
log_debug(" -> %s\n", escaped_s.unescape());
}
else {
RTLIL::IdString indexed_name = stringf("%s[%d]", escaped_s, index);
existing = module->wire(indexed_name);
if (!existing)
module->rename(wire, indexed_name);
else {
wire->port_output = false;
existing->port_output = true;
module->connect(wire, existing);
}
log_debug(" -> %s\n", indexed_name.unescape());
}
if (wideports && !existing) {
auto r = wideports_cache.insert(escaped_s);
if (r.second) {
r.first->second.first = index;
r.first->second.second = index;
}
else {
r.first->second.first = std::min(r.first->second.first, index);
r.first->second.second = std::max(r.first->second.second, index);
}
}
}
else if (type == "box") {
RTLIL::Cell* cell = module->cell(stringf("$box%d", variable));
if (!cell)
log_debug("Box %d (%s) no longer exists.\n", variable, escaped_s.unescape());
else
module->rename(cell, escaped_s);
}
else
log_error("Symbol type '%s' not recognised.\n", type);
}
}
for (auto &wp : wideports_cache) {
auto name = wp.first;
int min = wp.second.first;
int max = wp.second.second;
if (min == 0 && max == 0)
continue;
RTLIL::Wire *wire = module->wire(name);
if (wire)
module->rename(wire, RTLIL::escape_id(stringf("%s[%d]", name, 0)));
// Do not make ports with a mix of input/output into
// wide ports
bool port_input = false, port_output = false;
for (int i = min; i <= max; i++) {
RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
RTLIL::Wire *other_wire = module->wire(other_name);
if (other_wire) {
port_input = port_input || other_wire->port_input;
port_output = port_output || other_wire->port_output;
}
}
wire = module->addWire(name, max-min+1);
wire->start_offset = min;
wire->port_input = port_input;
wire->port_output = port_output;
for (int i = min; i <= max; i++) {
RTLIL::IdString other_name = stringf("%s[%d]", name, i);
RTLIL::Wire *other_wire = module->wire(other_name);
if (other_wire) {
other_wire->port_input = false;
other_wire->port_output = false;
if (wire->port_input)
module->connect(other_wire, SigSpec(wire, i-min));
else
module->connect(SigSpec(wire, i-min), other_wire);
}
}
}
module->fixup_ports();
design->scratchpad_set_int("read_aiger.co_count", co_count);
// Insert into a new (temporary) design so that "clean" will only
// operate (and run checks on) this one module
RTLIL::Design *mapped_design = new RTLIL::Design;
@ -1081,10 +919,6 @@ struct AigerFrontend : public Frontend {
log(" -map <filename>\n");
log(" read file with port and latch symbols\n");
log("\n");
log(" -wideports\n");
log(" merge ports that match the pattern 'name[int]' into a single\n");
log(" multi-bit port 'name'\n");
log("\n");
log(" -xaiger\n");
log(" read XAIGER extensions\n");
log("\n");
@ -1096,7 +930,7 @@ struct AigerFrontend : public Frontend {
RTLIL::IdString clk_name;
RTLIL::IdString module_name;
std::string map_filename;
bool wideports = false, xaiger = false;
bool xaiger = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@ -1113,10 +947,6 @@ struct AigerFrontend : public Frontend {
map_filename = args[++argidx];
continue;
}
if (arg == "-wideports") {
wideports = true;
continue;
}
if (arg == "-xaiger") {
xaiger = true;
continue;
@ -1139,7 +969,7 @@ struct AigerFrontend : public Frontend {
#endif
}
AigerReader reader(design, *f, module_name, clk_name, map_filename, wideports);
AigerReader reader(design, *f, module_name, clk_name, map_filename);
if (xaiger)
reader.parse_xaiger();
else

3
frontends/aiger/aigerparse.h
View file

@ -32,7 +32,6 @@ struct AigerReader
RTLIL::IdString clk_name;
RTLIL::Module *module;
std::string map_filename;
bool wideports;
const int aiger_autoidx;
unsigned M, I, L, O, A;
@ -47,7 +46,7 @@ struct AigerReader
std::vector<RTLIL::Cell*> boxes;
std::vector<int> mergeability, initial_state;
AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename, bool wideports);
AigerReader(RTLIL::Design *design, std::istream &f, RTLIL::IdString module_name, RTLIL::IdString clk_name, std::string map_filename);
void parse_aiger();
void parse_xaiger();
void parse_aiger_ascii();

8
passes/techmap/abc9.cc
View file

@ -377,8 +377,8 @@ struct Abc9Pass : public ScriptPass
run(" abc9_ops -write_box <abc-temp-dir>/input.box", "(skip if '-box')");
run(" write_xaiger -map <abc-temp-dir>/input.sym [-dff] <abc-temp-dir>/input.xaig");
run(" abc9_exe [options] -cwd <abc-temp-dir> -lut [<abc-temp-dir>/input.lut] -box [<abc-temp-dir>/input.box]");
run(" read_aiger -xaiger -wideports -module_name <module-name>$abc9 -map <abc-temp-dir>/input.sym <abc-temp-dir>/output.aig");
run(" abc_ops_reintegrate [-dff]");
run(" read_aiger -xaiger -module_name <module-name>$abc9 <abc-temp-dir>/output.aig");
run(" abc_ops_reintegrate -map <abc-temp-dir>/input.sym [-dff]");
}
else {
auto selected_modules = active_design->selected_modules();
@ -429,8 +429,8 @@ struct Abc9Pass : public ScriptPass
else
abc9_exe_cmd += stringf(" -box %s", box_file);
run_nocheck(abc9_exe_cmd);
run_nocheck(stringf("read_aiger -xaiger -wideports -module_name %s$abc9 -map %s/input.sym %s/output.aig", mod, tempdir_name, tempdir_name));
run_nocheck(stringf("abc_ops_reintegrate %s", dff_mode ? "-dff" : ""));
run_nocheck(stringf("read_aiger -xaiger -module_name %s$abc9 %s/output.aig", mod, tempdir_name));
run_nocheck(stringf("abc_ops_reintegrate -map %s/input.sym %s", tempdir_name, dff_mode ? "-dff" : ""));
}
else
log("Don't call ABC as there is nothing to map.\n");

177
passes/techmap/abc_ops_reintegrate.cc
View file

@ -34,7 +34,7 @@ inline std::string remap_name(RTLIL::IdString abc9_name)
return stringf("$abc$%d$%s", map_autoidx, abc9_name.c_str()+1);
}
void reintegrate(RTLIL::Module *module, bool dff_mode)
void reintegrate(RTLIL::Module *module, bool dff_mode, std::string map_filename)
{
auto design = module->design;
log_assert(design);
@ -45,6 +45,167 @@ void reintegrate(RTLIL::Module *module, bool dff_mode)
if (mapped_mod == NULL)
log_error("ABC output file does not contain a module `%s$abc'.\n", module);
int input_count = design->scratchpad_get_int("read_aiger.inputs", 0);
int output_count = design->scratchpad_get_int("read_aiger.outputs", 0);
int co_count = design->scratchpad_get_int("read_aiger.co_count", 0);
dict<RTLIL::IdString, std::pair<int,int>> wideports_cache;
if (!map_filename.empty()) {
std::ifstream mf(map_filename);
std::string type, symbol;
int variable, index;
while (mf >> type >> variable >> index >> symbol) {
RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
if (type == "input") {
log_assert(variable < input_count);
RTLIL::Wire* wire = mapped_mod->wire(stringf("$aiger$i%d", variable + 1));
log_assert(wire);
log_assert(wire->port_input);
log_debug("Renaming input %s", wire);
RTLIL::Wire *existing = nullptr;
if (index == 0) {
// Cope with the fact that a CI might be identical
// to a PI (necessary due to ABC); in those cases
// simply connect the latter to the former
existing = mapped_mod->wire(escaped_s);
if (!existing)
mapped_mod->rename(wire, escaped_s);
else {
wire->port_input = false;
mapped_mod->connect(wire, existing);
}
log_debug(" -> %s\n", escaped_s);
}
else {
RTLIL::IdString indexed_name = stringf("%s[%d]", escaped_s, index);
existing = mapped_mod->wire(indexed_name);
if (!existing)
mapped_mod->rename(wire, indexed_name);
else {
mapped_mod->connect(wire, existing);
wire->port_input = false;
}
log_debug(" -> %s\n", indexed_name);
}
if (!existing) {
auto r = wideports_cache.insert(escaped_s);
if (r.second) {
r.first->second.first = index;
r.first->second.second = index;
}
else {
r.first->second.first = std::min(r.first->second.first, index);
r.first->second.second = std::max(r.first->second.second, index);
}
}
}
else if (type == "output") {
log_assert(variable + co_count < output_count);
RTLIL::Wire* wire = mapped_mod->wire(stringf("$aiger$o%d", variable + co_count));
log_assert(wire);
log_assert(wire->port_output);
log_debug("Renaming output %s", wire);
RTLIL::Wire *existing;
if (index == 0) {
// Cope with the fact that a CO might be identical
// to a PO (necessary due to ABC); in those cases
// simply connect the latter to the former
existing = mapped_mod->wire(escaped_s);
if (!existing)
mapped_mod->rename(wire, escaped_s);
else {
wire->port_output = false;
existing->port_output = true;
mapped_mod->connect(wire, existing);
wire = existing;
}
log_debug(" -> %s\n", escaped_s);
}
else {
RTLIL::IdString indexed_name = stringf("%s[%d]", escaped_s, index);
existing = mapped_mod->wire(indexed_name);
if (!existing)
mapped_mod->rename(wire, indexed_name);
else {
wire->port_output = false;
existing->port_output = true;
mapped_mod->connect(wire, existing);
}
log_debug(" -> %s\n", indexed_name);
}
if (!existing) {
auto r = wideports_cache.insert(escaped_s);
if (r.second) {
r.first->second.first = index;
r.first->second.second = index;
}
else {
r.first->second.first = std::min(r.first->second.first, index);
r.first->second.second = std::max(r.first->second.second, index);
}
}
}
else if (type == "box") {
RTLIL::Cell* cell = mapped_mod->cell(stringf("$box%d", variable));
if (!cell)
log_debug("Box %d (%s) no longer exists.\n", variable, escaped_s.unescape());
else
mapped_mod->rename(cell, escaped_s);
}
else
log_error("Symbol type '%s' not recognised.\n", type);
}
}
for (auto &wp : wideports_cache) {
auto name = wp.first;
int min = wp.second.first;
int max = wp.second.second;
if (min == 0 && max == 0)
continue;
RTLIL::Wire *wire = mapped_mod->wire(name);
if (wire)
mapped_mod->rename(wire, RTLIL::escape_id(stringf("%s[%d]", name, 0)));
// Do not make ports with a mix of input/output into
// wide ports
bool port_input = false, port_output = false;
for (int i = min; i <= max; i++) {
RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
RTLIL::Wire *other_wire = mapped_mod->wire(other_name);
if (other_wire) {
port_input = port_input || other_wire->port_input;
port_output = port_output || other_wire->port_output;
}
}
wire = mapped_mod->addWire(name, max-min+1);
wire->start_offset = min;
wire->port_input = port_input;
wire->port_output = port_output;
for (int i = min; i <= max; i++) {
RTLIL::IdString other_name = stringf("%s[%d]", name, i);
RTLIL::Wire *other_wire = mapped_mod->wire(other_name);
if (other_wire) {
other_wire->port_input = false;
other_wire->port_output = false;
if (wire->port_input)
mapped_mod->connect(other_wire, SigSpec(wire, i-min));
else
mapped_mod->connect(SigSpec(wire, i-min), other_wire);
}
}
}
mapped_mod->fixup_ports();
for (auto w : mapped_mod->wires()) {
auto nw = module->addWire(remap_name(w->name), GetSize(w));
nw->start_offset = w->start_offset;
@ -475,12 +636,20 @@ struct AbcOpsReintegratePass : public Pass {
log("by first recovering ABC9 boxes, and then stitching in the remaining\n");
log("primary inputs and outputs.\n");
log("\n");
log(" -dff\n");
log(" consider flop cells (those instantiating modules marked with\n");
log(" (* abc9_flop *)) during -prep_{delays,xaiger,box}.\n");
log("\n");
log(" -map <filename>\n");
log(" read file with port and latch symbols\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
log_header(design, "Executing ABC_OPS_REINTEGRATE pass (reintegrate ABC mapped design into module).\n");
bool dff_mode = false;
std::string map_filename;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@ -489,6 +658,10 @@ struct AbcOpsReintegratePass : public Pass {
dff_mode = true;
continue;
}
if (map_filename.empty() && arg == "-map" && argidx+1 < args.size()) {
map_filename = args[++argidx];
continue;
}
}
extra_args(args, argidx, design);
@ -501,7 +674,7 @@ struct AbcOpsReintegratePass : public Pass {
if (!design->selected_whole_module(mod))
log_error("Can't handle partially selected module %s!\n", mod);
reintegrate(mod, dff_mode);
reintegrate(mod, dff_mode, map_filename);
}
}
} AbcOpsReintegratePass;

36
tests/aiger/neg.ys
View file

@ -1,36 +0,0 @@
read_verilog <<EOT
module top(input [31:-32] a, input [-65:-128] b, output [128:65] c);
assign c = a & b;
endmodule
EOT
select -assert-count 1 i:a
select -assert-count 1 i:b
select -assert-count 1 o:c
select -assert-count 3 x:* s:64 %i
design -save read
!rm -rf neg.out
!mkdir neg.out
simplemap
write_aiger -map neg.out/neg.map neg.out/neg.aig
design -reset
read_aiger -wideports -map neg.out/neg.map neg.out/neg.aig
select -assert-count 1 i:a
select -assert-count 1 i:b
select -assert-count 1 o:c
select -assert-count 3 x:* s:64 %i
design -load read
!rm -rf neg.out
!mkdir neg.out
simplemap
write_xaiger -map neg.out/neg.map neg.out/neg.aig
design -reset
read_aiger -wideports -map neg.out/neg.map neg.out/neg.aig
select -assert-count 1 i:a
select -assert-count 1 i:b
select -assert-count 1 o:c
select -assert-count 3 x:* s:64 %i

4
tests/arch/analogdevices/logic.ys
View file

@ -5,7 +5,7 @@ equiv_opt -assert -map +/analogdevices/cells_sim.v synth_analogdevices -noiopad
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT1
select -assert-count 6 t:LUT2
select -assert-count 4 t:LUT1
select -assert-count 3 t:LUT2
select -assert-count 2 t:LUT4
select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D

4
tests/arch/gowin/logic.ys
View file

@ -5,8 +5,8 @@ equiv_opt -assert -map +/gowin/cells_sim.v synth_gowin # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT1
select -assert-count 6 t:LUT2
select -assert-count 4 t:LUT1
select -assert-count 3 t:LUT2
select -assert-count 2 t:LUT4
select -assert-count 8 t:IBUF
select -assert-count 10 t:OBUF

4
tests/arch/intel_alm/logic.ys
View file

@ -5,8 +5,8 @@ equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cycl
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:MISTRAL_NOT
select -assert-count 6 t:MISTRAL_ALUT2
select -assert-count 4 t:MISTRAL_NOT
select -assert-count 3 t:MISTRAL_ALUT2
select -assert-count 2 t:MISTRAL_ALUT4
select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D

4
tests/arch/quicklogic/pp3/logic.ys
View file

@ -5,8 +5,8 @@ equiv_opt -assert -map +/quicklogic/pp3/cells_sim.v -map +/quicklogic/common/cel
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:LUT1
select -assert-count 6 t:LUT2
select -assert-count 4 t:LUT1
select -assert-count 3 t:LUT2
select -assert-count 2 t:LUT3
select -assert-count 8 t:inpad
select -assert-count 10 t:outpad

12
tests/various/abc9.v
View file

@ -1,15 +1,3 @@
module abc9_test027(output reg o);
initial o = 1'b0;
always @*
o <= ~o;
endmodule
module abc9_test028(input i, output o);
wire w;
unknown u(~i, w);
unknown2 u2(w, o);
endmodule
module abc9_test032(input clk, d, r, output reg q);
initial q = 1'b0;
always @(negedge clk or negedge r)

27
tests/various/abc9.ys
View file

@ -1,31 +1,4 @@
read_verilog abc9.v
design -save read
hierarchy -top abc9_test027
proc
design -save gold
abc9 -lut 4
check
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top abc9_test028
proc
abc9 -lut 4
select -assert-count 1 t:$lut r:LUT=2'b01 r:WIDTH=1 %i %i
select -assert-count 1 t:unknown
select -assert-none t:$lut t:unknown %% t: %D
design -load read
hierarchy -top abc9_test032
proc
clk2fflogic