yosys/frontends/verific/verific.cc

/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
 *
 *  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/log.h"
#include <stdlib.h>
#include <stdio.h>
#include <string.h>

#ifndef _WIN32
#  include <unistd.h>
#  include <dirent.h>
#endif

#include "frontends/verific/verific.h"

USING_YOSYS_NAMESPACE

#ifdef YOSYS_ENABLE_VERIFIC

#ifdef __clang__
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Woverloaded-virtual"
#endif

#include "veri_file.h"
#include "vhdl_file.h"
#include "VeriModule.h"
#include "VeriWrite.h"
#include "VhdlUnits.h"
#include "Message.h"

#ifdef __clang__
#pragma clang diagnostic pop
#endif

#ifdef VERIFIC_NAMESPACE
using namespace Verific;
#endif

#endif

#ifdef YOSYS_ENABLE_VERIFIC
YOSYS_NAMESPACE_BEGIN

int verific_verbose;
string verific_error_msg;

void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
{
	string message_prefix = stringf("VERIFIC-%s [%s] ",
			msg_type == VERIFIC_NONE ? "NONE" :
			msg_type == VERIFIC_ERROR ? "ERROR" :
			msg_type == VERIFIC_WARNING ? "WARNING" :
			msg_type == VERIFIC_IGNORE ? "IGNORE" :
			msg_type == VERIFIC_INFO ? "INFO" :
			msg_type == VERIFIC_COMMENT ? "COMMENT" :
			msg_type == VERIFIC_PROGRAM_ERROR ? "PROGRAM_ERROR" : "UNKNOWN", message_id);

	string message = linefile ? stringf("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile)) : "";
	message += vstringf(msg, args);

	if (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_WARNING || msg_type == VERIFIC_PROGRAM_ERROR)
		log_warning_noprefix("%s%s\n", message_prefix.c_str(), message.c_str());
	else
		log("%s%s\n", message_prefix.c_str(), message.c_str());

	if (verific_error_msg.empty() && (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_PROGRAM_ERROR))
		verific_error_msg = message;
}

string get_full_netlist_name(Netlist *nl)
{
	if (nl->NumOfRefs() == 1) {
		Instance *inst = (Instance*)nl->GetReferences()->GetLast();
		return get_full_netlist_name(inst->Owner()) + "." + inst->Name();
	}

	return nl->CellBaseName();
}

// ==================================================================

VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names) :
		mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
		mode_names(mode_names)
{
}

RTLIL::SigBit VerificImporter::net_map_at(Net *net)
{
	if (net->IsExternalTo(netlist))
		log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
				get_full_netlist_name(net->Owner()).c_str(), net->Name(), get_full_netlist_name(netlist).c_str());

	return net_map.at(net);
}

void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
{
	MapIter mi;
	Att *attr;

	if (obj->Linefile())
		attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));

	// FIXME: Parse numeric attributes
	FOREACH_ATTRIBUTE(obj, mi, attr)
		attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
}

RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
{
	RTLIL::SigSpec sig;
	for (int i = int(inst->InputSize())-1; i >= 0; i--)
		if (inst->GetInputBit(i))
			sig.append(net_map_at(inst->GetInputBit(i)));
		else
			sig.append(RTLIL::State::Sz);
	return sig;
}

RTLIL::SigSpec VerificImporter::operatorInput1(Instance *inst)
{
	RTLIL::SigSpec sig;
	for (int i = int(inst->Input1Size())-1; i >= 0; i--)
		if (inst->GetInput1Bit(i))
			sig.append(net_map_at(inst->GetInput1Bit(i)));
		else
			sig.append(RTLIL::State::Sz);
	return sig;
}

RTLIL::SigSpec VerificImporter::operatorInput2(Instance *inst)
{
	RTLIL::SigSpec sig;
	for (int i = int(inst->Input2Size())-1; i >= 0; i--)
		if (inst->GetInput2Bit(i))
			sig.append(net_map_at(inst->GetInput2Bit(i)));
		else
			sig.append(RTLIL::State::Sz);
	return sig;
}

RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portname)
{
	PortBus *portbus = inst->View()->GetPortBus(portname);
	if (portbus) {
		RTLIL::SigSpec sig;
		for (unsigned i = 0; i < portbus->Size(); i++) {
			Net *net = inst->GetNet(portbus->ElementAtIndex(i));
			if (net) {
				if (net->IsGnd())
					sig.append(RTLIL::State::S0);
				else if (net->IsPwr())
					sig.append(RTLIL::State::S1);
				else
					sig.append(net_map_at(net));
			} else
				sig.append(RTLIL::State::Sz);
		}
		return sig;
	} else {
		Port *port = inst->View()->GetPort(portname);
		log_assert(port != NULL);
		Net *net = inst->GetNet(port);
		return net_map_at(net);
	}
}

RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst)
{
	RTLIL::SigSpec sig;
	RTLIL::Wire *dummy_wire = NULL;
	for (int i = int(inst->OutputSize())-1; i >= 0; i--)
		if (inst->GetOutputBit(i)) {
			sig.append(net_map_at(inst->GetOutputBit(i)));
			dummy_wire = NULL;
		} else {
			if (dummy_wire == NULL)
				dummy_wire = module->addWire(NEW_ID);
			else
				dummy_wire->width++;
			sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
		}
	return sig;
}

bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
{
	if (inst->Type() == PRIM_AND) {
		module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_NAND) {
		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
		module->addAndGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
		module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_OR) {
		module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_NOR) {
		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
		module->addOrGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
		module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_XOR) {
		module->addXorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_XNOR) {
		module->addXnorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_BUF) {
		module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_INV) {
		module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_MUX) {
		module->addMuxGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_TRI) {
		module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_FADD)
	{
		RTLIL::SigSpec a = net_map_at(inst->GetInput1()), b = net_map_at(inst->GetInput2()), c = net_map_at(inst->GetCin());
		RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(NEW_ID);
		RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
		RTLIL::SigSpec tmp1 = module->addWire(NEW_ID);
		RTLIL::SigSpec tmp2 = module->addWire(NEW_ID);
		RTLIL::SigSpec tmp3 = module->addWire(NEW_ID);
		module->addXorGate(NEW_ID, a, b, tmp1);
		module->addXorGate(inst_name, tmp1, c, y);
		module->addAndGate(NEW_ID, tmp1, c, tmp2);
		module->addAndGate(NEW_ID, a, b, tmp3);
		module->addOrGate(NEW_ID, tmp2, tmp3, x);
		return true;
	}

	if (inst->Type() == PRIM_DFFRS)
	{
		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
			module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		else if (inst->GetSet()->IsGnd())
			module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false);
		else if (inst->GetReset()->IsGnd())
			module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true);
		else
			module->addDffsrGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		return true;
	}

	return false;
}

bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
{
	if (inst->Type() == PRIM_AND) {
		module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_NAND) {
		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
		module->addAnd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
		module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_OR) {
		module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_NOR) {
		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
		module->addOr(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
		module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_XOR) {
		module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_XNOR) {
		module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_INV) {
		module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_MUX) {
		module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_TRI) {
		module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_FADD)
	{
		RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
		RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(NEW_ID);
		if (inst->GetCout())
			y.append(net_map_at(inst->GetCout()));
		module->addAdd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
		module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
		return true;
	}

	if (inst->Type() == PRIM_DFFRS)
	{
		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
			module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		else if (inst->GetSet()->IsGnd())
			module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()),
					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
		else if (inst->GetReset()->IsGnd())
			module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()),
					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
		else
			module->addDffsr(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == PRIM_DLATCHRS)
	{
		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
			module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		else
			module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
					net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
		return true;
	}

	#define IN  operatorInput(inst)
	#define IN1 operatorInput1(inst)
	#define IN2 operatorInput2(inst)
	#define OUT operatorOutput(inst)
	#define SIGNED inst->View()->IsSigned()

	if (inst->Type() == OPER_ADDER) {
		RTLIL::SigSpec out = OUT;
		if (inst->GetCout() != NULL)
			out.append(net_map_at(inst->GetCout()));
		if (inst->GetCin()->IsGnd()) {
			module->addAdd(inst_name, IN1, IN2, out, SIGNED);
		} else {
			RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
			module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
			module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
		}
		return true;
	}

	if (inst->Type() == OPER_MULTIPLIER) {
		module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_DIVIDER) {
		module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_MODULO) {
		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_REMAINDER) {
		module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_SHIFT_LEFT) {
		module->addShl(inst_name, IN1, IN2, OUT, false);
		return true;
	}

	if (inst->Type() == OPER_ENABLED_DECODER) {
		RTLIL::SigSpec vec;
		vec.append(net_map_at(inst->GetControl()));
		for (unsigned i = 1; i < inst->OutputSize(); i++) {
			vec.append(RTLIL::State::S0);
		}
		module->addShl(inst_name, vec, IN, OUT, false);
		return true;
	}

	if (inst->Type() == OPER_DECODER) {
		RTLIL::SigSpec vec;
		vec.append(RTLIL::State::S1);
		for (unsigned i = 1; i < inst->OutputSize(); i++) {
			vec.append(RTLIL::State::S0);
		}
		module->addShl(inst_name, vec, IN, OUT, false);
		return true;
	}

	if (inst->Type() == OPER_SHIFT_RIGHT) {
		Net *net_cin = inst->GetCin();
		Net *net_a_msb = inst->GetInput1Bit(0);
		if (net_cin->IsGnd())
			module->addShr(inst_name, IN1, IN2, OUT, false);
		else if (net_cin == net_a_msb)
			module->addSshr(inst_name, IN1, IN2, OUT, true);
		else
			log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
		return true;
	}

	if (inst->Type() == OPER_REDUCE_AND) {
		module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
		return true;
	}

	if (inst->Type() == OPER_REDUCE_OR) {
		module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
		return true;
	}

	if (inst->Type() == OPER_REDUCE_XOR) {
		module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
		return true;
	}

	if (inst->Type() == OPER_REDUCE_XNOR) {
		module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
		return true;
	}

	if (inst->Type() == OPER_REDUCE_NOR) {
		SigSpec t = module->ReduceOr(NEW_ID, IN, SIGNED);
		module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == OPER_LESSTHAN) {
		Net *net_cin = inst->GetCin();
		if (net_cin->IsGnd())
			module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
		else if (net_cin->IsPwr())
			module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
		else
			log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
		return true;
	}

	if (inst->Type() == OPER_WIDE_AND) {
		module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_WIDE_OR) {
		module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_WIDE_XOR) {
		module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_WIDE_XNOR) {
		module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_WIDE_BUF) {
		module->addPos(inst_name, IN, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_WIDE_INV) {
		module->addNot(inst_name, IN, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_MINUS) {
		module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_UMINUS) {
		module->addNeg(inst_name, IN, OUT, SIGNED);
		return true;
	}

	if (inst->Type() == OPER_EQUAL) {
		module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
		return true;
	}

	if (inst->Type() == OPER_NEQUAL) {
		module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
		return true;
	}

	if (inst->Type() == OPER_WIDE_MUX) {
		module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
		return true;
	}

	if (inst->Type() == OPER_NTO1MUX) {
		module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == OPER_WIDE_NTO1MUX)
	{
		SigSpec data = IN2, out = OUT;

		int wordsize_bits = ceil_log2(GetSize(out));
		int wordsize = 1 << wordsize_bits;

		SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)};

		SigSpec padded_data;
		for (int i = 0; i < GetSize(data); i += GetSize(out)) {
			SigSpec d = data.extract(i, GetSize(out));
			d.extend_u0(wordsize);
			padded_data.append(d);
		}

		module->addShr(inst_name, padded_data, sel, out);
		return true;
	}

	if (inst->Type() == OPER_SELECTOR)
	{
		module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
		return true;
	}

	if (inst->Type() == OPER_WIDE_SELECTOR)
	{
		SigSpec out = OUT;
		module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
		return true;
	}

	if (inst->Type() == OPER_WIDE_TRI) {
		module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
		return true;
	}

	if (inst->Type() == OPER_WIDE_DFFRS) {
		RTLIL::SigSpec sig_set = operatorInport(inst, "set");
		RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
		if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
			module->addDff(inst_name, net_map_at(inst->GetClock()), IN, OUT);
		else
			module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
		return true;
	}

	#undef IN
	#undef IN1
	#undef IN2
	#undef OUT
	#undef SIGNED

	return false;
}

