Merge pull request #4894 from YosysHQ/emil/abstract

Add `abstract` pass for formal verification

kernel/rtlil.h

@@ -1673,6 +1673,19 @@ public:
 	RTLIL::Cell *driverCell() const    { log_assert(driverCell_); return driverCell_; };
 	RTLIL::IdString driverPort() const { log_assert(driverCell_); return driverPort_; };
 
+	int from_hdl_index(int hdl_index) {
+		int zero_index = hdl_index - start_offset;
+		int rtlil_index = upto ? width - 1 - zero_index : zero_index;
+		return rtlil_index >= 0 && rtlil_index < width ? rtlil_index : INT_MIN;
+	}
+
+	int to_hdl_index(int rtlil_index) {
+		if (rtlil_index < 0 || rtlil_index >= width)
+			return INT_MIN;
+		int zero_index = upto ? width - 1 - rtlil_index : rtlil_index;
+		return zero_index + start_offset;
+	}
+
 #ifdef WITH_PYTHON
 	static std::map<unsigned int, RTLIL::Wire*> *get_all_wires(void);
 #endif

passes/cmds/Makefile.inc

@@ -53,3 +53,4 @@ OBJS += passes/cmds/example_dt.o
 OBJS += passes/cmds/portarcs.o
 OBJS += passes/cmds/wrapcell.o
 OBJS += passes/cmds/setenv.o
+OBJS += passes/cmds/abstract.o

passes/cmds/abstract.cc

