Merge branch 'YosysHQ:master' into issue/2616

Makefile

@@ -141,7 +141,7 @@ LDLIBS += -lrt
 endif
 endif
 
-YOSYS_VER := 0.29+34
+YOSYS_VER := 0.29+40
 
 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo

kernel/hashlib.h

@@ -84,6 +84,12 @@ template<> struct hash_ops<int64_t> : hash_int_ops
 		return mkhash((unsigned int)(a), (unsigned int)(a >> 32));
 	}
 };
+template<> struct hash_ops<uint32_t> : hash_int_ops
+{
+	static inline unsigned int hash(uint32_t a) {
+		return a;
+	}
+};
 
 template<> struct hash_ops<std::string> {
 	static inline bool cmp(const std::string &a, const std::string &b) {

passes/sat/Makefile.inc

@@ -16,6 +16,7 @@ OBJS += passes/sat/fmcombine.o
 OBJS += passes/sat/mutate.o
 OBJS += passes/sat/cutpoint.o
 OBJS += passes/sat/fminit.o
+OBJS += passes/sat/recover_names.o
 ifeq ($(DISABLE_SPAWN),0)
 OBJS += passes/sat/qbfsat.o
 endif

passes/sat/recover_names.cc

@@ -0,0 +1,730 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2021 gatecat <gatecat@ds0.me>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+#include "kernel/consteval.h"
+#include "kernel/celltypes.h"
+#include "kernel/utils.h"
+#include "kernel/satgen.h"
+
+#include <algorithm>
+#include <queue>
+
+USING_YOSYS_NAMESPACE
+
+template<> struct hashlib::hash_ops<uint64_t> : hashlib::hash_int_ops
+{
+	static inline unsigned int hash(uint64_t a) {
+		return mkhash((unsigned int)(a), (unsigned int)(a >> 32));
+	}
+};
+
+PRIVATE_NAMESPACE_BEGIN
+
+// xorshift128 params
+#define INIT_X 123456789
+#define INIT_Y 362436069
+#define INIT_Z 521288629
+#define INIT_W  88675123
+
+
+// Similar to a SigBit; but module-independent
+struct IdBit {
+    IdBit() : name(), bit(0) {};
+    IdBit(IdString name, int bit = 0) : name(name), bit(bit) {};
+
+    bool operator==(const IdBit &other) const { return name == other.name && bit == other.bit; };
+    bool operator!=(const IdBit &other) const { return name != other.name || bit != other.bit; };
+    unsigned hash() const
+    {
+        return mkhash_add(name.hash(), bit);
+    }
+
+    IdString name;
+    int bit;
+};
+
+// As above; but can be inverted
+struct InvBit {
+    InvBit() : bit(), inverted(false) {};
+    explicit InvBit(IdBit bit, bool inverted = false) : bit(bit), inverted(inverted) {};
+
+    bool operator==(const InvBit &other) const { return bit == other.bit && inverted == other.inverted; };
+    bool operator!=(const InvBit &other) const { return bit != other.bit || inverted != other.inverted; };
+    unsigned hash() const
+    {
+        return mkhash(bit.hash(), inverted);
+    }
+
+    IdBit bit;
+    bool inverted;
+};
+
+typedef uint64_t equiv_cls_t;
+static const int sim_length = sizeof(equiv_cls_t) * 8;
+
+struct RecoverModuleWorker {
+    Design *design = nullptr;
+    Module *mod, *flat = nullptr;
+    RecoverModuleWorker(Module *mod) : design(mod->design), mod(mod) {};
+
+    ConstEval *ce = nullptr;
+    SigMap *sigmap = nullptr;
+
+    dict<IdBit, SigBit> flat2orig;
+    dict<IdBit, IdBit> bit2primary;
+    dict<IdBit, Cell*> bit2driver;
+
+    void prepare()
+    {
+        // Create a derivative of the module with whiteboxes flattened so we can
+        // run eval and sat on it
+        flat = design->addModule(NEW_ID);
+        mod->cloneInto(flat);
+        Pass::call_on_module(design, flat, "flatten -wb");
+        ce = new ConstEval(flat);
+        sigmap = new SigMap(flat);
+        // Create a mapping from primary name-bit in the box-flattened module to original sigbit
+        SigMap orig_sigmap(mod);
+        for (auto wire : mod->wires()) {
+            Wire *flat_wire = flat->wire(wire->name);
+            if (!flat_wire)
+                continue;
+            for (int i = 0; i < wire->width; i++) {
+                SigBit orig_sigbit = orig_sigmap(SigBit(wire, i));
+                SigBit flat_sigbit = (*sigmap)(SigBit(flat_wire, i));
+                if (!orig_sigbit.wire || !flat_sigbit.wire)
+                    continue;
+                flat2orig[IdBit(flat_sigbit.wire->name, flat_sigbit.offset)] = orig_sigbit;
+            }
+        }
+        find_driven_bits();
+    }
+
+    void find_driven_bits()
+    {
+        // Add primary inputs
+        for (auto wire : flat->wires()) {
+            if (!wire->port_input)
+                continue;
+            for (int i = 0; i < wire->width; i++) {
+                SigBit bit(wire, i);
+                bit = (*sigmap)(bit);
+                if (bit.wire)
+                    bit2driver[IdBit(bit.wire->name, bit.offset)] = nullptr;
+            }
+        }
+        // Add cell outputs
+        for (auto cell : flat->cells()) {
+            for (auto conn : cell->connections()) {
+                if (!cell->output(conn.first))
+                    continue;
+                for (auto bit : conn.second) {
+                    auto resolved = (*sigmap)(bit);
+                    if (resolved.wire)
+                        bit2driver[IdBit(resolved.wire->name, resolved.offset)] = cell;
+                }
+            }
+        }
+        // Setup bit2primary
+        for (auto wire : flat->wires()) {
+            for (int i = 0; i < wire->width; i++) {
+                SigBit bit(wire, i);
+                bit = (*sigmap)(bit);
+                if (bit.wire)
+                    bit2primary[IdBit(wire->name, i)] = IdBit(bit.wire->name, bit.offset);
+            }
+        }
+    }
+
+    // Mapping from bit to (candidate) equivalence classes
+    dict<IdBit, equiv_cls_t> bit2cls;
+    void sim_cycle(int t, const dict<IdBit, RTLIL::State> &anchors)
+    {
+        ce->clear();
+        for (auto anchor : anchors) {
+            SigBit bit = (*sigmap)(SigBit(flat->wire(anchor.first.name), anchor.first.bit));
+            // Ignore in the rare case that it's already determined
+            SigSpec res(bit);
+            if (ce->eval(res))
+                continue;
+            ce->set(bit, anchor.second);
+        }
+        // Only evaluate IdBits that exist in the non-flat design; as they are all we care about
+        for (auto idbit : flat2orig) {
+            if (anchors.count(idbit.first))
+                continue;
+            SigBit bit = (*sigmap)(SigBit(flat->wire(idbit.first.name), idbit.first.bit));
+            SigSpec res(bit);
+            if (!ce->eval(res))
+                continue;
+            if (res != State::S0 && res != State::S1)
+                continue;
+            // Update equivalence classes
+            if (res == State::S1)
+                bit2cls[idbit.first] = bit2cls[idbit.first] | (equiv_cls_t(1) << t);
+        }
+    }
+
+    // Update the equivalence class groupings
+    void group_classes(dict<equiv_cls_t, std::pair<pool<IdBit>, pool<InvBit>>> &cls2bits, bool is_gate)
+    {
+        equiv_cls_t all_ones = 0;
+        for (int i = 0; i < sim_length; i++) all_ones |= (equiv_cls_t(1) << i);
+        for (auto pair : bit2cls) {
+            if (pair.second == 0 || pair.second == all_ones)
+                continue; // skip stuck-ats
+            if (is_gate) {
+                // True doesn't exist in gold; but inverted does
+                if (!cls2bits.count(pair.second) && cls2bits.count(pair.second ^ all_ones))
+                    cls2bits[pair.second ^ all_ones].second.emplace(pair.first, true);
+                else
+                    cls2bits[pair.second].second.emplace(pair.first, false);
+            } else {
+                cls2bits[pair.second].first.insert(pair.first);
+            }
+        }
+    }
+
+    // Compute depths of IdBits
+    dict<IdBit, int> bit2depth;
+    void compute_depths(const dict<IdBit, IdBit> &anchor_bits)
+    {
+        dict<SigBit, pool<IdString>> bit_drivers, bit_users;
+        TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
+
+        for (auto cell : flat->cells())
+        for (auto conn : cell->connections())
+        {
+            for (auto bit : (*sigmap)(conn.second)) {
+                if (!bit.wire)
+                    continue;
+                IdBit idbit(bit.wire->name, bit.offset);
+                if (anchor_bits.count(idbit))
+                    continue;
+                if (cell->input(conn.first))
+                    bit_users[bit].insert(cell->name);
+
+                if (cell->output(conn.first))
+                    bit_drivers[bit].insert(cell->name);
+            }
+
+            toposort.node(cell->name);
+        }
+
+        for (auto &it : bit_users)
+            if (bit_drivers.count(it.first))
+                for (auto driver_cell : bit_drivers.at(it.first))
+                for (auto user_cell : it.second)
+                    toposort.edge(driver_cell, user_cell);
+
+        toposort.sort();
+        for (auto cell_name : toposort.sorted) {
+            Cell *cell = flat->cell(cell_name);
+            int cell_depth = 0;
+            for (auto conn : cell->connections()) {
+                if (!cell->input(conn.first))
+                    continue;
+                for (auto bit : (*sigmap)(conn.second)) {
+                    if (!bit.wire)
+                        continue;
+                    IdBit idbit(bit.wire->name, bit.offset);
+                    if (!bit2depth.count(idbit))
+                        continue;
+                    cell_depth = std::max(cell_depth, bit2depth.at(idbit));
+                }
+            }
+            for (auto conn : cell->connections()) {
+                if (!cell->output(conn.first))
+                    continue;
+                for (auto bit : (*sigmap)(conn.second)) {
+                    if (!bit.wire)
+                        continue;
+                    IdBit idbit(bit.wire->name, bit.offset);
+                    bit2depth[idbit] = std::max(bit2depth[idbit], cell_depth + 1);
+                }
+            }
+        }
+    }
+
+    // SAT thresholds
+    const int max_sat_cells = 50;
+
+    SigBit id2bit(IdBit bit) { return SigBit(flat->wire(bit.name), bit.bit); }
+
+    // Set up the SAT problem for an IdBit
+    // the value side of 'anchors' will be populated with the SAT variable for anchor bits
+    int setup_sat(SatGen *sat, const std::string &prefix, IdBit bit, const dict<IdBit, IdBit> &anchor_bits, dict<IdBit, int> &anchor2var)
+    {
+        sat->setContext(sigmap, prefix);
+        pool<IdString> imported_cells;
+        int result = sat->importSigBit(id2bit(bit));
+        // Recursively import driving cells
+        std::queue<IdBit> to_import;
+        to_import.push(bit);
+        while (!to_import.empty()) {
+            // Too many cells imported
+            if (GetSize(imported_cells) > max_sat_cells)
+                return -1;
+            IdBit cursor = to_import.front();
+            to_import.pop();
+            if (anchor_bits.count(cursor)) {
+                if (!anchor2var.count(cursor)) {
+                    anchor2var[cursor] = sat->importSigBit(id2bit(cursor));
+                }
+                continue;
+            }
+            // Import driver if it exists
+            if (!bit2driver.count(cursor))
+                continue;
+            Cell *driver = bit2driver.at(cursor);
+            if (!driver || imported_cells.count(driver->name))
+                continue;
+            if (!sat->importCell(driver))
+                return -1; // cell can't be imported
+            imported_cells.insert(driver->name);
+            // Add cell inputs to queue
+            for (auto conn : driver->connections()) {
+                if (!driver->input(conn.first))
+                    continue;
+                for (SigBit in_bit : (*sigmap)(conn.second)) {
+                    if (!in_bit.wire)
+                        continue;
+                    IdBit in_idbit(in_bit.wire->name, in_bit.offset);
+                    to_import.push(in_idbit);
+                }
+            }
+        }
+        return result;
+    }
+
+    void find_buffers(const pool<IdString> &buffer_types, dict<SigBit, pool<SigBit>> &root2buffered)
+    {
+        SigMap orig_sigmap(mod);
+        dict<SigBit, SigBit> buffer2root;
+        for (auto cell : mod->cells()) {
+            if (!buffer_types.count(cell->type))
+                continue;
+            SigBit in, out;
+            for (auto conn : cell->connections()) {
+                if (cell->input(conn.first)) {
+                    in = orig_sigmap(conn.second[0]);
+                }
+                if (cell->output(conn.first)) {
+                    out = orig_sigmap(conn.second[0]);
+                }
+            }
+            if (!in.wire || !out.wire)
+                continue;
+            SigBit root = in;
+            if (buffer2root.count(root))
+                root = buffer2root[root];
+            if (root2buffered.count(out)) {
+                for (auto out_sig : root2buffered.at(out))
+                    root2buffered[root].insert(out_sig);
+                root2buffered.erase(out);
+            }
+            root2buffered[root].insert(out);
+            buffer2root[out] = root;
+        }
+    }
+
+    void do_rename(Module *gold, const dict<IdBit, InvBit> &gate2gold, const pool<IdString> &buffer_types)
+    {
+        dict<SigBit, std::vector<std::tuple<Cell*, IdString, int>>> bit2port;
+        pool<SigBit> unused_bits;
+        SigMap orig_sigmap(mod);
+        for (auto wire : mod->wires()) {
+            if (wire->port_input || wire->port_output)
+                continue;
+            for (int i = 0; i < wire->width; i++)
+                unused_bits.insert(orig_sigmap(SigBit(wire, i)));
+        }
+        for (auto cell : mod->cells()) {
+            for (auto conn : cell->connections()) {
+                for (int i = 0; i < GetSize(conn.second); i++) {
+                    SigBit bit = orig_sigmap(conn.second[i]);
+                    if (!bit.wire)
+                        continue;
+                    bit2port[bit].emplace_back(cell, conn.first, i);
+                    unused_bits.erase(bit);
+                }
+            }
+        }
+        dict<SigBit, pool<SigBit>> root2buffered;
+        find_buffers(buffer_types, root2buffered);
+
+        // An extension of gate2gold that deals with buffers too
+        // gate sigbit --> (new name, invert, gold wire)
+        dict<SigBit, std::pair<InvBit, Wire*>> rename_map;
+        for (auto pair : gate2gold) {
+            SigBit gate_bit = flat2orig.at(pair.first);
+            Wire *gold_wire = gold->wire(pair.second.bit.name);
+            rename_map[gate_bit] = std::make_pair(pair.second, gold_wire);
+            if (root2buffered.count(gate_bit)) {
+                int buf_idx = 0;
+                for (auto buf_bit : root2buffered.at(gate_bit)) {
+                    std::string buf_name_str = stringf("%s_buf_%d", pair.second.bit.name.c_str(), ++buf_idx);
+                    if (buf_name_str[0] == '\\')
+                        buf_name_str[0] = '$';
+                    rename_map[buf_bit] = std::make_pair(
+                        InvBit(IdBit(IdString(buf_name_str), pair.second.bit.bit), pair.second.inverted), gold_wire);
+                }
+            }
+        }
+
+        for (auto rule : rename_map) {
+            // Pick a uniq new name
+            IdBit new_name = rule.second.first.bit;
+            int dup_idx = 0;
+            bool must_invert_name = rule.second.first.inverted;
+            while (must_invert_name ||
+                    (mod->wire(new_name.name) && !unused_bits.count(SigBit(mod->wire(new_name.name), new_name.bit)))) {
+                std::string new_name_str = stringf("%s_%s_%d", rule.second.first.bit.name.c_str(),
+                    rule.second.first.inverted ? "inv" : "dup", ++dup_idx);
+                if (new_name_str[0] == '\\')
+                    new_name_str[0] = '$';
+                new_name.name = IdString(new_name_str);
+                must_invert_name = false;
+            }
+            // Create the wire if needed
+            Wire *new_wire = mod->wire(new_name.name);
+            if (!new_wire) {
+                Wire *gold_wire = rule.second.second;
+                new_wire = mod->addWire(new_name.name, gold_wire->width);
+                new_wire->start_offset = gold_wire->start_offset;
+                new_wire->upto = gold_wire->upto;
+                for (const auto &attr : gold_wire->attributes)
+                    new_wire->attributes[attr.first] = attr.second;
+                for (int i = 0; i < new_wire->width; i++)
+                    unused_bits.insert(SigBit(new_wire, i));
+            }
+            // Ensure it's wide enough
+            if (new_wire->width <= new_name.bit)
+                new_wire->width = new_name.bit + 1;
+            SigBit old_bit = rule.first;
+            SigBit new_bit(new_wire, new_name.bit);
+            unused_bits.erase(new_bit);
+            // Replace all users
+            if (bit2port.count(old_bit))
+                for (auto port_ref : bit2port.at(old_bit)) {
+                    Cell *cell = std::get<0>(port_ref);
+                    IdString port_name = std::get<1>(port_ref);
+                    int port_bit = std::get<2>(port_ref);
+                    SigSpec port_sig = cell->getPort(port_name);
+                    port_sig.replace(port_bit, new_bit);
+                    cell->unsetPort(port_name);
+                    cell->setPort(port_name, port_sig);
+                }
+        }
+    }
+
+    ~RecoverModuleWorker()
+    {
+        delete ce;
+        delete sigmap;
+        if (flat)
+            design->remove(flat);
+    }
+};
+
+struct RecoverNamesWorker {
+    Design *design, *gold_design = nullptr;
+    CellTypes ct_all;
+    RecoverNamesWorker(Design *design) : design(design) {}
+
+    pool<IdString> comb_whiteboxes, buffer_types;
+
+    // class -> (gold, (gate, inverted))
+    dict<equiv_cls_t, std::pair<pool<IdBit>, dict<IdBit, bool>>> cls2bits; 
+
+    void analyse_boxes()
+    {
+        for (auto mod : design->modules()) {
+            if (!mod->get_bool_attribute(ID::whitebox))
+                continue;
+            bool is_comb = true;
+            for (auto cell : mod->cells()) {
+                if (ct_all.cell_evaluable(cell->type)) {
+                    is_comb = false;
+                    break;
+                }
+            }
+            if (!is_comb)
+                continue;
+            comb_whiteboxes.insert(mod->name);
+            // Buffers have one input and one output; exactly
+            SigBit in{}, out{};
+            ConstEval eval(mod);
+            for (auto wire : mod->wires()) {
+                if (wire->port_input) {
+                    if (wire->width != 1 || in.wire)
+                        goto not_buffer;
+                    in = SigBit(wire, 0);
+                }
+                if (wire->port_output) {
+                    if (wire->width != 1 || out.wire)
+                        goto not_buffer;
+                    out = SigBit(wire, 0);
+                }
+            }
+            if (!in.wire || !out.wire)
+                goto not_buffer;
+            // Buffer input mirrors output
+            for (auto bit : {State::S0, State::S1}) {
+                eval.clear();
+                eval.set(in, bit);
+                SigSpec result(out);
+                if (!eval.eval(result))
+                    goto not_buffer;
+                if (result != bit)
+                    goto not_buffer;
+            }
+            buffer_types.insert(mod->name);
+            if (false) {
+                not_buffer:
+                    continue;
+            }
+        }
+        log_debug("Found %d combinational cells and %d buffer whiteboxes.\n", GetSize(comb_whiteboxes), GetSize(buffer_types));
+    }
+
+    uint32_t x, y, z, w, rng_val;
+    int rng_bit;
+    void rng_init()
+    {
+        x = INIT_X;
+        y = INIT_Y;
+        z = INIT_Z;
+        w = INIT_W;
+        rng_bit = 32;
+    }
+    uint32_t xorshift128()
+    {
+        uint32_t t = x ^ (x << 11);
+        x = y; y = z; z = w;
+        w ^= (w >> 19) ^ t ^ (t >> 8);
+        return w;
+    }
+    RTLIL::State next_randbit()
+    {
+        if (rng_bit >= 32) {
+            rng_bit = 0;
+            rng_val = xorshift128();
+        }
+        return ((rng_val >> (rng_bit++)) & 0x1) ? RTLIL::State::S1 : RTLIL::State::S0;
+    }
+
+    int popcount(equiv_cls_t cls) {
+    	int result = 0;
+    	for (unsigned i = 0; i < 8*sizeof(equiv_cls_t); i++)
+    		if ((cls >> i) & 0x1)
+    			++result;
+    	return result;
+    }
+
+    bool prove_equiv(RecoverModuleWorker &gold_worker, RecoverModuleWorker &gate_worker,
+            const dict<IdBit, IdBit> &gold_anchors, const dict<IdBit, IdBit> &gate_anchors,
+            IdBit gold_bit, IdBit gate_bit, bool invert) {
+        ezSatPtr ez;
+        SatGen satgen(ez.get(), nullptr);
+        dict<IdBit, int> anchor2var_gold, anchor2var_gate;
+        int gold_var = gold_worker.setup_sat(&satgen, "gold", gold_bit, gold_anchors, anchor2var_gold);
+        if (gold_var == -1)
+            return false;
+        int gate_var = gate_worker.setup_sat(&satgen, "gate", gate_bit, gate_anchors, anchor2var_gate);
+        if (gate_var == -1)
+            return false;
+        // Assume anchors are equal
+        for (auto anchor : anchor2var_gate) {
+            IdBit gold_anchor = gate_anchors.at(anchor.first);
+            if (!anchor2var_gold.count(gold_anchor))
+                continue;
+            ez->assume(ez->IFF(anchor.second, anchor2var_gold.at(gold_anchor)));
+        }
+        // Prove equivalence
+        return !ez->solve(ez->NOT(ez->IFF(gold_var, invert ? ez->NOT(gate_var) : gate_var)));
+    }
+
+    void analyse_mod(Module *gate_mod)
+    {
+        Module *gold_mod = gold_design->module(gate_mod->name);
+        if (!gold_mod)
+            return;
+
+        RecoverModuleWorker gold_worker(gold_mod);
+        RecoverModuleWorker gate_worker(gate_mod);
+
+        gold_worker.prepare();
+        gate_worker.prepare();
+
+        // Find anchors (same-name wire-bits driven in both gold and gate)
+        dict<IdBit, IdBit> gold_anchors, gate_anchors;
+
+        for (auto gold_bit : gold_worker.bit2driver) {
+            if (gate_worker.bit2primary.count(gold_bit.first)) {
+                IdBit gate_bit = gate_worker.bit2primary.at(gold_bit.first);
+                if (!gate_worker.bit2driver.count(gate_bit))
+                    continue;
+                gold_anchors[gold_bit.first] = gate_bit;
+                gate_anchors[gate_bit] = gold_bit.first;
+            }
+        }
+        // Run a random-value combinational simulation to find candidate equivalence classes
+        dict<IdBit, RTLIL::State> gold_anchor_vals, gate_anchor_vals;
+        rng_init();
+        for (int t = 0; t < sim_length; t++) {
+            for (auto anchor : gold_anchors) {
+                gold_anchor_vals[anchor.first] = next_randbit();
+                gate_anchor_vals[anchor.second] = gold_anchor_vals[anchor.first];
+            }
+            gold_worker.sim_cycle(t, gold_anchor_vals);
+            gate_worker.sim_cycle(t, gate_anchor_vals);
+        }
+        log_debug("%d candidate equiv classes in gold; %d in gate\n", GetSize(gold_worker.bit2cls), GetSize(gate_worker.bit2cls));
+        // Group bits by equivalence classes together
+        dict<equiv_cls_t, std::pair<pool<IdBit>, pool<InvBit>>> cls2bits;
+        gold_worker.group_classes(cls2bits, false);
+        gate_worker.group_classes(cls2bits, true);
+        gate_worker.compute_depths(gate_anchors);
+        // Sort equivalence classes by shallowest first (so we have as many anchors as possible when reaching deeper bits)
+        std::vector<std::pair<equiv_cls_t, int>> cls_depth;
+        for (auto &cls : cls2bits) {
+            if (cls.second.second.empty())
+                continue;
+            int depth = 0;
+            for (auto gate_bit : cls.second.second) {
+                if (!gate_worker.bit2depth.count(gate_bit.bit))
+                    continue;
+                depth = std::max(depth, gate_worker.bit2depth.at(gate_bit.bit));
+            }
+            cls_depth.emplace_back(cls.first, depth);
+        }
+        std::stable_sort(cls_depth.begin(), cls_depth.end(),
+            [](const std::pair<equiv_cls_t, int> &a, const std::pair<equiv_cls_t, int> &b) {
+                return a.second < b.second;
+            });
+        // The magic result we've worked hard for....
+        dict<IdBit, InvBit> gate2gold;
+        // Solve starting from shallowest
+        for (auto cls : cls_depth) {
+        	int pop = popcount(cls.first);
+        	// Equivalence classes with only one set bit are invariably a waste of SAT time
+        	if (pop == 1 || pop == (8*sizeof(equiv_cls_t) - 1))
+        		continue;
+
+        	log_debug("equivalence class: %016lx\n", cls.first);
+            const pool<IdBit> &gold_bits = cls2bits.at(cls.first).first;
+            const pool<InvBit> &gate_bits = cls2bits.at(cls.first).second;
+            if (gold_bits.empty() || gate_bits.empty())
+                continue;
+            pool<IdBit> solved_gate;
+            if (GetSize(gold_bits) > 10)
+                continue; // large equivalence classes are not very interesting; skip
+            for (IdBit gold_bit : gold_bits) {
+                for (auto gate_bit : gate_bits) {
+                    if (solved_gate.count(gate_bit.bit))
+                        continue;
+                    log_debug("   attempting to prove %s[%d] == %s%s[%d]\n", log_id(gold_bit.name), gold_bit.bit,
+                        gate_bit.inverted ? "" : "!", log_id(gate_bit.bit.name), gate_bit.bit.bit);
+                    if (!prove_equiv(gold_worker, gate_worker, gold_anchors, gate_anchors, gold_bit, gate_bit.bit, gate_bit.inverted))
+                        continue;
+                    log_debug("       success!\n");
+                    // Success!
+                    gate2gold[gate_bit.bit] = InvBit(gold_bit, gate_bit.inverted);
+                    if (!gate_bit.inverted) {
+                        // Only add as anchor if not inverted
+                        gold_anchors[gold_bit] = gate_bit.bit;
+                        gate_anchors[gate_bit.bit] = gold_bit;
+                    }
+                    solved_gate.insert(gate_bit.bit);
+                }
+                // All solved...
+                if (GetSize(solved_gate) == GetSize(gate_bits))
+                    break;
+            }
+        }
+        log("Recovered %d net name pairs in module `%s' out.\n", GetSize(gate2gold), log_id(gate_mod));
+        gate_worker.do_rename(gold_mod, gate2gold, buffer_types);
+    }
+
+    void operator()(string command)
+    {
+        // Make a backup copy of the pre-mapping design for later
+        gold_design = new RTLIL::Design;
+
+        for (auto mod : design->modules())
+            gold_design->add(mod->clone());
+
+        run_pass(command, design);
+
+        analyse_boxes();
+
+        // keeping our own std::vector here avoids modify-while-iterating issues
+        std::vector<Module *> to_analyse;
+        for (auto mod : design->modules())
+            if (!mod->get_blackbox_attribute())
+                to_analyse.push_back(mod);
+        for (auto mod : to_analyse)
+            analyse_mod(mod);
+    }
+    ~RecoverNamesWorker() {
+        delete gold_design;
+    }
+};
+
+struct RecoverNamesPass : public Pass {
+    RecoverNamesPass() : Pass("recover_names", "Execute a lossy mapping command and recover original netnames") { }
+    void help() override
+    {
+        //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+        log("\n");
+        log("    recover_names [command]\n");
+        log("\n");
+        log("This pass executes a lossy mapping command and uses a combination of simulation\n");
+        log(" to find candidate equivalences and SAT to recover exact original net names.\n");
+        log("\n");
+    }
+    void execute(std::vector<std::string> args, RTLIL::Design *design) override
+    {
+        log_header(design, "Executing RECOVER_NAMES pass (run mapping and recover original names).\n");
+        string command;
+
+        size_t argidx = 1;
+        for (; argidx < args.size(); argidx++) {
+            if (command.empty()) {
+                if (args[argidx].compare(0, 1, "-") == 0)
+                    cmd_error(args, argidx, "Unknown option.");
+            } else {
+                command += " ";
+            }
+            command += args[argidx];
+        }
+
+        if (command.empty())
+            log_cmd_error("No mapping pass specified!\n");
+
+        RecoverNamesWorker worker(design);
+        worker(command);
+
+    }
+} RecoverNamesPass;
+
+PRIVATE_NAMESPACE_END

passes/techmap/abc9_ops.cc

@@ -233,22 +233,23 @@ void prep_hier(RTLIL::Design *design, bool dff_mode)
 
 				if (derived_type != cell->type) {
 					auto unmap_module = unmap_design->addModule(derived_type);
+					auto replace_cell = unmap_module->addCell(ID::_TECHMAP_REPLACE_, cell->type);
 					for (auto port : derived_module->ports) {
 						auto w = unmap_module->addWire(port, derived_module->wire(port));
 						// Do not propagate (* init *) values into the box,
 						//   in fact, remove it from outside too
 						if (w->port_output)
 							w->attributes.erase(ID::init);
+						// Attach (* techmap_autopurge *) to all ports to ensure that
+						//   undriven inputs/unused outputs are propagated through to
+						//   the techmapped cell
+						w->attributes[ID::techmap_autopurge] = 1;
+
+						replace_cell->setPort(port, w);
 					}
 					unmap_module->ports = derived_module->ports;
 					unmap_module->check();
 
-					auto replace_cell = unmap_module->addCell(ID::_TECHMAP_REPLACE_, cell->type);
-					for (const auto &conn : cell->connections()) {
-						auto w = unmap_module->wire(conn.first);
-						log_assert(w);
-						replace_cell->setPort(conn.first, w);
-					}
 					replace_cell->parameters = cell->parameters;
 				}
 			}

techlibs/intel_alm/common/alm_sim.v

@@ -1,5 +1,5 @@
 // The core logic primitive of the Cyclone V/10GX is the Adaptive Logic Module
-// (ALM). Each ALM is made up of an 8-input, 2-output look-up table, covered 
+// (ALM). Each ALM is made up of an 8-input, 2-output look-up table, covered
 // in this file, connected to combinational outputs, a carry chain, and four
 // D flip-flops (which are covered as MISTRAL_FF in dff_sim.v).
 //
@@ -283,10 +283,8 @@ assign Q = ~A;
 
 endmodule
 
-// Despite the abc9_carry attributes, this doesn't seem to stop ABC9 adding illegal fanout to the carry chain that nextpnr cannot handle.
-// So we treat it as a total blackbox from ABC9's perspective for now.
-// (* abc9_box, lib_whitebox *)
-module MISTRAL_ALUT_ARITH(input A, B, C, D0, D1, /* (* abc9_carry *) */ input CI, output SO, /* (* abc9_carry *) */ output CO);
+(* abc9_box, lib_whitebox *)
+module MISTRAL_ALUT_ARITH(input A, B, C, D0, D1, (* abc9_carry *) input CI, output SO, (* abc9_carry *) output CO);
 
 parameter LUT0 = 16'h0000;
 parameter LUT1 = 16'h0000;

techlibs/intel_alm/common/bram_m10k.txt

@@ -1,5 +1,5 @@
 bram $__MISTRAL_M10K
-    init   0   # TODO: Re-enable when I figure out how BRAM init works
+    init   1
     abits 13   @D8192x1
     dbits  1   @D8192x1
     abits 12   @D4096x2
@@ -10,6 +10,8 @@ bram $__MISTRAL_M10K
     dbits 10   @D1024x10
     abits  9   @D512x20
     dbits 20   @D512x20
+    abits  8   @D256x40
+    dbits 40   @D256x40
     groups 2
     ports  1 1
     wrmode 1 0

techlibs/intel_alm/common/bram_m10k_map.v

@@ -2,6 +2,8 @@
 
 module \$__MISTRAL_M10K (CLK1, A1ADDR, A1DATA, A1EN, B1ADDR, B1DATA, B1EN);
 
+parameter INIT = 0;
+
 parameter CFG_ABITS = 10;
 parameter CFG_DBITS = 10;
 
@@ -11,6 +13,14 @@ input [CFG_DBITS-1:0] A1DATA;
 input A1EN, B1EN;
 output reg [CFG_DBITS-1:0] B1DATA;
 
-MISTRAL_M10K #(.CFG_ABITS(CFG_ABITS), .CFG_DBITS(CFG_DBITS)) _TECHMAP_REPLACE_ (.CLK1(CLK1), .A1ADDR(A1ADDR), .A1DATA(A1DATA), .A1EN(!A1EN), .B1ADDR(B1ADDR), .B1DATA(B1DATA), .B1EN(B1EN));
+// Normal M10K configs use WREN[1], which is negative-true.
+// However, 8x40-bit mode uses WREN[0], which is positive-true.
+wire a1en;
+if (CFG_DBITS == 40)
+    assign a1en = A1EN;
+else
+    assign a1en = !A1EN;
 
-endmodule
+MISTRAL_M10K #(.INIT(INIT), .CFG_ABITS(CFG_ABITS), .CFG_DBITS(CFG_DBITS)) _TECHMAP_REPLACE_ (.CLK1(CLK1), .A1ADDR(A1ADDR), .A1DATA(A1DATA), .A1EN(a1en), .B1ADDR(B1ADDR), .B1DATA(B1DATA), .B1EN(B1EN));
+
+endmodule

techlibs/intel_alm/common/mem_sim.v

@@ -3,7 +3,7 @@
 // In addition to Logic Array Blocks (LABs) that contain ten Adaptive Logic
 // Modules (ALMs, see alm_sim.v), the Cyclone V/10GX also contain
 // Memory/Logic Array Blocks (MLABs) that can act as either ten ALMs, or utilise
-// the memory the ALM uses to store the look-up table data for general usage, 
+// the memory the ALM uses to store the look-up table data for general usage,
 // producing a 32 address by 20-bit block of memory. MLABs are spread out
 // around the chip, so they can be placed near where they are needed, rather than
 // being comparatively limited in placement for a deep but narrow memory such as
@@ -43,7 +43,7 @@
 // Quartus will pack external flops into the MLAB, but this is an assumption
 // that needs testing.
 
-// The vendor sim model outputs 'x for a very short period (a few 
+// The vendor sim model outputs 'x for a very short period (a few
 // combinational delta cycles) after each write. This has been omitted from
 // the following model because it's very difficult to trigger this in practice
 // as clock cycles will be much longer than any potential blip of 'x, so the
@@ -110,6 +110,8 @@ endmodule
 
 module MISTRAL_M10K(CLK1, A1ADDR, A1DATA, A1EN, B1ADDR, B1DATA, B1EN);
 
+parameter INIT = 0;
+
 parameter CFG_ABITS = 10;
 parameter CFG_DBITS = 10;
 
@@ -119,7 +121,7 @@ input [CFG_DBITS-1:0] A1DATA;
 input A1EN, B1EN;
 output reg [CFG_DBITS-1:0] B1DATA;
 
-reg [2**CFG_ABITS * CFG_DBITS - 1 : 0] mem = 0;
+reg [2**CFG_ABITS * CFG_DBITS - 1 : 0] mem = INIT;
 
 `ifdef cyclonev
 specify

tests/arch/intel_alm/counter.ys

@@ -6,7 +6,7 @@ equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm
 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 2 t:MISTRAL_NOT
 select -assert-count 8 t:MISTRAL_ALUT_ARITH
 select -assert-count 8 t:MISTRAL_FF
 select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D
@@ -21,7 +21,7 @@ equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm
 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 2 t:MISTRAL_NOT
 select -assert-count 8 t:MISTRAL_ALUT_ARITH
 select -assert-count 8 t:MISTRAL_FF
 select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D

tests/arch/xilinx/dsp_abc9.ys

@@ -1,3 +1,5 @@
+logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
+
 read_verilog <<EOT
 module top(input [24:0] A, input [17:0] B, output [47:0] P);
 DSP48E1 #(.PREG(0)) dsp(.A(A), .B(B), .P(P));
@@ -35,3 +37,18 @@ techmap -autoproc -wb -map +/xilinx/cells_sim.v
 opt -full -fine
 select -assert-count 0 t:* t:$assert %d
 sat -verify -prove-asserts
+
+
+design -reset
+read_verilog <<EOT
+module top(input signed [29:0] A, input signed [17:0] B, output signed [47:0] P);
+wire [47:0] casc;
+DSP48E1 #(.AREG(1)) u1(.A(A), .B(B), .PCOUT(casc));
+DSP48E1 #(.AREG(1)) u2(.A(A), .B(B), .PCIN(casc), .P(P));
+endmodule
+EOT
+synth_xilinx -run :prepare
+abc9
+clean
+check
+logger -expect-no-warnings