diff --git a/README.md b/README.md index d9989eb29..56f428548 100644 --- a/README.md +++ b/README.md @@ -405,6 +405,23 @@ Verilog Attributes and non-standard features blackboxes and whiteboxes. Use ``read_verilog -specify`` to enable this functionality. (By default specify .. endspecify blocks are ignored.) +- The module attribute ``abc_box_id`` specifies a positive integer linking a + blackbox or whitebox definition to a corresponding entry in a `abc9` + box-file. + +- The port attribute ``abc_scc_break`` indicates a module input port that will + be treated as a primary output during `abc9` techmapping. Doing so eliminates + the possibility of a strongly-connected component (i.e. a combinatorial loop) + existing. Typically, this is specified for sequential inputs on otherwise + combinatorial boxes -- for example, applying ``abc_scc_break`` onto the `D` + port of a LUTRAM cell prevents `abc9` from interpreting any `Q` -> `D` paths + as a combinatorial loop. + +- The port attribute ``abc_carry`` marks the carry-in (if an input port) and + carry-out (if output port) ports of a box. This information is necessary for + `abc9` to preserve the integrity of carry-chains. Specifying this attribute + onto a bus port will affect only its most significant bit. + Non-standard or SystemVerilog features for formal verification ============================================================== diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 5e12e9a34..77d0e94c2 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -326,7 +326,6 @@ struct XAigerWriter #endif log_assert(no_loops); - pool seen_boxes; for (auto cell_name : toposort.sorted) { RTLIL::Cell *cell = module->cell(cell_name); log_assert(cell); @@ -335,47 +334,6 @@ struct XAigerWriter if (!box_module || !box_module->attributes.count("\\abc_box_id")) continue; - if (seen_boxes.insert(cell->type).second) { - auto it = box_module->attributes.find("\\abc_carry"); - if (it != box_module->attributes.end()) { - RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr; - auto carry_in_out = it->second.decode_string(); - auto pos = carry_in_out.find(','); - if (pos == std::string::npos) - log_error("'abc_carry' attribute on module '%s' does not contain ','.\n", log_id(cell->type)); - auto carry_in_name = RTLIL::escape_id(carry_in_out.substr(0, pos)); - carry_in = box_module->wire(carry_in_name); - if (!carry_in || !carry_in->port_input) - log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an input port.\n", log_id(cell->type), carry_in_name.c_str()); - - auto carry_out_name = RTLIL::escape_id(carry_in_out.substr(pos+1)); - carry_out = box_module->wire(carry_out_name); - if (!carry_out || !carry_out->port_output) - log_error("'abc_carry' on module '%s' contains '%s' which does not exist or is not an output port.\n", log_id(cell->type), carry_out_name.c_str()); - - auto &ports = box_module->ports; - for (auto jt = ports.begin(); jt != ports.end(); ) { - RTLIL::Wire* w = box_module->wire(*jt); - log_assert(w); - if (w == carry_in || w == carry_out) { - jt = ports.erase(jt); - continue; - } - if (w->port_id > carry_in->port_id) - --w->port_id; - if (w->port_id > carry_out->port_id) - --w->port_id; - log_assert(w->port_input || w->port_output); - log_assert(ports[w->port_id-1] == w->name); - ++jt; - } - ports.push_back(carry_in->name); - carry_in->port_id = ports.size(); - ports.push_back(carry_out->name); - carry_out->port_id = ports.size(); - } - } - // Fully pad all unused input connections of this box cell with S0 // Fully pad all undriven output connections of this box cell with anonymous wires // NB: Assume box_module->ports are sorted alphabetically diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index c1d4fff2d..84cb2c04f 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -76,12 +76,11 @@ inline std::string remap_name(RTLIL::IdString abc_name) return stringf("$abc$%d$%s", map_autoidx, abc_name.c_str()+1); } -void handle_loops(RTLIL::Design *design) +void handle_loops(RTLIL::Design *design, + const dict> &scc_break_inputs) { Pass::call(design, "scc -set_attr abc_scc_id {}"); - dict> abc_scc_break; - // For every unique SCC found, (arbitrarily) find the first // cell in the component, and select (and mark) all its output // wires @@ -116,44 +115,29 @@ void handle_loops(RTLIL::Design *design) cell->attributes.erase(it); } - auto jt = abc_scc_break.find(cell->type); - if (jt == abc_scc_break.end()) { - std::vector ports; - RTLIL::Module* box_module = design->module(cell->type); - if (box_module) { - auto ports_csv = box_module->attributes.at(ID(abc_scc_break), RTLIL::Const::from_string("")).decode_string(); - for (const auto &port_name : split_tokens(ports_csv, ",")) { - auto port_id = RTLIL::escape_id(port_name); - auto kt = cell->connections_.find(port_id); - if (kt == cell->connections_.end()) - log_error("abc_scc_break attribute value '%s' does not exist as port on module '%s'\n", port_name.c_str(), log_id(box_module)); - ports.push_back(port_id); + auto jt = scc_break_inputs.find(cell->type); + if (jt != scc_break_inputs.end()) + for (auto port_name : jt->second) { + RTLIL::SigSpec sig; + auto &rhs = cell->connections_.at(port_name); + for (auto b : rhs) { + Wire *w = b.wire; + if (!w) continue; + w->port_output = true; + w->set_bool_attribute(ID(abc_scc_break)); + w = module->wire(stringf("%s.abci", w->name.c_str())); + if (!w) { + w = module->addWire(stringf("%s.abci", b.wire->name.c_str()), GetSize(b.wire)); + w->port_input = true; + } + else { + log_assert(b.offset < GetSize(w)); + log_assert(w->port_input); + } + sig.append(RTLIL::SigBit(w, b.offset)); } + rhs = sig; } - jt = abc_scc_break.insert(std::make_pair(cell->type, std::move(ports))).first; - } - - for (auto port_name : jt->second) { - RTLIL::SigSpec sig; - auto &rhs = cell->connections_.at(port_name); - for (auto b : rhs) { - Wire *w = b.wire; - if (!w) continue; - w->port_output = true; - w->set_bool_attribute(ID(abc_scc_break)); - w = module->wire(stringf("%s.abci", w->name.c_str())); - if (!w) { - w = module->addWire(stringf("%s.abci", b.wire->name.c_str()), GetSize(b.wire)); - w->port_input = true; - } - else { - log_assert(b.offset < GetSize(w)); - log_assert(w->port_input); - } - sig.append(RTLIL::SigBit(w, b.offset)); - } - rhs = sig; - } } module->fixup_ports(); @@ -288,7 +272,9 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri bool cleanup, vector lut_costs, bool dff_mode, std::string clk_str, bool /*keepff*/, std::string delay_target, std::string /*lutin_shared*/, bool fast_mode, bool show_tempdir, std::string box_file, std::string lut_file, - std::string wire_delay, const dict &box_lookup) + std::string wire_delay, const dict &box_lookup, + const dict> &scc_break_inputs +) { module = current_module; map_autoidx = autoidx++; @@ -427,7 +413,7 @@ void abc9_module(RTLIL::Design *design, RTLIL::Module *current_module, std::stri RTLIL::Selection& sel = design->selection_stack.back(); sel.select(module); - handle_loops(design); + handle_loops(design, scc_break_inputs); Pass::call(design, "aigmap"); @@ -1081,6 +1067,7 @@ struct Abc9Pass : public Pass { extra_args(args, argidx, design); dict box_lookup; + dict> scc_break_inputs; for (auto m : design->modules()) { auto it = m->attributes.find(ID(abc_box_id)); if (it == m->attributes.end()) @@ -1093,6 +1080,56 @@ struct Abc9Pass : public Pass { log_error("Module '%s' has the same abc_box_id = %d value as '%s'.\n", log_id(m), id, log_id(r.first->second)); log_assert(r.second); + + RTLIL::Wire *carry_in = nullptr, *carry_out = nullptr; + for (auto p : m->ports) { + auto w = m->wire(p); + log_assert(w); + if (w->port_input) { + if (w->attributes.count(ID(abc_scc_break))) + scc_break_inputs[m->name].insert(p); + if (w->attributes.count(ID(abc_carry))) { + if (carry_in) + log_error("Module '%s' contains more than one 'abc_carry' input port.\n", log_id(m)); + carry_in = w; + } + } + if (w->port_output) { + if (w->attributes.count(ID(abc_carry))) { + if (carry_out) + log_error("Module '%s' contains more than one 'abc_carry' input port.\n", log_id(m)); + carry_out = w; + } + } + } + if (carry_in || carry_out) { + if (carry_in && !carry_out) + log_error("Module '%s' contains an 'abc_carry' input port but no output port.\n", log_id(m)); + if (!carry_in && carry_out) + log_error("Module '%s' contains an 'abc_carry' output port but no input port.\n", log_id(m)); + // Make carry_in the last PI, and carry_out the last PO + // since ABC requires it this way + auto &ports = m->ports; + for (auto it = ports.begin(); it != ports.end(); ) { + RTLIL::Wire* w = m->wire(*it); + log_assert(w); + if (w == carry_in || w == carry_out) { + it = ports.erase(it); + continue; + } + if (w->port_id > carry_in->port_id) + --w->port_id; + if (w->port_id > carry_out->port_id) + --w->port_id; + log_assert(w->port_input || w->port_output); + log_assert(ports[w->port_id-1] == w->name); + ++it; + } + ports.push_back(carry_in->name); + carry_in->port_id = ports.size(); + ports.push_back(carry_out->name); + carry_out->port_id = ports.size(); + } } for (auto mod : design->selected_modules()) @@ -1110,7 +1147,7 @@ struct Abc9Pass : public Pass { if (!dff_mode || !clk_str.empty()) { abc9_module(design, mod, script_file, exe_file, cleanup, lut_costs, dff_mode, clk_str, keepff, delay_target, lutin_shared, fast_mode, show_tempdir, - box_file, lut_file, wire_delay, box_lookup); + box_file, lut_file, wire_delay, box_lookup, scc_break_inputs); continue; } @@ -1256,7 +1293,7 @@ struct Abc9Pass : public Pass { en_sig = assign_map(std::get<3>(it.first)); abc9_module(design, mod, script_file, exe_file, cleanup, lut_costs, !clk_sig.empty(), "$", keepff, delay_target, lutin_shared, fast_mode, show_tempdir, - box_file, lut_file, wire_delay, box_lookup); + box_file, lut_file, wire_delay, box_lookup, scc_break_inputs); assign_map.set(mod); } } diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v index 3d343b315..2fcb0369e 100644 --- a/techlibs/ecp5/cells_sim.v +++ b/techlibs/ecp5/cells_sim.v @@ -15,10 +15,13 @@ module L6MUX21 (input D0, D1, SD, output Z); endmodule // --------------------------------------- -(* abc_box_id=1, abc_carry="CIN,COUT", lib_whitebox *) -module CCU2C(input CIN, A0, B0, C0, D0, A1, B1, C1, D1, - output S0, S1, COUT); - +(* abc_box_id=1, lib_whitebox *) +module CCU2C( + (* abc_carry *) input CIN, + input A0, B0, C0, D0, A1, B1, C1, D1, + output S0, S1, + (* abc_carry *) output COUT +); parameter [15:0] INIT0 = 16'h0000; parameter [15:0] INIT1 = 16'h0000; parameter INJECT1_0 = "YES"; @@ -104,12 +107,13 @@ module PFUMX (input ALUT, BLUT, C0, output Z); endmodule // --------------------------------------- -//(* abc_box_id=2, abc_scc_break="DI,WAD,WRE" *) +//(* abc_box_id=2 *) module TRELLIS_DPR16X4 ( - input [3:0] DI, - input [3:0] WAD, - input WRE, WCK, - input [3:0] RAD, + (* abc_scc_break *) input [3:0] DI, + (* abc_scc_break *) input [3:0] WAD, + (* abc_scc_break *) input WRE, + input WCK, + input [3:0] RAD, output [3:0] DO ); parameter WCKMUX = "WCK"; diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v index 2205be27d..ab04808f4 100644 --- a/techlibs/ice40/cells_sim.v +++ b/techlibs/ice40/cells_sim.v @@ -141,8 +141,14 @@ module SB_CARRY (output CO, input I0, I1, CI); assign CO = (I0 && I1) || ((I0 || I1) && CI); endmodule -(* abc_box_id = 1, abc_carry="CI,CO", lib_whitebox *) -module \$__ICE40_FULL_ADDER (output CO, O, input A, B, CI); +(* abc_box_id = 1, lib_whitebox *) +module \$__ICE40_FULL_ADDER ( + (* abc_carry *) output CO, + output O, + input A, + input B, + (* abc_carry *) input CI +); SB_CARRY carry ( .I0(A), .I1(B), diff --git a/techlibs/xilinx/cells_sim.v b/techlibs/xilinx/cells_sim.v index 05e46b4e7..bec9ea1a0 100644 --- a/techlibs/xilinx/cells_sim.v +++ b/techlibs/xilinx/cells_sim.v @@ -181,8 +181,14 @@ module XORCY(output O, input CI, LI); assign O = CI ^ LI; endmodule -(* abc_box_id = 4, abc_carry="CI,CO", lib_whitebox *) -module CARRY4(output [3:0] CO, O, input CI, CYINIT, input [3:0] DI, S); +(* abc_box_id = 4, lib_whitebox *) +module CARRY4( + (* abc_carry *) output [3:0] CO, + output [3:0] O, + (* abc_carry *) input CI, + input CYINIT, + input [3:0] DI, S +); assign O = S ^ {CO[2:0], CI | CYINIT}; assign CO[0] = S[0] ? CI | CYINIT : DI[0]; assign CO[1] = S[1] ? CO[0] : DI[1]; @@ -289,10 +295,12 @@ module FDPE_1 (output reg Q, input C, CE, D, PRE); always @(negedge C, posedge PRE) if (PRE) Q <= 1'b1; else if (CE) Q <= D; endmodule -(* abc_box_id = 5, abc_scc_break="D,WE" *) +(* abc_box_id = 5 *) module RAM32X1D ( output DPO, SPO, - input D, WCLK, WE, + (* abc_scc_break *) input D, + input WCLK, + (* abc_scc_break *) input WE, input A0, A1, A2, A3, A4, input DPRA0, DPRA1, DPRA2, DPRA3, DPRA4 ); @@ -307,10 +315,12 @@ module RAM32X1D ( always @(posedge clk) if (WE) mem[a] <= D; endmodule -(* abc_box_id = 6, abc_scc_break="D,WE" *) +(* abc_box_id = 6 *) module RAM64X1D ( output DPO, SPO, - input D, WCLK, WE, + (* abc_scc_break *) input D, + input WCLK, + (* abc_scc_break *) input WE, input A0, A1, A2, A3, A4, A5, input DPRA0, DPRA1, DPRA2, DPRA3, DPRA4, DPRA5 ); @@ -325,10 +335,12 @@ module RAM64X1D ( always @(posedge clk) if (WE) mem[a] <= D; endmodule -(* abc_box_id = 7, abc_scc_break="D,WE" *) +(* abc_box_id = 7 *) module RAM128X1D ( output DPO, SPO, - input D, WCLK, WE, + (* abc_scc_break *) input D, + input WCLK, + (* abc_scc_break *) input WE, input [6:0] A, DPRA ); parameter INIT = 128'h0;