void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
{
	bool keep_running = true;
	SigMap sigmap;

	while (keep_running)
	{
		keep_running = false;

		dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
		SigSpec dbits;

		for (auto cell : candidates) {
			SigBit bit = sigmap(cell->getPort("\\D"));
			dbits_db[bit].insert(cell);
			dbits.append(bit);
		}

		dbits.sort_and_unify();

		for (auto chunk : dbits.chunks())
		{
			SigSpec sig_d = chunk;

			if (chunk.wire == nullptr || GetSize(sig_d) == 1)
				continue;

			SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
			RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);

			if (verific_verbose)
				log("  merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));

			for (int i = 0; i < GetSize(sig_d); i++)
				for (auto old_ff : dbits_db[sig_d[i]])
				{
					if (verific_verbose)
						log("    replacing old ff %s on bit %d.\n", log_id(old_ff), i);

					SigBit old_q = old_ff->getPort("\\Q");
					SigBit new_q = sig_q[i];

					sigmap.add(old_q, new_q);
					module->connect(old_q, new_q);
					candidates.erase(old_ff);
					module->remove(old_ff);
					keep_running = true;
				}
		}
	}
}

void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
{
	dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;

	for (auto cell : candidates)
	{
		SigBit clock = cell->getPort("\\CLK");
		bool clock_pol = cell->getParam("\\CLK_POLARITY").as_bool();
		database[make_pair(clock, int(clock_pol))].insert(cell);
	}

	for (auto it : database)
		merge_past_ffs_clock(it.second, it.first.first, it.first.second);
}

