riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Move Verific SVA importer to extra C++ source file 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-02-18 13:52:49 +01:00
parent c4bf34f6ce
commit 5fa2aa2741
4 changed files with 1526 additions and 1435 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
frontends/verific/Makefile.inc
View File

@ -3,6 +3,8 @@ OBJS += frontends/verific/verific.o
ifeq ($(ENABLE_VERIFIC),1) ifeq ($(ENABLE_VERIFIC),1)
OBJS += frontends/verific/verificsva.o
EXTRA_TARGETS += share/verific EXTRA_TARGETS += share/verific
share/verific: share/verific:

472
frontends/verific/verific.cc
View File

@ -29,6 +29,8 @@
# include <dirent.h> # include <dirent.h>
#endif #endif
#include "frontends/verific/verific.h"
USING_YOSYS_NAMESPACE USING_YOSYS_NAMESPACE
#ifdef YOSYS_ENABLE_VERIFIC #ifdef YOSYS_ENABLE_VERIFIC
@ -43,7 +45,6 @@ USING_YOSYS_NAMESPACE
#include "VeriModule.h" #include "VeriModule.h"
#include "VeriWrite.h" #include "VeriWrite.h"
#include "VhdlUnits.h" #include "VhdlUnits.h"
#include "DataBase.h"
#include "Message.h" #include "Message.h"
#ifdef __clang__ #ifdef __clang__
@ -51,14 +52,13 @@ USING_YOSYS_NAMESPACE
#endif #endif
#ifdef VERIFIC_NAMESPACE #ifdef VERIFIC_NAMESPACE
using namespace Verific ; using namespace Verific;
#endif #endif
#endif #endif
PRIVATE_NAMESPACE_BEGIN
#ifdef YOSYS_ENABLE_VERIFIC #ifdef YOSYS_ENABLE_VERIFIC
YOSYS_NAMESPACE_BEGIN
pool<int> verific_sva_prims = { pool<int> verific_sva_prims = {
// Copy&paste from Verific 3.16_484_32_170630 Netlist.h // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
@ -118,48 +118,25 @@ string get_full_netlist_name(Netlist *nl)
return nl->CellBaseName(); return nl->CellBaseName();
} }
struct VerificImporter; // ==================================================================
void import_sva_assert(VerificImporter *importer, Instance *inst);
void import_sva_assume(VerificImporter *importer, Instance *inst);
void import_sva_cover(VerificImporter *importer, Instance *inst);
void svapp_assert(Instance *inst);
void svapp_assume(Instance *inst);
void svapp_cover(Instance *inst);
struct VerificClockEdge { VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
Net *clock_net = nullptr;
SigBit clock_sig = State::Sx;
bool posedge = false;
VerificClockEdge(VerificImporter *importer, Instance *inst);
};
struct VerificImporter
{
RTLIL::Module *module;
Netlist *netlist;
std::map<Net*, RTLIL::SigBit> net_map;
std::map<Net*, Net*> sva_posedge_map;
bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose) mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
{ {
} }
RTLIL::SigBit net_map_at(Net *net) RTLIL::SigBit VerificImporter::net_map_at(Net *net)
{ {
if (net->IsExternalTo(netlist)) if (net->IsExternalTo(netlist))
log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n", 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()); get_full_netlist_name(net->Owner()).c_str(), net->Name(), get_full_netlist_name(netlist).c_str());
return net_map.at(net); return net_map.at(net);
} }
void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
{ {
MapIter mi; MapIter mi;
Att *attr; Att *attr;
@ -169,10 +146,10 @@ struct VerificImporter
// FIXME: Parse numeric attributes // FIXME: Parse numeric attributes
FOREACH_ATTRIBUTE(obj, mi, attr) FOREACH_ATTRIBUTE(obj, mi, attr)
attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value())); attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
} }
RTLIL::SigSpec operatorInput(Instance *inst) RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
{ {
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
for (int i = int(inst->InputSize())-1; i >= 0; i--) for (int i = int(inst->InputSize())-1; i >= 0; i--)
if (inst->GetInputBit(i)) if (inst->GetInputBit(i))
@ -180,10 +157,10 @@ struct VerificImporter
else else
sig.append(RTLIL::State::Sz); sig.append(RTLIL::State::Sz);
return sig; return sig;
} }
RTLIL::SigSpec operatorInput1(Instance *inst) RTLIL::SigSpec VerificImporter::operatorInput1(Instance *inst)
{ {
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
for (int i = int(inst->Input1Size())-1; i >= 0; i--) for (int i = int(inst->Input1Size())-1; i >= 0; i--)
if (inst->GetInput1Bit(i)) if (inst->GetInput1Bit(i))
@ -191,10 +168,10 @@ struct VerificImporter
else else
sig.append(RTLIL::State::Sz); sig.append(RTLIL::State::Sz);
return sig; return sig;
} }
RTLIL::SigSpec operatorInput2(Instance *inst) RTLIL::SigSpec VerificImporter::operatorInput2(Instance *inst)
{ {
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
for (int i = int(inst->Input2Size())-1; i >= 0; i--) for (int i = int(inst->Input2Size())-1; i >= 0; i--)
if (inst->GetInput2Bit(i)) if (inst->GetInput2Bit(i))
@ -202,10 +179,10 @@ struct VerificImporter
else else
sig.append(RTLIL::State::Sz); sig.append(RTLIL::State::Sz);
return sig; return sig;
} }
RTLIL::SigSpec operatorInport(Instance *inst, const char *portname) RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portname)
{ {
PortBus *portbus = inst->View()->GetPortBus(portname); PortBus *portbus = inst->View()->GetPortBus(portname);
if (portbus) { if (portbus) {
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
@ -228,10 +205,10 @@ struct VerificImporter
Net *net = inst->GetNet(port); Net *net = inst->GetNet(port);
return net_map_at(net); return net_map_at(net);
} }
} }
RTLIL::SigSpec operatorOutput(Instance *inst) RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst)
{ {
RTLIL::SigSpec sig; RTLIL::SigSpec sig;
RTLIL::Wire *dummy_wire = NULL; RTLIL::Wire *dummy_wire = NULL;
for (int i = int(inst->OutputSize())-1; i >= 0; i--) for (int i = int(inst->OutputSize())-1; i >= 0; i--)
@ -246,10 +223,10 @@ struct VerificImporter
sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1)); sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
} }
return sig; return sig;
} }
bool import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name) bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
{ {
if (inst->Type() == PRIM_AND) { if (inst->Type() == PRIM_AND) {
module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
@ -337,10 +314,10 @@ struct VerificImporter
} }
return false; return false;
} }
bool import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name) bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
{ {
if (inst->Type() == PRIM_AND) { if (inst->Type() == PRIM_AND) {
module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
return true; return true;
@ -612,10 +589,10 @@ struct VerificImporter
#undef SIGNED #undef SIGNED
return false; return false;
} }
void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol) void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
{ {
bool keep_running = true; bool keep_running = true;
SigMap sigmap; SigMap sigmap;
@ -664,10 +641,10 @@ struct VerificImporter
} }
} }
} }
} }
void merge_past_ffs(pool<RTLIL::Cell*> &candidates) void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
{ {
dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database; dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
for (auto cell : candidates) for (auto cell : candidates)
@ -679,10 +656,10 @@ struct VerificImporter
for (auto it : database) for (auto it : database)
merge_past_ffs_clock(it.second, it.first.first, it.first.second); merge_past_ffs_clock(it.second, it.first.first, it.first.second);
} }
void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo) 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()); std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
netlist = nl; netlist = nl;
@ -1263,8 +1240,9 @@ struct VerificImporter
merge_past_ffs(past_ffs); merge_past_ffs(past_ffs);
} }
} }
};
// ==================================================================
VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
{ {
@ -1290,361 +1268,6 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
// ================================================================== // ==================================================================
struct VerificSvaImporter
{
VerificImporter *importer;
Module *module;
Netlist *netlist;
Instance *root;
SigBit clock = State::Sx;
bool clock_posedge = false;
SigBit disable_iff = State::S0;
bool mode_assert = false;
bool mode_assume = false;
bool mode_cover = false;
bool eventually = false;
bool did_something = false;
Instance *net_to_ast_driver(Net *n)
{
if (n == nullptr)
return nullptr;
if (n->IsMultipleDriven())
return nullptr;
Instance *inst = n->Driver();
if (inst == nullptr)
return nullptr;
if (!verific_sva_prims.count(inst->Type()))
return nullptr;
if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST)
return nullptr;
return inst;
}
Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
// ----------------------------------------------------------
// SVA Preprocessor
Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
Net *rewrite(Instance *inst, Net *default_net = nullptr)
{
if (inst == nullptr)
return default_net;
if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
Net *new_net = rewrite(get_ast_input(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput());
inst->Connect(inst->View()->GetInput(), new_net);
}
return default_net;
}
if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
Net *new_net = rewrite(get_ast_input2(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput2());
inst->Connect(inst->View()->GetInput2(), new_net);
}
return default_net;
}
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
{
if (mode_cover) {
did_something = true;
Net *new_in1 = rewrite_input1(inst);
Net *new_in2 = rewrite_input2(inst);
return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
}
return default_net;
}
if (inst->Type() == PRIM_SVA_NOT)
{
if (mode_assert || mode_assume) {
did_something = true;
Net *new_in = rewrite_input(inst);
Net *net_zero = netlist->Gnd(inst->Linefile());
return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
}
return default_net;
}
return default_net;
}
void rewrite()
{
netlist = root->Owner();
do {
did_something = false;
rewrite(root);
} while (did_something);
}
// ----------------------------------------------------------
// SVA Inporter
struct sequence_t {
int length = 0;
SigBit sig_a = State::S1;
SigBit sig_en = State::S1;
};
void sequence_cond(sequence_t &seq, SigBit cond)
{
seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
}
void sequence_ff(sequence_t &seq)
{
if (disable_iff != State::S0)
seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
Wire *sig_a_q = module->addWire(NEW_ID);
sig_a_q->attributes["\\init"] = Const(0, 1);
Wire *sig_en_q = module->addWire(NEW_ID);
sig_en_q->attributes["\\init"] = Const(0, 1);
module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge);
module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge);
seq.length++;
seq.sig_a = sig_a_q;
seq.sig_en = sig_en_q;
}
void parse_sequence(sequence_t &seq, Net *n)
{
Instance *inst = net_to_ast_driver(n);
// Regular expression
if (inst == nullptr) {
sequence_cond(seq, importer->net_map_at(n));
return;
}
// SVA Primitives
if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION)
{
parse_sequence(seq, inst->GetInput1());
seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
parse_sequence(seq, inst->GetInput2());
return;
}
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
{
parse_sequence(seq, inst->GetInput1());
seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
sequence_ff(seq);
parse_sequence(seq, inst->GetInput2());
return;
}
if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
{
int sva_low = atoi(inst->GetAttValue("sva:low"));
int sva_high = atoi(inst->GetAttValue("sva:low"));
if (sva_low != sva_high)
log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n");
parse_sequence(seq, inst->GetInput1());
for (int i = 0; i < sva_low; i++)
sequence_ff(seq);
parse_sequence(seq, inst->GetInput2());
return;
}
if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
{
int sva_low = atoi(inst->GetAttValue("sva:low"));
int sva_high = atoi(inst->GetAttValue("sva:low"));
if (sva_low != sva_high)
log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n");
parse_sequence(seq, inst->GetInput());
for (int i = 1; i < sva_low; i++) {
sequence_ff(seq);
parse_sequence(seq, inst->GetInput());
}
return;
}
// Handle unsupported primitives
if (!importer->mode_keep)
log_error("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
log_warning("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
}
void import()
{
module = importer->module;
netlist = root->Owner();
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
// parse SVA property clock event
Instance *at_node = get_ast_input(root);
// asynchronous immediate assertion/assumption/cover
if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
{
SigSpec sig_a = importer->net_map_at(root->GetInput());
RTLIL::Cell *c = nullptr;
if (eventually) {
if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
} else {
if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
}
importer->import_attributes(c->attributes, root);
return;
}
log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
clock = clock_edge.clock_sig;
clock_posedge = clock_edge.posedge;
// parse disable_iff expression
Net *sequence_net = at_node->GetInput2();
while (1)
{
Instance *sequence_node = net_to_ast_driver(sequence_net);
if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
eventually = true;
sequence_net = sequence_node->GetInput();
continue;
}
if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
disable_iff = importer->net_map_at(sequence_node->GetInput1());
sequence_net = sequence_node->GetInput2();
continue;
}
break;
}
// parse SVA sequence into trigger signal
sequence_t seq;
parse_sequence(seq, sequence_net);
sequence_ff(seq);
// generate assert/assume/cover cell
RTLIL::Cell *c = nullptr;
if (eventually) {
if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
} else {
if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en);
if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
}
importer->import_attributes(c->attributes, root);
}
};
void svapp_assert(Instance *inst)
{
VerificSvaImporter worker;
worker.root = inst;
worker.mode_assert = true;
worker.rewrite();
}
void svapp_assume(Instance *inst)
{
VerificSvaImporter worker;
worker.root = inst;
worker.mode_assume = true;
worker.rewrite();
}
void svapp_cover(Instance *inst)
{
VerificSvaImporter worker;
worker.root = inst;
worker.mode_cover = true;
worker.rewrite();
}
void import_sva_assert(VerificImporter *importer, Instance *inst)
{
VerificSvaImporter worker;
worker.importer = importer;
worker.root = inst;
worker.mode_assert = true;
worker.import();
}
void import_sva_assume(VerificImporter *importer, Instance *inst)
{
VerificSvaImporter worker;
worker.importer = importer;
worker.root = inst;
worker.mode_assume = true;
worker.import();
}
void import_sva_cover(VerificImporter *importer, Instance *inst)
{
VerificSvaImporter worker;
worker.importer = importer;
worker.root = inst;
worker.mode_cover = true;
worker.import();
}
// ==================================================================
struct VerificExtNets struct VerificExtNets
{ {
int portname_cnt = 0; int portname_cnt = 0;
@ -1728,8 +1351,11 @@ struct VerificExtNets
} }
}; };
YOSYS_NAMESPACE_END
#endif /* YOSYS_ENABLE_VERIFIC */ #endif /* YOSYS_ENABLE_VERIFIC */
PRIVATE_NAMESPACE_BEGIN
struct VerificPass : public Pass { struct VerificPass : public Pass {
VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { } VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
virtual void help() virtual void help()

79
frontends/verific/verific.h Normal file
View File

@ -0,0 +1,79 @@
/*
* 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.
*
*/
#ifdef YOSYS_ENABLE_VERIFIC
#include "DataBase.h"
YOSYS_NAMESPACE_BEGIN
extern pool<int> verific_sva_prims;
struct VerificImporter;
struct VerificClockEdge {
Verific::Net *clock_net = nullptr;
SigBit clock_sig = State::Sx;
bool posedge = false;
VerificClockEdge(VerificImporter *importer, Verific::Instance *inst);
};
struct VerificImporter
{
RTLIL::Module *module;
Verific::Netlist *netlist;
std::map<Verific::Net*, RTLIL::SigBit> net_map;
std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose);
RTLIL::SigBit net_map_at(Verific::Net *net);
void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, Verific::DesignObj *obj);
RTLIL::SigSpec operatorInput(Verific::Instance *inst);
RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
RTLIL::SigSpec operatorInput2(Verific::Instance *inst);
RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname);
RTLIL::SigSpec operatorOutput(Verific::Instance *inst);
bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name);
bool import_netlist_instance_cells(Verific::Instance *inst, RTLIL::IdString inst_name);
void merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol);
void merge_past_ffs(pool<RTLIL::Cell*> &candidates);
void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set<Verific::Netlist*> &nl_todo);
};
void import_sva_assert(VerificImporter *importer, Verific::Instance *inst);
void import_sva_assume(VerificImporter *importer, Verific::Instance *inst);
void import_sva_cover(VerificImporter *importer, Verific::Instance *inst);
void svapp_assert(Verific::Instance *inst);
void svapp_assume(Verific::Instance *inst);
void svapp_cover(Verific::Instance *inst);
YOSYS_NAMESPACE_END
#endif