@@ -0,0 +1,491 @@
+#include "kernel/yosys.h"
+#include "kernel/celltypes.h"
+#include "kernel/ff.h"
+#include "kernel/ffinit.h"
+#include <variant>
+#include <charconv>
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EnableLogic {
+	SigBit bit;
+	bool pol;
+};
+
+enum SliceIndices {
+	RtlilSlice,
+	HdlSlice,
+};
+
+struct Slice {
+	SliceIndices indices;
+	int first;
+	int last;
+
+	Slice(SliceIndices indices, const std::string &slice) :
+		indices(indices)
+	{
+		if (slice.empty())
+			syntax_error(slice);
+		auto sep = slice.find(':');
+		const char *first_begin, *first_end, *last_begin, *last_end;
+		if (sep == std::string::npos) {
+			first_begin = last_begin = slice.c_str();
+			first_end = last_end = slice.c_str() + slice.length();
+		} else {
+			first_begin = slice.c_str();
+			first_end = first_begin + sep;
+
+			last_begin = first_end + 1;
+			last_end = slice.c_str() + slice.length();
+		}
+		first = parse_index(first_begin, first_end, slice);
+		last = parse_index(last_begin, last_end, slice);
+	}
+
+	static int parse_index(const char *begin, const char *end, const std::string &slice) {
+		int value;
+		auto result = std::from_chars(begin, end, value, 10);
+        if (result.ptr != end || result.ptr == begin)
+			syntax_error(slice);
+		return value;
+	}
+
+	static void syntax_error(const std::string &slice) {
+		log_cmd_error("Invalid slice '%s', expected '<first>:<last>' or '<single>'", slice.c_str());
+	}
+
+	std::string to_string() const {
+		const char *option = indices == RtlilSlice ? "-rtlilslice" : "-slice";
+		if (first == last)
+			return stringf("%s %d", option, first);
+		else
+			return stringf("%s %d:%d", option, first, last);
+	}
+
+	int wire_offset(RTLIL::Wire *wire, int index) const {
+		int rtl_offset = indices == RtlilSlice ? index : wire->from_hdl_index(index);
+		if (rtl_offset < 0 || rtl_offset >= wire->width) {
+			log_error("Slice %s is out of bounds for wire %s in module %s", to_string().c_str(), log_id(wire), log_id(wire->module));
+		}
+		return rtl_offset;
+	}
+
+	std::pair<int, int> wire_range(RTLIL::Wire *wire) const {
+		int rtl_first = wire_offset(wire, first);
+		int rtl_last = wire_offset(wire, last);
+		if (rtl_first > rtl_last)
+			std::swap(rtl_first, rtl_last);
+		return {rtl_first, rtl_last + 1};
+	}
+};
+
+void emit_mux_anyseq(Module* mod, const SigSpec& mux_input, const SigSpec& mux_output, EnableLogic enable) {
+	auto anyseq = mod->Anyseq(NEW_ID, mux_input.size());
+	if (enable.bit == (enable.pol ? State::S1 : State::S0)) {
+		mod->connect(mux_output, anyseq);
+	}
+	SigSpec mux_a, mux_b;
+	if (enable.pol) {
+		mux_a = mux_input;
+		mux_b = anyseq;
+	} else {
+		mux_a = anyseq;
+		mux_b = mux_input;
+	}
+	(void)mod->addMux(NEW_ID,
+		mux_a,
+		mux_b,
+		enable.bit,
+		mux_output);
+}
+
+bool abstract_state_port(FfData& ff, SigSpec& port_sig, std::set<int> offsets, EnableLogic enable) {
+	Wire* abstracted = ff.module->addWire(NEW_ID, offsets.size());
+	SigSpec mux_input;
+	int abstracted_idx = 0;
+	for (int d_idx = 0; d_idx < ff.width; d_idx++) {
+		if (offsets.count(d_idx)) {
+			mux_input.append(port_sig[d_idx]);
+			port_sig[d_idx].wire = abstracted;
+			port_sig[d_idx].offset = abstracted_idx;
+			log_assert(abstracted_idx < abstracted->width);
+			abstracted_idx++;
+		}
+	}
+	emit_mux_anyseq(ff.module, mux_input, abstracted, enable);
+	(void)ff.emit();
+	return true;
+}
+
+using SelReason=std::variant<Wire*, Cell*>;
+
+dict<SigBit, std::vector<SelReason>> gather_selected_reps(Module* mod, const std::vector<Slice> &slices, SigMap& sigmap) {
+	dict<SigBit, std::vector<SelReason>> selected_reps;
+
+	if (slices.empty()) {
+		// Collect reps for all wire bits of selected wires
+		for (auto wire : mod->selected_wires())
+			for (auto bit : sigmap(wire))
+				selected_reps.insert(bit).first->second.push_back(wire);
+
+		// Collect reps for all output wire bits of selected cells
+		for (auto cell : mod->selected_cells())
+			for (auto conn : cell->connections())
+				if (cell->output(conn.first))
+					for (auto bit : conn.second.bits())
+						selected_reps.insert(sigmap(bit)).first->second.push_back(cell);
+	} else {
+		if (mod->selected_wires().size() != 1 || !mod->selected_cells().empty())
+			log_error("Slices are only supported for single-wire selections\n");
+
+		auto wire = mod->selected_wires()[0];
+
+		for (auto slice : slices) {
+			auto [begin, end] = slice.wire_range(wire);
+			for (int i = begin; i < end; i++) {
+				selected_reps.insert(sigmap(SigBit(wire, i))).first->second.push_back(wire);
+			}
+		}
+
+	}
+	return selected_reps;
+}
+
+void explain_selections(const std::vector<SelReason>& reasons) {
+	for (std::variant<Wire*, Cell*> reason : reasons) {
+		if (Cell** cell_reason = std::get_if<Cell*>(&reason))
+			log_debug("\tcell %s\n", (*cell_reason)->name.c_str());
+		else if (Wire** wire_reason = std::get_if<Wire*>(&reason))
+			log_debug("\twire %s\n", (*wire_reason)->name.c_str());
+		else
+			log_assert(false && "insane reason variant\n");
+	}
+}
+
+unsigned int abstract_state(Module* mod, EnableLogic enable, const std::vector<Slice> &slices) {
+	CellTypes ct;
+	ct.setup_internals_ff();
+	SigMap sigmap(mod);
+	dict<SigBit, std::vector<SelReason>> selected_reps = gather_selected_reps(mod, slices, sigmap);
+
+	unsigned int changed = 0;
+	std::vector<FfData> ffs;
+	// Abstract flop inputs if they're driving a selected output rep
+	for (auto cell : mod->cells()) {
+		if (!ct.cell_types.count(cell->type))
+			continue;
+		FfData ff(nullptr, cell);
+		if (ff.has_sr)
+			log_cmd_error("SR not supported\n");
+		ffs.push_back(ff);
+	}
+	for (auto ff : ffs) {
+		// A bit inefficient
+		std::set<int> offsets_to_abstract;
+		for (int i = 0; i < GetSize(ff.sig_q); i++) {
+			SigBit bit = ff.sig_q[i];
+			if (selected_reps.count(sigmap(bit))) {
+				log_debug("Abstracting state for %s.Q[%i] in module %s due to selections:\n", log_id(ff.cell), i, log_id(mod));
+				explain_selections(selected_reps.at(sigmap(bit)));
+				offsets_to_abstract.insert(i);
+			}
+		}
+
+		if (offsets_to_abstract.empty())
+			continue;
+
+		// Normalize to simpler FF
+		ff.unmap_ce();
+		ff.unmap_srst();
+		if (ff.has_arst)
+			ff.arst_to_aload();
+
+		bool cell_changed = false;
+
+		if (ff.has_aload)
+			cell_changed = abstract_state_port(ff, ff.sig_ad, offsets_to_abstract, enable);
+		cell_changed |= abstract_state_port(ff, ff.sig_d, offsets_to_abstract, enable);
+		changed += cell_changed;
+	}
+	return changed;
+}
+
+bool abstract_value_cell_port(Module* mod, Cell* cell, std::set<int> offsets, IdString port_name, EnableLogic enable) {
+	Wire* to_abstract = mod->addWire(NEW_ID, offsets.size());
+	SigSpec mux_input;
+	SigSpec mux_output;
+	const SigSpec& old_port = cell->getPort(port_name);
+	SigSpec new_port = old_port;
+	int to_abstract_idx = 0;
+	for (int port_idx = 0; port_idx < old_port.size(); port_idx++) {
+		if (offsets.count(port_idx)) {
+			mux_output.append(old_port[port_idx]);
+			SigBit in_bit {to_abstract, to_abstract_idx};
+			new_port.replace(port_idx, in_bit);
+			mux_input.append(in_bit);
+			log_assert(to_abstract_idx < to_abstract->width);
+			to_abstract_idx++;
+		}
+	}
+	cell->setPort(port_name, new_port);
+	emit_mux_anyseq(mod, mux_input, mux_output, enable);
+	return true;
+}
+
+bool abstract_value_mod_port(Module* mod, Wire* wire, std::set<int> offsets, EnableLogic enable) {
+	Wire* to_abstract = mod->addWire(NEW_ID, wire);
+	to_abstract->port_input = true;
+	to_abstract->port_id = wire->port_id;
+	wire->port_input = false;
+	wire->port_id = 0;
+	mod->swap_names(wire, to_abstract);
+	SigSpec mux_input;
+	SigSpec mux_output;
+	SigSpec direct_lhs;
+	SigSpec direct_rhs;
+	for (int port_idx = 0; port_idx < wire->width; port_idx++) {
+		if (offsets.count(port_idx)) {
+			mux_output.append(SigBit(wire, port_idx));
+			mux_input.append(SigBit(to_abstract, port_idx));
+		} else {
+			direct_lhs.append(SigBit(wire, port_idx));
+			direct_rhs.append(SigBit(to_abstract, port_idx));
+		}
+	}
+	mod->connections_.push_back(SigSig(direct_lhs, direct_rhs));
+	emit_mux_anyseq(mod, mux_input, mux_output, enable);
+	return true;
+}
+
+unsigned int abstract_value(Module* mod, EnableLogic enable, const std::vector<Slice> &slices) {
+	SigMap sigmap(mod);
+	dict<SigBit, std::vector<SelReason>> selected_reps = gather_selected_reps(mod, slices, sigmap);
+	unsigned int changed = 0;
+	std::vector<Cell*> cells_snapshot = mod->cells();
+	for (auto cell : cells_snapshot) {
+		for (auto conn : cell->connections())
+			if (cell->output(conn.first)) {
+				std::set<int> offsets_to_abstract;
+				for (int i = 0; i < conn.second.size(); i++) {
+					if (selected_reps.count(sigmap(conn.second[i]))) {
+						log_debug("Abstracting value for %s.%s[%i] in module %s due to selections:\n",
+							log_id(cell), log_id(conn.first), i, log_id(mod));
+						explain_selections(selected_reps.at(sigmap(conn.second[i])));
+						offsets_to_abstract.insert(i);
+					}
+				}
+				if (offsets_to_abstract.empty())
+					continue;
+
+				changed += abstract_value_cell_port(mod, cell, offsets_to_abstract, conn.first, enable);
+			}
+	}
+	std::vector<Wire*> wires_snapshot = mod->wires();
+	for (auto wire : wires_snapshot)
+		if (wire->port_input) {
+			std::set<int> offsets_to_abstract;
+			for (auto bit : SigSpec(wire))
+				if (selected_reps.count(sigmap(bit))) {
+					log_debug("Abstracting value for module input port bit %s in module %s due to selections:\n",
+						log_signal(bit), log_id(mod));
+					explain_selections(selected_reps.at(sigmap(bit)));
+					offsets_to_abstract.insert(bit.offset);
+				}
+			if (offsets_to_abstract.empty())
+				continue;
+
+			changed += abstract_value_mod_port(mod, wire, offsets_to_abstract, enable);
+		}
+	return changed;
+}
+
+unsigned int abstract_init(Module* mod, const std::vector<Slice> &slices) {
+	unsigned int changed = 0;
+	FfInitVals initvals;
+	SigMap sigmap(mod);
+	dict<SigBit, std::vector<SelReason>> selected_reps = gather_selected_reps(mod, slices, sigmap);
+	initvals.set(&sigmap, mod);
+	for (auto bit : selected_reps) {
+		log_debug("Removing init bit on %s due to selections:\n", log_signal(bit.first));
+		explain_selections(bit.second);
+		initvals.remove_init(bit.first);
+		changed++;
+	}
+	return changed;
+}
+
+struct AbstractPass : public Pass {
+	AbstractPass() : Pass("abstract", "replace signals with abstract values during formal verification") { }
+	void help() override {
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    abstract [mode] [options] [selection]\n");
+		log("\n");
+		log("Perform abstraction of signals within the design. Abstraction replaces a signal\n");
+		log("with an unconstrained abstract value that can take an arbitrary concrete value\n");
+		log("during formal verification. The mode and options control when a signal should\n");
+		log("be abstracted and how it should affect FFs present in the design.\n");
+		log("\n");
+		log("Modes:");
+		log("\n");
+		log("    -state\n");
+		log("        The selected FFs will be modified to load a new abstract value on every\n");
+		log("        active clock edge, async reset or async load. This is independent of any\n");
+		log("        clock enable that may be present on the FF cell. Conditional abstraction\n");
+		log("        is supported with the -enable/-enabeln options. If present, the condition\n");
+		log("        is sampled at the same time as the FF would smaple the correspnding data\n");
+		log("        or async-data input whose value will be replaced with an abstract value.\n");
+		log("\n");
+		log("        The selection can be used to specify which state bits to abstract. For\n");
+		log("        each selected wire, any state bits that the wire is driven by will be\n");
+		log("        abstracted. For a selected FF cell, all of its state is abstracted.\n");
+		log("        Individual bits of a single wire can be abtracted using the -slice and\n");
+		log("        -rtlilslice options.\n");
+		log("\n");
+		log("    -init\n");
+		log("        The selected FFs will be modified to have an abstract initial value.\n");
+		log("        The -enable/-enablen options are not supported in this mode.\n");
+		log("        \n");
+		log("        The selection is used in the same way as it is for the -state mode.\n");
+		log("\n");
+		log("    -value\n");
+		log("        The drivers of the selected signals will be replaced with an abstract\n");
+		log("        value. In this mode, the abstract value can change at any time and is\n");
+		log("        not synchronized to any clock or other signal. Conditional abstraction\n");
+		log("        is supported with the -enable/-enablen options. The condition will\n");
+		log("        combinationally select between the original driver and the abstract\n");
+		log("        value.\n");
+		log("\n");
+		log("        The selection can be used to specify which output bits of which drivers\n");
+		log("        to abtract. For a selected cell, all its output bits will be abstracted.\n");
+		log("        For a selected wire, every output bit that is driving the wire will be\n");
+		log("        abstracted. Individual bits of a single wire can be abstracted using the\n");
+		log("        -slice and -rtlilslice options.\n");
+		log("\n");
+		log("    -enable <wire-name>\n");
+		log("    -enablen <wire-name>\n");
+		log("        Perform conditional abstraction with a named single bit wire as\n");
+		log("        condition. For -enable the wire is used as an active-high condition and\n");
+		log("        for -enablen as an active-low condition. See the description of the\n");
+		log("        -state and -value modes for details on how the condition affects the\n");
+		log("        abstractions performed by either mode. This option is not supported in\n");
+		log("        the -init mode.\n");
+		log("\n");
+		log("    -slice <lhs>:<rhs>\n");
+		log("    -slice <index>\n");
+		log("    -rtlilslice <lhs>:<rhs>\n");
+		log("    -rtlilslice <index>\n");
+		log("        Limit the abstraction to a slice of a single selected wire. The targeted\n");
+		log("        bits of the wire can be given as an inclusive range of indices or as a\n");
+		log("        single index. When using the -slice option, the indices are interpreted\n");
+		log("        following the source level declaration of the wire. This means the\n");
+		log("        -slice option will respect declarations with a non-zero-based index range\n");
+		log("        or with reversed bitorder. The -rtlilslice options will always use\n");
+		log("        zero-based indexing where index 0 corresponds to the least significant\n");
+		log("        bit of the wire.\n");
+		log("\n");
+	}
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override {
+		log_header(design, "Executing ABSTRACT pass.\n");
+
+		size_t argidx;
+		enum Mode {
+			None,
+			State,
+			Initial,
+			Value,
+		};
+		Mode mode = Mode::None;
+		enum Enable {
+			Always = -1,
+			ActiveLow = false, // ensuring we can use bool(enable)
+			ActiveHigh = true,
+		};
+		Enable enable = Enable::Always;
+		std::string enable_name;
+		std::vector<Slice> slices;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			std::string arg = args[argidx];
+			if (arg == "-state") {
+				mode = State;
+				continue;
+			}
+			if (arg == "-init") {
+				mode = Initial;
+				continue;
+			}
+			if (arg == "-value") {
+				mode = Value;
+				continue;
+			}
+			if (arg == "-enable" && argidx + 1 < args.size()) {
+				if (enable != Enable::Always)
+					log_cmd_error("Multiple enable condition are not supported\n");
+				enable_name = args[++argidx];
+				enable = Enable::ActiveHigh;
+				continue;
+			}
+			if (arg == "-enablen" && argidx + 1 < args.size()) {
+				if (enable != Enable::Always)
+					log_cmd_error("Multiple enable condition are not supported\n");
+				enable_name = args[++argidx];
+				enable = Enable::ActiveLow;
+				continue;
+			}
+			if (arg == "-slice" && argidx + 1 < args.size()) {
+				slices.emplace_back(SliceIndices::HdlSlice, args[++argidx]);
+				continue;
+			}
+			if (arg == "-rtlilslice" && argidx + 1 < args.size()) {
+				slices.emplace_back(SliceIndices::RtlilSlice, args[++argidx]);
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		if (enable != Enable::Always) {
+			if (mode == Mode::Initial)
+				log_cmd_error("Conditional initial value abstraction is not supported\n");
+
+			if (enable_name.empty())
+				log_cmd_error("Unspecified enable wire\n");
+		}
+
+		unsigned int changed = 0;
+		if ((mode == State) || (mode == Value)) {
+			for (auto mod : design->selected_modules()) {
+				EnableLogic enable_logic = { State::S1, true };
+				if (enable != Enable::Always) {
+					Wire *enable_wire = mod->wire("\\" + enable_name);
+					if (!enable_wire)
+						log_cmd_error("Enable wire %s not found in module %s\n", enable_name.c_str(), mod->name.c_str());
+					if (GetSize(enable_wire) != 1)
+						log_cmd_error("Enable wire %s must have width 1 but has width %d in module %s\n",
+								enable_name.c_str(), GetSize(enable_wire), mod->name.c_str());
+					enable_logic = { enable_wire, enable == Enable::ActiveHigh };
+				}
+				if (mode == State)
+					changed += abstract_state(mod, enable_logic, slices);
+				else
+					changed += abstract_value(mod, enable_logic, slices);
+			}
+			if (mode == State)
+				log("Abstracted %d stateful cells.\n", changed);
+			else
+				log("Abstracted %d driver ports.\n", changed);
+		} else if (mode == Initial) {
+			for (auto mod : design->selected_modules()) {
+				changed += abstract_init(mod, slices);
+			}
+			log("Abstracted %d init bits.\n", changed);
+		} else {
+			log_cmd_error("No mode selected, see help message\n");
+		}
+	}
+} AbstractPass;
+
+PRIVATE_NAMESPACE_END

tests/unit/kernel/rtlilTest.cc

@@ -5,7 +5,22 @@ YOSYS_NAMESPACE_BEGIN
 
 namespace RTLIL {
 
-	class KernelRtlilTest : public testing::Test {};
+	struct SafePrintToStringParamName {
+		template <class ParamType>
+		std::string operator()(const testing::TestParamInfo<ParamType>& info) const {
+			std::string name = testing::PrintToString(info.param);
+			for (auto &c : name)
+				if (!('0' <= c && c <= '9') && !('a' <= c && c <= 'z') && !('A' <= c && c <= 'Z')  ) c = '_';
+			return name;
+		}
+	};
+
+	class KernelRtlilTest : public testing::Test {
+	protected:
+		KernelRtlilTest() {
+			if (log_files.empty()) log_files.emplace_back(stdout);
+		}
+	};
 
 	TEST_F(KernelRtlilTest, ConstAssignCompare)
 	{
@@ -74,6 +89,83 @@ namespace RTLIL {
 		}
 
 	}
+
+	class WireRtlVsHdlIndexConversionTest :
+		public KernelRtlilTest,
+		public testing::WithParamInterface<std::tuple<bool, int, int>>
+	{};
+
+	INSTANTIATE_TEST_SUITE_P(
+		WireRtlVsHdlIndexConversionInstance,
+		WireRtlVsHdlIndexConversionTest,
+		testing::Values(
+			std::make_tuple(false, 0, 10),
+			std::make_tuple(true, 0, 10),
+			std::make_tuple(false, 4, 10),
+			std::make_tuple(true, 4, 10),
+			std::make_tuple(false, -4, 10),
+			std::make_tuple(true, -4, 10),
+			std::make_tuple(false, 0, 1),
+			std::make_tuple(true, 0, 1),
+			std::make_tuple(false, 4, 1),
+			std::make_tuple(true, 4, 1),
+			std::make_tuple(false, -4, 1),
+			std::make_tuple(true, -4, 1)
+		),
+		SafePrintToStringParamName()
+	);
+
+	TEST_P(WireRtlVsHdlIndexConversionTest, WireRtlVsHdlIndexConversion) {
+		std::unique_ptr<Module> mod = std::make_unique<Module>();
+		Wire *wire = mod->addWire(ID(test), 10);
+
+		auto [upto, start_offset, width] = GetParam();
+
+		wire->upto = upto;
+		wire->start_offset = start_offset;
+		wire->width = width;
+
+		int smallest = INT_MAX;
+		int largest = INT_MIN;
+
+		for (int i = 0; i < wire->width; i++) {
+			int j = wire->to_hdl_index(i);
+			smallest = std::min(smallest, j);
+			largest = std::max(largest, j);
+			EXPECT_EQ(
+				std::make_pair(wire->from_hdl_index(j), j),
+				std::make_pair(i, wire->to_hdl_index(i))
+			);
+		}
+
+		EXPECT_EQ(smallest, start_offset);
+		EXPECT_EQ(largest, start_offset + wire->width - 1);
+
+		for (int i = 1; i < wire->width; i++) {
+			EXPECT_EQ(
+				wire->to_hdl_index(i) - wire->to_hdl_index(i - 1),
+				upto ? -1 : 1
+			);
+		}
+
+		for (int j = smallest; j < largest; j++) {
+			int i = wire->from_hdl_index(j);
+			EXPECT_EQ(
+				std::make_pair(wire->from_hdl_index(j), j),
+				std::make_pair(i, wire->to_hdl_index(i))
+			);
+		}
+
+		for (int i = -10; i < 0; i++)
+			EXPECT_EQ(wire->to_hdl_index(i), INT_MIN);
+		for (int i = wire->width; i < wire->width + 10; i++)
+			EXPECT_EQ(wire->to_hdl_index(i), INT_MIN);
+		for (int j = smallest - 10; j < smallest; j++)
+			EXPECT_EQ(wire->from_hdl_index(j), INT_MIN);
+		for (int j = largest + 1; j < largest + 11; j++)
+			EXPECT_EQ(wire->from_hdl_index(j), INT_MIN);
+	}
+
 }
 
 YOSYS_NAMESPACE_END

tests/various/abstract_init.ys

@@ -0,0 +1,121 @@
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q, QQQ);
+	input CLK;
+	output reg QQQ;
+	output reg Q = 1'b1;
+	assign QQQ = Q;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init %i
+abstract -init w:QQQ
+check -assert
+select -assert-count 0 w:Q a:init %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q, QQQ);
+	input CLK;
+	output reg QQQ;
+	output reg [1:0] Q = 1'b1;
+	assign QQQ = Q;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init w:QQQ
+check -assert
+select -assert-count 1 w:Q a:init=2'b0x %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         downto
+	output reg [1:0] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+design -save basic
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -slice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'b0x %i
+design -load basic
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -slice 0:1 w:Q
+check -assert
+select -assert-count 0 w:Q a:init %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         downto
+	output reg [1:0] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -rtlilslice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'b0x %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         upto
+	output reg [0:1] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -slice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'bx1 %i
+
+design -reset
+read_verilog <<EOT
+module foo (CLK, Q);
+	input CLK;
+	//         upto
+	output reg [0:1] Q = 1'b1;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+EOT
+
+proc
+opt_expr
+opt_dff
+select -assert-count 1 w:Q a:init=2'b01 %i
+abstract -init -rtlilslice 0 w:Q
+check -assert
+select -assert-count 1 w:Q a:init=2'b0x %i