void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
{
	std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());

	netlist = nl;

	if (design->has(module_name)) {
		if (!nl->IsOperator())
			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
		return;
	}

	module = new RTLIL::Module;
	module->name = module_name;
	design->add(module);

	if (nl->IsBlackBox()) {
		log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
		module->set_bool_attribute("\\blackbox");
	} else {
		log("Importing module %s.\n", RTLIL::id2cstr(module->name));
	}

	SetIter si;
	MapIter mi, mi2;
	Port *port;
	PortBus *portbus;
	Net *net;
	NetBus *netbus;
	Instance *inst;
	PortRef *pr;

	FOREACH_PORT_OF_NETLIST(nl, mi, port)
	{
		if (port->Bus())
			continue;

		if (verific_verbose)
			log("  importing port %s.\n", port->Name());

		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
		import_attributes(wire->attributes, port);

		wire->port_id = nl->IndexOf(port) + 1;

		if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
			wire->port_input = true;
		if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
			wire->port_output = true;

		if (port->GetNet()) {
			net = port->GetNet();
			if (net_map.count(net) == 0)
				net_map[net] = wire;
			else if (wire->port_input)
				module->connect(net_map_at(net), wire);
			else
				module->connect(wire, net_map_at(net));
		}
	}

	FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
	{
		if (verific_verbose)
			log("  importing portbus %s.\n", portbus->Name());

		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
		wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
		import_attributes(wire->attributes, portbus);

		if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
			wire->port_input = true;
		if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
			wire->port_output = true;

		for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
			if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
				net = portbus->ElementAtIndex(i)->GetNet();
				RTLIL::SigBit bit(wire, i - wire->start_offset);
				if (net_map.count(net) == 0)
					net_map[net] = bit;
				else if (wire->port_input)
					module->connect(net_map_at(net), bit);
				else
					module->connect(bit, net_map_at(net));
			}
			if (i == portbus->RightIndex())
				break;
		}
	}

	module->fixup_ports();

	dict<Net*, char, hash_ptr_ops> init_nets;
	pool<Net*, hash_ptr_ops> anyconst_nets;
	pool<Net*, hash_ptr_ops> anyseq_nets;

	FOREACH_NET_OF_NETLIST(nl, mi, net)
	{
		if (net->IsRamNet())
		{
			RTLIL::Memory *memory = new RTLIL::Memory;
			memory->name = RTLIL::escape_id(net->Name());
			log_assert(module->count_id(memory->name) == 0);
			module->memories[memory->name] = memory;

			int number_of_bits = net->Size();
			int bits_in_word = number_of_bits;
			FOREACH_PORTREF_OF_NET(net, si, pr) {
				if (pr->GetInst()->Type() == OPER_READ_PORT) {
					bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
					continue;
				}
				if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
					bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
					continue;
				}
				log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
						net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
			}

			memory->width = bits_in_word;
			memory->size = number_of_bits / bits_in_word;

			const char *ascii_initdata = net->GetWideInitialValue();
			if (ascii_initdata) {
				while (*ascii_initdata != 0 && *ascii_initdata != '\'')
					ascii_initdata++;
				if (*ascii_initdata == '\'')
					ascii_initdata++;
				if (*ascii_initdata != 0) {
					log_assert(*ascii_initdata == 'b');
					ascii_initdata++;
				}
				for (int word_idx = 0; word_idx < memory->size; word_idx++) {
					Const initval = Const(State::Sx, memory->width);
					bool initval_valid = false;
					for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
						if (*ascii_initdata == 0)
							break;
						if (*ascii_initdata == '0' || *ascii_initdata == '1') {
							initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
							initval_valid = true;
						}
						ascii_initdata++;
					}
					if (initval_valid) {
						RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit");
						cell->parameters["\\WORDS"] = 1;
						if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
							cell->setPort("\\ADDR", word_idx);
						else
							cell->setPort("\\ADDR", memory->size - word_idx - 1);
						cell->setPort("\\DATA", initval);
						cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str());
						cell->parameters["\\ABITS"] = 32;
						cell->parameters["\\WIDTH"] = memory->width;
						cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1);
					}
				}
			}
			continue;
		}

		if (net->GetInitialValue())
			init_nets[net] = net->GetInitialValue();

		const char *rand_const_attr = net->GetAttValue(" rand_const");
		const char *rand_attr = net->GetAttValue(" rand");

		if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
			anyconst_nets.insert(net);

		else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
			anyseq_nets.insert(net);

		if (net_map.count(net)) {
			if (verific_verbose)
				log("  skipping net %s.\n", net->Name());
			continue;
		}

		if (net->Bus())
			continue;

		RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID);

		if (verific_verbose)
			log("  importing net %s as %s.\n", net->Name(), log_id(wire_name));

		RTLIL::Wire *wire = module->addWire(wire_name);
		import_attributes(wire->attributes, net);

		net_map[net] = wire;
	}

	FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
	{
		bool found_new_net = false;
		for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
			net = netbus->ElementAtIndex(i);
			if (net_map.count(net) == 0)
				found_new_net = true;
			if (i == netbus->RightIndex())
				break;
		}

		if (found_new_net)
		{
			RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID);

			if (verific_verbose)
				log("  importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));

			RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
			wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
			import_attributes(wire->attributes, netbus);

			RTLIL::Const initval = Const(State::Sx, GetSize(wire));
			bool initval_valid = false;

			for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
			{
				if (netbus->ElementAtIndex(i))
				{
					int bitidx = i - wire->start_offset;
					net = netbus->ElementAtIndex(i);
					RTLIL::SigBit bit(wire, bitidx);

					if (init_nets.count(net)) {
						if (init_nets.at(net) == '0')
							initval.bits.at(bitidx) = State::S0;
						if (init_nets.at(net) == '1')
							initval.bits.at(bitidx) = State::S1;
						initval_valid = true;
						init_nets.erase(net);
					}

					if (net_map.count(net) == 0)
						net_map[net] = bit;
					else
						module->connect(bit, net_map_at(net));
				}

				if (i == netbus->RightIndex())
					break;
			}

			if (initval_valid)
				wire->attributes["\\init"] = initval;
		}
		else
		{
			if (verific_verbose)
				log("  skipping netbus %s.\n", netbus->Name());
		}

		SigSpec anyconst_sig;
		SigSpec anyseq_sig;

		for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
			net = netbus->ElementAtIndex(i);
			if (net != nullptr && anyconst_nets.count(net)) {
				anyconst_sig.append(net_map_at(net));
				anyconst_nets.erase(net);
			}
			if (net != nullptr && anyseq_nets.count(net)) {
				anyseq_sig.append(net_map_at(net));
				anyseq_nets.erase(net);
			}
			if (i == netbus->LeftIndex())
				break;
		}

		if (GetSize(anyconst_sig))
			module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));

		if (GetSize(anyseq_sig))
			module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
	}

	for (auto it : init_nets)
	{
		Const initval;
		SigBit bit = net_map_at(it.first);
		log_assert(bit.wire);

		if (bit.wire->attributes.count("\\init"))
			initval = bit.wire->attributes.at("\\init");

		while (GetSize(initval) < GetSize(bit.wire))
			initval.bits.push_back(State::Sx);

		if (it.second == '0')
			initval.bits.at(bit.offset) = State::S0;
		if (it.second == '1')
			initval.bits.at(bit.offset) = State::S1;

		bit.wire->attributes["\\init"] = initval;
	}

	for (auto net : anyconst_nets)
		module->connect(net_map_at(net), module->Anyconst(NEW_ID));

	for (auto net : anyseq_nets)
		module->connect(net_map_at(net), module->Anyseq(NEW_ID));

	pool<Instance*, hash_ptr_ops> sva_asserts;
	pool<Instance*, hash_ptr_ops> sva_assumes;
	pool<Instance*, hash_ptr_ops> sva_covers;

	pool<RTLIL::Cell*> past_ffs;

	FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
	{
		RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID);

		if (verific_verbose)
			log("  importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));

		if (inst->Type() == PRIM_PWR) {
			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
			continue;
		}

		if (inst->Type() == PRIM_GND) {
			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
			continue;
		}

		if (inst->Type() == PRIM_BUF) {
			module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
			continue;
		}

		if (inst->Type() == PRIM_X) {
			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
			continue;
		}

		if (inst->Type() == PRIM_Z) {
			module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
			continue;
		}

		if (inst->Type() == OPER_READ_PORT)
		{
			RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
			if (memory->width != int(inst->OutputSize()))
				log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());

			RTLIL::SigSpec addr = operatorInput1(inst);
			RTLIL::SigSpec data = operatorOutput(inst);

			RTLIL::Cell *cell = module->addCell(inst_name, "$memrd");
			cell->parameters["\\MEMID"] = memory->name.str();
			cell->parameters["\\CLK_ENABLE"] = false;
			cell->parameters["\\CLK_POLARITY"] = true;
			cell->parameters["\\TRANSPARENT"] = false;
			cell->parameters["\\ABITS"] = GetSize(addr);
			cell->parameters["\\WIDTH"] = GetSize(data);
			cell->setPort("\\CLK", RTLIL::State::Sx);
			cell->setPort("\\EN", RTLIL::State::Sx);
			cell->setPort("\\ADDR", addr);
			cell->setPort("\\DATA", data);
			continue;
		}

		if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
		{
			RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
			if (memory->width != int(inst->Input2Size()))
				log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());

			RTLIL::SigSpec addr = operatorInput1(inst);
			RTLIL::SigSpec data = operatorInput2(inst);

			RTLIL::Cell *cell = module->addCell(inst_name, "$memwr");
			cell->parameters["\\MEMID"] = memory->name.str();
			cell->parameters["\\CLK_ENABLE"] = false;
			cell->parameters["\\CLK_POLARITY"] = true;
			cell->parameters["\\PRIORITY"] = 0;
			cell->parameters["\\ABITS"] = GetSize(addr);
			cell->parameters["\\WIDTH"] = GetSize(data);
			cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
			cell->setPort("\\CLK", RTLIL::State::S0);
			cell->setPort("\\ADDR", addr);
			cell->setPort("\\DATA", data);

			if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
				cell->parameters["\\CLK_ENABLE"] = true;
				cell->setPort("\\CLK", net_map_at(inst->GetClock()));
			}
			continue;
		}

		if (!mode_gates) {
			if (import_netlist_instance_cells(inst, inst_name))
				continue;
			if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
				log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
		} else {
			if (import_netlist_instance_gates(inst, inst_name))
				continue;
		}

		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
			sva_asserts.insert(inst);

		if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
			sva_assumes.insert(inst);

		if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
			sva_covers.insert(inst);

		if (inst->Type() == OPER_SVA_STABLE)
		{
			VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver());

			log_assert(inst->Input1Size() == inst->OutputSize());

			SigSpec sig_d, sig_q, sig_o;
			sig_q = module->addWire(NEW_ID, inst->Input1Size());

			for (int i = int(inst->Input1Size())-1; i >= 0; i--){
				sig_d.append(net_map_at(inst->GetInput1Bit(i)));
				sig_o.append(net_map_at(inst->GetOutputBit(i)));
			}

			if (verific_verbose) {
				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
				log("    XNOR with A=%s, B=%s, Y=%s.\n",
						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
			}

			module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);

			if (!mode_keep)
				continue;
		}

		if (inst->Type() == PRIM_SVA_STABLE)
		{
			VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());

			SigSpec sig_d = net_map_at(inst->GetInput1());
			SigSpec sig_o = net_map_at(inst->GetOutput());
			SigSpec sig_q = module->addWire(NEW_ID);

			if (verific_verbose) {
				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
				log("    XNOR with A=%s, B=%s, Y=%s.\n",
						log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
			}

			module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
			module->addXnor(NEW_ID, sig_d, sig_q, sig_o);

			if (!mode_keep)
				continue;
		}

		if (inst->Type() == PRIM_SVA_PAST)
		{
			VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());

			SigBit sig_d = net_map_at(inst->GetInput1());
			SigBit sig_q = net_map_at(inst->GetOutput());

			if (verific_verbose)
				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));

			past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge));

			if (!mode_keep)
				continue;
		}

		if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
		{
			VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());

			SigBit sig_d = net_map_at(inst->GetInput1());
			SigBit sig_o = net_map_at(inst->GetOutput());
			SigBit sig_q = module->addWire(NEW_ID);

			if (verific_verbose)
				log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
						log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));

			module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
			module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);

			if (!mode_keep)
				continue;
		}

		if (!mode_keep && verific_sva_prims.count(inst->Type())) {
			if (verific_verbose)
				log("    skipping SVA cell in non k-mode\n");
			continue;
		}

		if (inst->IsPrimitive())
		{
			if (inst->Type() == PRIM_HDL_ASSERTION)
				continue;

			if (!mode_keep)
				log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());

			if (!verific_sva_prims.count(inst->Type()))
				log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
		}

		nl_todo.insert(inst->View());

		RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ?
				std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));

		if (inst->IsPrimitive() && mode_keep)
			cell->attributes["\\keep"] = 1;

		dict<IdString, vector<SigBit>> cell_port_conns;

		if (verific_verbose)
			log("    ports in verific db:\n");

		FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
			if (verific_verbose)
				log("      .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
			const char *port_name = pr->GetPort()->Name();
			int port_offset = 0;
			if (pr->GetPort()->Bus()) {
				port_name = pr->GetPort()->Bus()->Name();
				port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
						min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
			}
			IdString port_name_id = RTLIL::escape_id(port_name);
			auto &sigvec = cell_port_conns[port_name_id];
			if (GetSize(sigvec) <= port_offset) {
				SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec));
				for (auto bit : zwires)
					sigvec.push_back(bit);
			}
			sigvec[port_offset] = net_map_at(pr->GetNet());
		}

		if (verific_verbose)
			log("    ports in yosys db:\n");

		for (auto &it : cell_port_conns) {
			if (verific_verbose)
				log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
			cell->setPort(it.first, it.second);
		}
	}

	if (!mode_nosva)
	{
		for (auto inst : sva_asserts)
			import_sva_assert(this, inst);

		for (auto inst : sva_assumes)
			import_sva_assume(this, inst);

		for (auto inst : sva_covers)
			import_sva_cover(this, inst);

		merge_past_ffs(past_ffs);
	}
}