384
frontends/verific/verificsva.cc Normal file
View File

@ -0,0 +1,384 @@
/*
* 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 "frontends/verific/verific.h"
USING_YOSYS_NAMESPACE
#ifdef VERIFIC_NAMESPACE
using namespace Verific;
#endif
YOSYS_NAMESPACE_BEGIN
struct VerificSvaImporter
{
VerificImporter *importer = nullptr;
Module *module = nullptr;
Netlist *netlist = nullptr;
Instance *root = nullptr;
SigBit clock = State::Sx;
bool clock_posedge = false;
SigBit disable_iff = State::S0;
bool mode_assert = false;
bool mode_assume = false;
bool mode_cover = false;
bool eventually = false;
bool did_something = false;
Instance *net_to_ast_driver(Net *n)
{
if (n == nullptr)
return nullptr;
if (n->IsMultipleDriven())
return nullptr;
Instance *inst = n->Driver();
if (inst == nullptr)
return nullptr;
if (!verific_sva_prims.count(inst->Type()))
return nullptr;
if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST)
return nullptr;
return inst;
}
Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
// ----------------------------------------------------------
// SVA Preprocessor
Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
Net *rewrite(Instance *inst, Net *default_net = nullptr)
{
if (inst == nullptr)
return default_net;
if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME ||
inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
Net *new_net = rewrite(get_ast_input(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput());
inst->Connect(inst->View()->GetInput(), new_net);
}
return default_net;
}
if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) {
Net *new_net = rewrite(get_ast_input2(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput2());
inst->Connect(inst->View()->GetInput2(), new_net);
}
return default_net;
}
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
{
if (mode_cover) {
did_something = true;
Net *new_in1 = rewrite_input1(inst);
Net *new_in2 = rewrite_input2(inst);
return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
}
return default_net;
}
if (inst->Type() == PRIM_SVA_NOT)
{
if (mode_assert || mode_assume) {
did_something = true;
Net *new_in = rewrite_input(inst);
Net *net_zero = netlist->Gnd(inst->Linefile());
return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
}
return default_net;
}
return default_net;
}
void rewrite()
{
netlist = root->Owner();
do {
did_something = false;
rewrite(root);
} while (did_something);
}
// ----------------------------------------------------------
// SVA Importer
struct sequence_t {
int length = 0;
SigBit sig_a = State::S1;
SigBit sig_en = State::S1;
};
void sequence_cond(sequence_t &seq, SigBit cond)
{
seq.sig_a = module->And(NEW_ID, seq.sig_a, cond);
}
void sequence_ff(sequence_t &seq)
{
if (disable_iff != State::S0)
seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
Wire *sig_a_q = module->addWire(NEW_ID);
sig_a_q->attributes["\\init"] = Const(0, 1);
Wire *sig_en_q = module->addWire(NEW_ID);
sig_en_q->attributes["\\init"] = Const(0, 1);
module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge);
module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge);
seq.length++;
seq.sig_a = sig_a_q;
seq.sig_en = sig_en_q;
}
void parse_sequence(sequence_t &seq, Net *n)
{
Instance *inst = net_to_ast_driver(n);
// Regular expression
if (inst == nullptr) {
sequence_cond(seq, importer->net_map_at(n));
return;
}
// SVA Primitives
if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION)
{
parse_sequence(seq, inst->GetInput1());
seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
parse_sequence(seq, inst->GetInput2());
return;
}
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
{
parse_sequence(seq, inst->GetInput1());
seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
sequence_ff(seq);
parse_sequence(seq, inst->GetInput2());
return;
}
if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
{
int sva_low = atoi(inst->GetAttValue("sva:low"));
int sva_high = atoi(inst->GetAttValue("sva:low"));
if (sva_low != sva_high)
log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n");
parse_sequence(seq, inst->GetInput1());
for (int i = 0; i < sva_low; i++)
sequence_ff(seq);
parse_sequence(seq, inst->GetInput2());
return;
}
if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
{
int sva_low = atoi(inst->GetAttValue("sva:low"));
int sva_high = atoi(inst->GetAttValue("sva:low"));
if (sva_low != sva_high)
log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n");
parse_sequence(seq, inst->GetInput());
for (int i = 1; i < sva_low; i++) {
sequence_ff(seq);
parse_sequence(seq, inst->GetInput());
}
return;
}
// Handle unsupported primitives
if (!importer->mode_keep)
log_error("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
log_warning("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name());
}
void import()
{
module = importer->module;
netlist = root->Owner();
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
// parse SVA property clock event
Instance *at_node = get_ast_input(root);
// asynchronous immediate assertion/assumption/cover
if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT ||
root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME))
{
SigSpec sig_a = importer->net_map_at(root->GetInput());
RTLIL::Cell *c = nullptr;
if (eventually) {
if (mode_assert) c = module->addLive(root_name, sig_a, State::S1);
if (mode_assume) c = module->addFair(root_name, sig_a, State::S1);
} else {
if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1);
if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1);
if (mode_cover) c = module->addCover(root_name, sig_a, State::S1);
}
importer->import_attributes(c->attributes, root);
return;
}
log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
clock = clock_edge.clock_sig;
clock_posedge = clock_edge.posedge;
// parse disable_iff expression
Net *sequence_net = at_node->GetInput2();
while (1)
{
Instance *sequence_node = net_to_ast_driver(sequence_net);
if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
eventually = true;
sequence_net = sequence_node->GetInput();
continue;
}
if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
disable_iff = importer->net_map_at(sequence_node->GetInput1());
sequence_net = sequence_node->GetInput2();
continue;
}
break;
}
// parse SVA sequence into trigger signal
sequence_t seq;
parse_sequence(seq, sequence_net);
sequence_ff(seq);
// generate assert/assume/cover cell
RTLIL::Cell *c = nullptr;
if (eventually) {
if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en);
if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en);
} else {
if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en);
if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en);
if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en);
}
importer->import_attributes(c->attributes, root);
}
};
void svapp_assert(Instance *inst)
{
VerificSvaImporter worker;
worker.root = inst;
worker.mode_assert = true;
worker.rewrite();
}
void svapp_assume(Instance *inst)
{
VerificSvaImporter worker;
worker.root = inst;
worker.mode_assume = true;
worker.rewrite();
}
void svapp_cover(Instance *inst)
{
VerificSvaImporter worker;
worker.root = inst;
worker.mode_cover = true;
worker.rewrite();
}
void import_sva_assert(VerificImporter *importer, Instance *inst)
{
VerificSvaImporter worker;
worker.importer = importer;
worker.root = inst;
worker.mode_assert = true;
worker.import();
}
void import_sva_assume(VerificImporter *importer, Instance *inst)
{
VerificSvaImporter worker;
worker.importer = importer;
worker.root = inst;
worker.mode_assume = true;
worker.import();
}
void import_sva_cover(VerificImporter *importer, Instance *inst)
{
VerificSvaImporter worker;
worker.importer = importer;
worker.root = inst;
worker.mode_cover = true;
worker.import();
}
YOSYS_NAMESPACE_END