tests/various/abstract_state.ys

@@ -0,0 +1,178 @@
+read_verilog <<EOT
+
+module half_clock (CLK, Q, magic);
+	input CLK;
+	output reg Q;
+	input magic;
+	always @(posedge CLK)
+		Q <= ~Q;
+endmodule
+
+EOT
+proc
+design -save half_clock
+
+# -----------------------------------------------------------------------------
+# An empty selection causes no change
+select -none
+
+logger -expect log "Abstracted 0 stateful cells" 1
+	abstract -state -enablen magic
+logger -check-expected
+
+logger -expect log "Abstracted 0 init bits" 1
+	abstract -init
+logger -check-expected
+
+logger -expect log "Abstracted 0 driver ports" 1
+	abstract -value -enablen magic
+logger -check-expected
+
+select -clear
+# -----------------------------------------------------------------------------
+design -load half_clock
+# Basic -state test
+abstract -state -enablen magic
+check -assert
+# Connections to dff D input port
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+# The D input port is fed with a mux
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+# The S input port is fed with the magic wire
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# The A input port is fed with an anyseq
+select -assert-count 1 @mux %x:+[A] %ci t:$anyseq %i
+# The B input port is fed with the negated Q
+select -set not @mux %x:+[B] %ci t:$not %i
+select -assert-count 1 @not %x:+[A] o:Q %i
+
+design -load half_clock
+# Same thing, inverted polarity
+abstract -state -enable magic
+check -assert
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# so we get swapped A and B
+select -assert-count 1 @mux %x:+[B] %ci t:$anyseq %i
+select -set not @mux %x:+[A] %ci t:$not %i
+select -assert-count 1 @not %x:+[A] o:Q %i
+# -----------------------------------------------------------------------------
+design -reset
+read_verilog <<EOT
+module wide_flop_no_q (CLK, DDD, QQQ, magic);
+	input CLK;
+	input [2:0] DDD;
+	output reg [2:0] QQQ;
+	input magic;
+	always @(posedge CLK)
+		QQQ <= DDD;
+endmodule
+EOT
+proc
+opt_expr
+opt_dff
+dump
+abstract -state -enablen magic -slice 0 w:QQQ
+check -assert
+# Connections to dff D input port
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+# The D input port is partially fed with a mux
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+# and also the DDD input
+select -assert-count 1 @conn_to_d w:DDD %i
+# The S input port is fed with the magic wire
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# The A input port is fed with an anyseq
+select -assert-count 1 @mux %x:+[A] %ci t:$anyseq %i
+# The B input port is fed with DDD
+select -assert-count 1 @mux %x:+[B] %ci w:DDD %i
+# -----------------------------------------------------------------------------
+# Selecting wire Q connected to bit 0 of QQQ is the same as specifying
+# QQQ with the -slice 0 argument
+design -reset
+read_verilog <<EOT
+module wide_flop (CLK, DDD, QQQ, Q, magic);
+	input CLK;
+	input [2:0] DDD;
+	output reg [2:0] QQQ;
+	output reg Q;
+	input magic;
+	always @(posedge CLK)
+		QQQ <= DDD;
+	assign Q = QQQ[0];
+endmodule
+EOT
+proc
+design -save wide_flop
+# Test that abstracting an output slice muxes an input slice
+abstract -state -enablen magic w:Q
+check -assert
+# Same testing as previous case
+select -set conn_to_d t:$dff %x:+[D] t:$dff %d
+select -set mux @conn_to_d %ci t:$mux %i
+select -assert-count 1 @mux
+select -assert-count 1 @conn_to_d w:DDD %i
+select -assert-count 1 @mux %x:+[S] w:magic %i
+select -assert-count 1 @mux %x:+[A] %ci t:$anyseq %i
+select -assert-count 1 @mux %x:+[B] %ci w:DDD %i
+# -----------------------------------------------------------------------------
+design -reset
+read_verilog <<EOT
+module half_clock_en (CLK, E, Q, magic);
+	input CLK;
+	input E;
+	output reg Q;
+	input magic;
+	always @(posedge CLK)
+        if (E)
+            Q <= ~Q;
+endmodule
+EOT
+proc
+opt_expr
+opt_dff
+design -save half_clock_en
+# Test that abstracting a $dffe unmaps the enable
+select -assert-count 1 t:$dffe
+abstract -state -enablen magic
+check -assert
+select -assert-count 0 t:$dffe
+select -assert-count 1 t:$dff
+# -----------------------------------------------------------------------------
+design -reset
+read_verilog <<EOT
+module top (CLK, E, Q, Q_EN);
+	input CLK;
+	input E;
+	output reg Q;
+	output reg Q_EN;
+	half_clock uut (CLK, Q, 1'b0);
+	half_clock_en uut_en (CLK, E, Q_EN, 1'b0);
+endmodule
+EOT
+proc
+design -import half_clock
+design -import half_clock_en
+hierarchy -check -top top
+# Test when the abstraction is disabled (enable is inactive),
+# the equivalence is preserved
+rename top top_gold
+design -save gold
+abstract -state -enable magic half_clock half_clock_en
+flatten
+rename top_gold top_gate
+design -save gate
+design -load gold
+flatten
+design -import gate -as top_gate
+
+equiv_make top_gold top_gate equiv
+equiv_induct equiv
+equiv_status -assert equiv
+# The reader may verify that this model checking is functional
+# by changing -enable to -enablen in the abstract pass invocation above
+# -----------------------------------------------------------------------------

tests/various/abstract_value.ys

@@ -0,0 +1,95 @@
+read_verilog <<EOT
+module split_output (A, B, Y, magic);
+	input [1:0] A;
+	input [1:0] B;
+	output [1:0] Y;
+	input magic;
+    wire W;
+    assign Y = A + B;
+    assign W = Y[0]; // <--- look here
+endmodule
+EOT
+proc
+design -save split_output
+# Basic -value test
+abstract -value -enable magic w:W
+check -assert
+# Connections to $add Y output port
+select -set conn_to_y t:$add %x:+[Y] t:$add %d
+# The $add Y output port feeds partially into a mux
+select -set mux @conn_to_y %ci t:$mux %i
+select -assert-count 1 @mux
+# and also the Y module output
+select -assert-count 1 @conn_to_y %a o:Y %i
+# The S input port is fed with the magic wire
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# The B input port is fed with an anyseq
+select -assert-count 1 @mux %x:+[B] %ci t:$anyseq %i
+# The Y output port feeds into the Y module output
+select -assert-count 1 @mux %x:+[Y] %co o:Y %i
+# -----------------------------------------------------------------------------
+# Same thing, but we use -slice instead of wire W
+design -reset
+read_verilog <<EOT
+module split_output_no_w (A, B, Y, magic);
+	input [1:0] A;
+	input [1:0] B;
+	output [1:0] Y;
+	input magic;
+    assign Y = A + B;
+endmodule
+EOT
+proc
+# Same test as the previous case
+abstract -value -enable magic -slice 0 w:Y
+check -assert
+select -set conn_to_y t:$add %x:+[Y] t:$add %d
+select -set mux @conn_to_y %ci t:$mux %i
+select -assert-count 1 @mux
+select -assert-count 1 @conn_to_y %a o:Y %i
+select -assert-count 1 @mux %x:+[S] w:magic %i
+select -assert-count 1 @mux %x:+[B] %ci t:$anyseq %i
+select -assert-count 1 @mux %x:+[Y] %co o:Y %i
+# -----------------------------------------------------------------------------
+design -reset
+read_verilog <<EOT
+module split_input (A, B, Y, magic);
+	input [1:0] A;
+	input [1:0] B;
+	output [1:0] Y;
+	input magic;
+    wire W;
+    assign Y = A + B;
+    assign W = A[0]; // <--- look here
+endmodule
+EOT
+proc
+design -save split_input
+# The mux goes on an input this time
+abstract -value -enable magic w:W
+check -assert
+# Connections to add A input port
+select -set conn_to_a t:$add %x:+[A] t:$add %d
+# The B input port is partially fed with a mux
+select -set mux @conn_to_a %ci t:$mux %i
+select -assert-count 1 @mux
+# and also the A input
+select -assert-count 1 @conn_to_a %a w:A %i
+# The S input port is fed with the magic wire
+select -assert-count 1 @mux %x:+[S] w:magic %i
+# The A input port is fed with the module input A
+select -assert-count 1 @mux %x:+[A] %ci i:A %i
+# The B input port is fed with an anyseq
+select -assert-count 1 @mux %x:+[B] %ci t:$anyseq %i
+# -----------------------------------------------------------------------------
+# All wires selected, excluding magic -> muxes on inputs and outputs
+design -load split_output
+select -assert-count 0 t:$mux
+abstract -value -enable magic w:* w:magic %d
+select -assert-count 3 t:$mux
+# All cells selected -> muxes on outputs only
+design -load split_output
+select -assert-count 0 t:$mux
+abstract -value -enable magic t:*
+select -assert-count 1 t:$mux
+# -----------------------------------------------------------------------------