// ==================================================================

VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
{
	log_assert(importer != nullptr);
	log_assert(inst != nullptr);

	// SVA posedge/negedge
	if (inst->Type() == PRIM_SVA_POSEDGE)
	{
		clock_net = inst->GetInput();
		posedge = true;

		Instance *driver = clock_net->Driver();
		if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) {
			clock_net = driver->GetInput();
			posedge = false;
		}

		clock_sig = importer->net_map_at(clock_net);
		return;
	}
}

// ==================================================================

struct VerificExtNets
{
	int portname_cnt = 0;

	// a map from Net to the same Net one level up in the design hierarchy
	std::map<Net*, Net*> net_level_up;

	Net *get_net_level_up(Net *net)
	{
		if (net_level_up.count(net) == 0)
		{
			Netlist *nl = net->Owner();

			// Simply return if Netlist is not unique
			if (nl->NumOfRefs() != 1)
				return net;

			Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
			Netlist *up_nl = up_inst->Owner();

			// create new Port
			string name = stringf("___extnets_%d", portname_cnt++);
			Port *new_port = new Port(name.c_str(), DIR_OUT);
			nl->Add(new_port);
			net->Connect(new_port);

			// create new Net in up Netlist
			Net *new_net = new Net(name.c_str());
			up_nl->Add(new_net);
			up_inst->Connect(new_port, new_net);

			net_level_up[net] = new_net;
		}

		return net_level_up.at(net);
	}

