/*
* 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/celltypes.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 "hier_tree.h"
#include "VeriModule.h"
#include "VeriWrite.h"
#include "VhdlUnits.h"
#include "VeriLibrary.h"
#ifndef SYMBIOTIC_VERIFIC_API_VERSION
# error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
#endif
#if SYMBIOTIC_VERIFIC_API_VERSION < 1
# error "Please update your version of Symbiotic EDA flavored Verific."
#endif
#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;
bool verific_import_pending;
string verific_error_msg;
int verific_sva_fsm_limit;
vector<string> verific_incdirs, verific_libdirs;
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, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover),
mode_fullinit(mode_fullinit)
{
}
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);
}
bool is_blackbox(Netlist *nl)
{
if (nl->IsBlackBox())
return true;
const char *attr = nl->GetAttValue("blackbox");
if (attr != nullptr && strcmp(attr, "0"))
return true;
return false;
}
RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj)
{
std::string s = stringf("$verific$%s", obj->Name());
if (obj->Linefile())
s += stringf("$%s:%d", Verific::LineFile::GetFileName(obj->Linefile()), Verific::LineFile::GetLineNo(obj->Linefile()));
s += stringf("$%d", autoidx++);
return s;
}
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) {
if (attr->Key()[0] == ' ' || attr->Value() == nullptr)
continue;
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, const pool<Net*, hash_ptr_ops> *any_all_nets)
{
RTLIL::SigSpec sig;
RTLIL::Wire *dummy_wire = NULL;
for (int i = int(inst->OutputSize())-1; i >= 0; i--)
if (inst->GetOutputBit(i) && (!any_all_nets || !any_all_nets->count(inst->GetOutputBit(i)))) {
sig.append(net_map_at(inst->GetOutputBit(i)));
dummy_wire = NULL;
} else {
if (dummy_wire == NULL)
dummy_wire = module->addWire(new_verific_id(inst));
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_verific_id(inst));
module->addAndGate(new_verific_id(inst), 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_verific_id(inst));
module->addOrGate(new_verific_id(inst), 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) {
auto outnet = inst->GetOutput();
if (!any_all_nets.count(outnet))
module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
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_verific_id(inst));
RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
RTLIL::SigSpec tmp1 = module->addWire(new_verific_id(inst));
RTLIL::SigSpec tmp2 = module->addWire(new_verific_id(inst));
RTLIL::SigSpec tmp3 = module->addWire(new_verific_id(inst));
module->addXorGate(new_verific_id(inst), a, b, tmp1);
module->addXorGate(inst_name, tmp1, c, y);
module->addAndGate(new_verific_id(inst), tmp1, c, tmp2);
module->addAndGate(new_verific_id(inst), a, b, tmp3);
module->addOrGate(new_verific_id(inst), tmp2, tmp3, x);
return true;
}
if (inst->Type() == PRIM_DFFRS)
{
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else if (inst->GetSet()->IsGnd())
clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S0);
else if (inst->GetReset()->IsGnd())
clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S1);
else
clocking.addDffsr(inst_name, 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)
{
RTLIL::Cell *cell = nullptr;
if (inst->Type() == PRIM_AND) {
cell = module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_NAND) {
RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
cell = module->addAnd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
import_attributes(cell->attributes, inst);
cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_OR) {
cell = module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_NOR) {
RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
cell = module->addOr(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
import_attributes(cell->attributes, inst);
cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_XOR) {
cell = module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_XNOR) {
cell = module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_INV) {
cell = module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_MUX) {
cell = module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_TRI) {
cell = module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_FADD)
{
RTLIL::SigSpec a_plus_b = module->addWire(new_verific_id(inst), 2);
RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
if (inst->GetCout())
y.append(net_map_at(inst->GetCout()));
cell = module->addAdd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
import_attributes(cell->attributes, inst);
cell = module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_DFFRS)
{
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else if (inst->GetSet()->IsGnd())
cell = clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
else if (inst->GetReset()->IsGnd())
cell = clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
else
cell = clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
import_attributes(cell->attributes, inst);
return true;
}
if (inst->Type() == PRIM_DLATCHRS)
{
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else
cell = 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()));
import_attributes(cell->attributes, inst);