	void run(Netlist *nl)
	{
		MapIter mi, mi2;
		Instance *inst;
		PortRef *pr;

		vector<tuple<Instance*, Port*, Net*>> todo_connect;

		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
			run(inst->View());

		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
		FOREACH_PORTREF_OF_INST(inst, mi2, pr)
		{
			Port *port = pr->GetPort();
			Net *net = pr->GetNet();

			if (!net->IsExternalTo(nl))
				continue;

			if (verific_verbose)
				log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());

			while (net->IsExternalTo(nl))
			{
				Net *newnet = get_net_level_up(net);
				if (newnet == net) break;

				if (verific_verbose)
					log("  external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name());
				net = newnet;
			}

			if (verific_verbose)
				log("  final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : "");
			todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net));
		}

		for (auto it : todo_connect) {
			get<0>(it)->Disconnect(get<1>(it));
			get<0>(it)->Connect(get<1>(it), get<2>(it));
		}
	}
};

YOSYS_NAMESPACE_END
#endif /* YOSYS_ENABLE_VERIFIC */

PRIVATE_NAMESPACE_BEGIN

struct VerificPass : public Pass {
	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
	virtual void help()
	{
		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
		log("\n");
		log("    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
		log("\n");
		log("Load the specified Verilog/SystemVerilog files into Verific.\n");
		log("\n");
		log("\n");
		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
		log("\n");
		log("Load the specified VHDL files into Verific.\n");
		log("\n");
		log("\n");
		log("    verific -vlog-incdir <directory>..\n");
		log("\n");
		log("Add Verilog include directories.\n");
		log("\n");
		log("\n");
		log("    verific -vlog-libdir <directory>..\n");
		log("\n");
		log("Add Verilog library directories. Verific will search in this directories to\n");
		log("find undefined modules.\n");
		log("\n");
		log("\n");
		log("    verific -vlog-define <macro>[=<value>]..\n");
		log("\n");
		log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n");
		log("\n");
		log("\n");
		log("    verific -import [options] <top-module>..\n");
		log("\n");
		log("Elaborate the design for the specified top modules, import to Yosys and\n");
		log("reset the internal state of Verific.\n");
		log("\n");
		log("Import options:\n");
		log("\n");
		log("  -all\n");
		log("    Elaborate all modules, not just the hierarchy below the given top\n");
		log("    modules. With this option the list of modules to import is optional.\n");
		log("\n");
		log("  -gates\n");
		log("    Create a gate-level netlist.\n");
		log("\n");
		log("  -flatten\n");
		log("    Flatten the design in Verific before importing.\n");
		log("\n");
		log("  -extnets\n");
		log("    Resolve references to external nets by adding module ports as needed.\n");
		log("\n");
		log("  -v, -vv\n");
		log("    Verbose log messages. (-vv is even more verbose than -v.)\n");
		log("\n");
		log("The following additional import options are useful for debugging the Verific\n");
		log("bindings (for Yosys and/or Verific developers):\n");
		log("\n");
		log("  -k\n");
		log("    Keep going after an unsupported verific primitive is found. The\n");
		log("    unsupported primitive is added as blockbox module to the design.\n");
		log("    This will also add all SVA related cells to the design parallel to\n");
		log("    the checker logic inferred by it.\n");
		log("\n");
		log("  -nosva\n");
		log("    Ignore SVA properties, do not infer checker logic.\n");
		log("\n");
		log("  -n\n");
		log("    Keep all Verific names on instances and nets. By default only\n");
		log("    user-declared names are preserved.\n");
		log("\n");
		log("  -d <dump_file>\n");
		log("    Dump the Verific netlist as a verilog file.\n");
		log("\n");
		log("Visit http://verific.com/ for more information on Verific.\n");
		log("\n");
	}
#ifdef YOSYS_ENABLE_VERIFIC
	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
	{
		log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");

		Message::SetConsoleOutput(0);
		Message::RegisterCallBackMsg(msg_func);
		RuntimeFlags::SetVar("db_allow_external_nets", 1);
		RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
		veri_file::DefineCmdLineMacro("VERIFIC");
		veri_file::DefineCmdLineMacro("SYNTHESIS");

		verific_verbose = 0;

		const char *release_str = Message::ReleaseString();
		time_t release_time = Message::ReleaseDate();
		char *release_tmstr = ctime(&release_time);

		if (release_str == nullptr)
			release_str = "(no release string)";

		for (char *p = release_tmstr; *p; p++)
			if (*p == '\n') *p = 0;

		log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);

		int argidx = 1;

		if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
			for (argidx++; argidx < GetSize(args); argidx++)
				veri_file::AddIncludeDir(args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
			for (argidx++; argidx < GetSize(args); argidx++)
				veri_file::AddYDir(args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
			for (argidx++; argidx < GetSize(args); argidx++) {
				string name = args[argidx];
				size_t equal = name.find('=');
				if (equal != std::string::npos) {
					string value = name.substr(equal+1);
					name = name.substr(0, equal);
					veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
				} else {
					veri_file::DefineCmdLineMacro(name.c_str());
				}
			}
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-vlog95") {
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95))
					log_cmd_error("Reading `%s' in VERILOG_95 mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-vlog2k") {
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_2K))
					log_cmd_error("Reading `%s' in VERILOG_2K mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-sv2005") {
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2005))
					log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2005 mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-sv2009") {
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG_2009))
					log_cmd_error("Reading `%s' in SYSTEM_VERILOG_2009 mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && (args[argidx] == "-sv2012" || args[argidx] == "-sv")) {
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::SYSTEM_VERILOG))
					log_cmd_error("Reading `%s' in SYSTEM_VERILOG mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_87))
					log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_93))
					log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2K))
					log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
			for (argidx++; argidx < GetSize(args); argidx++)
				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2008))
					log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
			goto check_error;
		}

		if (GetSize(args) > argidx && args[argidx] == "-import")
		{
			std::set<Netlist*> nl_todo, nl_done;
			bool mode_all = false, mode_gates = false, mode_keep = false;
			bool mode_nosva = false, mode_names = false;
			bool flatten = false, extnets = false;
			string dumpfile;

			for (argidx++; argidx < GetSize(args); argidx++) {
				if (args[argidx] == "-all") {
					mode_all = true;
					continue;
				}
				if (args[argidx] == "-gates") {
					mode_gates = true;
					continue;
				}
				if (args[argidx] == "-flatten") {
					flatten = true;
					continue;
				}
				if (args[argidx] == "-extnets") {
					extnets = true;
					continue;
				}
				if (args[argidx] == "-k") {
					mode_keep = true;
					continue;
				}
				if (args[argidx] == "-nosva") {
					mode_nosva = true;
					continue;
				}
				if (args[argidx] == "-n") {
					mode_names = true;
					continue;
				}
				if (args[argidx] == "-v") {
					verific_verbose = 1;
					continue;
				}
				if (args[argidx] == "-vv") {
					verific_verbose = 2;
					continue;
				}
				if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
					dumpfile = args[++argidx];
					continue;
				}
				break;
			}

			if (argidx > GetSize(args) && args[argidx].substr(0, 1) == "-")
				cmd_error(args, argidx, "unknown option");

			if (mode_all)
			{
				log("Running veri_file::ElaborateAll().\n");
				if (!veri_file::ElaborateAll())
					log_cmd_error("Elaboration of Verilog modules failed.\n");

				log("Running vhdl_file::ElaborateAll().\n");
				if (!vhdl_file::ElaborateAll())
					log_cmd_error("Elaboration of VHDL modules failed.\n");

				Library *lib = Netlist::PresentDesign()->Owner()->Owner();

				if (argidx == GetSize(args))
				{
					MapIter iter;
					char *iter_name;
					Verific::Cell *iter_cell;

					FOREACH_MAP_ITEM(lib->GetCells(), iter, &iter_name, &iter_cell) {
						if (*iter_name != '$')
							nl_todo.insert(iter_cell->GetFirstNetlist());
					}
				}
				else
				{
					for (; argidx < GetSize(args); argidx++)
					{
						Verific::Cell *cell = lib->GetCell(args[argidx].c_str());

						if (cell == nullptr)
							log_cmd_error("Module not found: %s\n", args[argidx].c_str());

						nl_todo.insert(cell->GetFirstNetlist());
						cell->GetFirstNetlist()->SetPresentDesign();
					}
				}
			}
			else
			{
				if (argidx == GetSize(args))
					log_cmd_error("No top module specified.\n");

				for (; argidx < GetSize(args); argidx++) {
					if (veri_file::GetModule(args[argidx].c_str())) {
						log("Running veri_file::Elaborate(\"%s\").\n", args[argidx].c_str());
						if (!veri_file::Elaborate(args[argidx].c_str()))
							log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
						nl_todo.insert(Netlist::PresentDesign());
					} else {
						log("Running vhdl_file::Elaborate(\"%s\").\n", args[argidx].c_str());
						if (!vhdl_file::Elaborate(args[argidx].c_str()))
							log_cmd_error("Elaboration of top module `%s' failed.\n", args[argidx].c_str());
						nl_todo.insert(Netlist::PresentDesign());
					}
				}
			}

			if (flatten) {
				for (auto nl : nl_todo)
					nl->Flatten();
			}

			if (extnets) {
				VerificExtNets worker;
				for (auto nl : nl_todo)
					worker.run(nl);
			}

			if (!dumpfile.empty()) {
				VeriWrite veri_writer;
				veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign());
			}

			while (!nl_todo.empty()) {
				Netlist *nl = *nl_todo.begin();
				if (nl_done.count(nl) == 0) {
					VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names);
					importer.import_netlist(design, nl, nl_todo);
				}
				nl_todo.erase(nl);
				nl_done.insert(nl);
			}

			veri_file::Reset();
			vhdl_file::Reset();
			Libset::Reset();
			goto check_error;
		}

		log_cmd_error("Missing or unsupported mode parameter.\n");

	check_error:
		if (!verific_error_msg.empty())
			log_error("%s\n", verific_error_msg.c_str());

	}
#else /* YOSYS_ENABLE_VERIFIC */
	virtual void execute(std::vector<std::string>, RTLIL::Design *) {
		log_cmd_error("This version of Yosys is built without Verific support.\n");
	}
#endif
} VerificPass;

PRIVATE_NAMESPACE_END