mirror of
https://github.com/YosysHQ/yosys
synced 2025-08-27 13:39:49 +00:00
Continue refactoring of Verific SVA importer code
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf
parent
25e33d7ab8
commit
15902d495f
3 changed files with 172 additions and 671 deletions
|
|
@ -72,11 +72,23 @@ using namespace Verific;
|
|||
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
struct SvaFsmNode
|
||||
// Non-deterministic FSM
|
||||
struct SvaNFsmNode
|
||||
{
|
||||
// Edge: Activate the target node if ctrl signal is true, consumes clock cycle
|
||||
// Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle
|
||||
vector<pair<int, SigBit>> edges, links;
|
||||
};
|
||||
|
||||
// Non-deterministic FSM after resolving links
|
||||
struct SvaUFsmNode
|
||||
{
|
||||
// Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle
|
||||
// Accept: This node functions as an accept node if all bits in ctrl signal are true
|
||||
vector<pair<int, SigSpec>> edges;
|
||||
vector<SigSpec> accept;
|
||||
};
|
||||
|
||||
struct SvaFsm
|
||||
{
|
||||
Module *module;
|
||||
|
|
@ -91,8 +103,11 @@ struct SvaFsm
|
|||
vector<SigBit> disable_stack;
|
||||
vector<SigBit> throughout_stack;
|
||||
|
||||
int startNode, acceptNode, rejectNode;
|
||||
vector<SvaFsmNode> nodes;
|
||||
int startNode, acceptNode;
|
||||
vector<SvaNFsmNode> nodes;
|
||||
|
||||
// ----------------------------------------------------
|
||||
// API for creating FSM
|
||||
|
||||
SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1)
|
||||
{
|
||||
|
|
@ -104,7 +119,6 @@ struct SvaFsm
|
|||
|
||||
startNode = createNode();
|
||||
acceptNode = createNode();
|
||||
rejectNode = createNode();
|
||||
}
|
||||
|
||||
void pushDisable(SigBit sig)
|
||||
|
|
@ -149,32 +163,12 @@ struct SvaFsm
|
|||
throughout_stack.pop_back();
|
||||
}
|
||||
|
||||
SigBit getAccept()
|
||||
{
|
||||
if (accept_sig != State::Sz)
|
||||
return accept_sig;
|
||||
|
||||
log_assert(!materialized);
|
||||
accept_sig = module->addWire(NEW_ID);
|
||||
return accept_sig;
|
||||
}
|
||||
|
||||
SigBit getReject()
|
||||
{
|
||||
if (reject_sig != State::Sz)
|
||||
return reject_sig;
|
||||
|
||||
log_assert(!materialized);
|
||||
reject_sig = module->addWire(NEW_ID);
|
||||
return reject_sig;
|
||||
}
|
||||
|
||||
int createNode()
|
||||
{
|
||||
log_assert(!materialized);
|
||||
|
||||
int idx = GetSize(nodes);
|
||||
nodes.push_back(SvaFsmNode());
|
||||
nodes.push_back(SvaNFsmNode());
|
||||
return idx;
|
||||
}
|
||||
|
||||
|
|
@ -217,15 +211,19 @@ struct SvaFsm
|
|||
make_link_order(order, it.first, order[node]+1);
|
||||
}
|
||||
|
||||
void materialize_ndfsm()
|
||||
// ----------------------------------------------------
|
||||
// API for generating NFSM circuit to acquire accept signal
|
||||
|
||||
SigBit getAccept()
|
||||
{
|
||||
log_assert(!materialized);
|
||||
materialized = true;
|
||||
|
||||
vector<SigBit> next_state_sig(GetSize(nodes));
|
||||
vector<Wire*> state_wire(GetSize(nodes));
|
||||
vector<SigBit> state_sig(GetSize(nodes));
|
||||
vector<SigBit> next_state_sig(GetSize(nodes));
|
||||
|
||||
// Create state FFs
|
||||
// Create state signals
|
||||
|
||||
{
|
||||
SigBit not_disable = State::S1;
|
||||
|
|
@ -235,14 +233,10 @@ struct SvaFsm
|
|||
|
||||
for (int i = 0; i < GetSize(nodes); i++)
|
||||
{
|
||||
next_state_sig[i] = module->addWire(NEW_ID);
|
||||
|
||||
Wire *w = module->addWire(NEW_ID);
|
||||
w->attributes["\\init"] = Const(0, 1);
|
||||
state_wire[i] = w;
|
||||
state_sig[i] = w;
|
||||
|
||||
module->addDff(NEW_ID, clock, next_state_sig[i], state_sig[i], clockpol);
|
||||
|
||||
if (i == startNode)
|
||||
state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig);
|
||||
|
||||
|
|
@ -295,86 +289,92 @@ struct SvaFsm
|
|||
|
||||
for (int i = 0; i < GetSize(nodes); i++) {
|
||||
if (GetSize(activate_sig[i]) == 0)
|
||||
activate_bit[i] = State::S0;
|
||||
next_state_sig[i] = State::S0;
|
||||
else if (GetSize(activate_sig[i]) == 1)
|
||||
activate_bit[i] = activate_sig[i];
|
||||
next_state_sig[i] = activate_sig[i];
|
||||
else
|
||||
activate_bit[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
|
||||
}
|
||||
|
||||
if (activate_bit[rejectNode] != State::S0)
|
||||
{
|
||||
SigBit not_rej = module->Not(NEW_ID, next_state_sig[rejectNode]);
|
||||
for (int i = 0; i < GetSize(nodes); i++)
|
||||
if (i != rejectNode && activate_bit[i] != State::S0)
|
||||
activate_bit[i] = module->And(NEW_ID, activate_bit[i], not_rej);
|
||||
activate_bit[rejectNode] = State::S0;
|
||||
}
|
||||
|
||||
for (int i = 0; i < GetSize(nodes); i++) {
|
||||
module->connect(next_state_sig[i], activate_bit[i]);
|
||||
next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
|
||||
}
|
||||
}
|
||||
|
||||
// Construct output signals
|
||||
// Create state FFs
|
||||
|
||||
if (accept_sig != State::Sz) {
|
||||
module->connect(accept_sig, state_sig[acceptNode]);
|
||||
}
|
||||
|
||||
if (reject_sig != State::Sz)
|
||||
for (int i = 0; i < GetSize(nodes); i++)
|
||||
{
|
||||
SigBit fsm_active = module->ReduceOr(NEW_ID, state_sig);
|
||||
SigBit fsm_next_active = module->ReduceOr(NEW_ID, next_state_sig);
|
||||
module->addEq(NEW_ID, {state_sig[acceptNode], fsm_next_active, fsm_active}, SigSpec(1, 3), reject_sig);
|
||||
if (next_state_sig[i] != State::S0) {
|
||||
state_wire[i]->attributes["\\init"] = Const(0, 1);
|
||||
module->addDff(NEW_ID, clock, next_state_sig[i], state_wire[i], clockpol);
|
||||
} else {
|
||||
module->connect(state_wire[i], State::S0);
|
||||
}
|
||||
}
|
||||
|
||||
return state_sig[acceptNode];
|
||||
}
|
||||
|
||||
void materialize_dfsm()
|
||||
// ----------------------------------------------------
|
||||
// API for generating quantifier-based NFSM circuit to acquire reject signal
|
||||
|
||||
SigBit getAnyAllRejectWorker(bool allMode)
|
||||
{
|
||||
// FIXME
|
||||
log_abort();
|
||||
}
|
||||
|
||||
bool is_linear()
|
||||
SigBit getAnyReject()
|
||||
{
|
||||
for (int i = 0; i < GetSize(nodes); i++)
|
||||
if (GetSize(nodes[i].edges) + GetSize(nodes[i].links) > 1)
|
||||
return false;
|
||||
return true;
|
||||
return getAnyAllRejectWorker(false);
|
||||
}
|
||||
|
||||
SigBit getAllReject()
|
||||
{
|
||||
return getAnyAllRejectWorker(true);
|
||||
}
|
||||
|
||||
// ----------------------------------------------------
|
||||
// API for generating DFSM circuit to acquire reject signal
|
||||
|
||||
SigBit getReject()
|
||||
{
|
||||
// FIXME
|
||||
log("-----------------\n");
|
||||
dump();
|
||||
log_abort();
|
||||
}
|
||||
|
||||
// ----------------------------------------------------
|
||||
// State dump for verbose log messages
|
||||
|
||||
void dump()
|
||||
{
|
||||
log("-----------\n");
|
||||
for (int i = 0; i < GetSize(nodes); i++)
|
||||
if (!nodes.empty())
|
||||
{
|
||||
log("node %d:\n", i);
|
||||
log(" non-deterministic encoding:\n");
|
||||
for (int i = 0; i < GetSize(nodes); i++)
|
||||
{
|
||||
log(" node %d:\n", i);
|
||||
|
||||
if (i == startNode)
|
||||
log(" startNode\n");
|
||||
if (i == startNode)
|
||||
log(" startNode\n");
|
||||
|
||||
if (i == rejectNode)
|
||||
log(" rejectNode\n");
|
||||
if (i == acceptNode)
|
||||
log(" acceptNode\n");
|
||||
|
||||
if (i == acceptNode)
|
||||
log(" acceptNode\n");
|
||||
for (auto &it : nodes[i].edges) {
|
||||
if (it.second != State::S1)
|
||||
log(" egde %s -> %d\n", log_signal(it.second), it.first);
|
||||
else
|
||||
log(" egde -> %d\n", it.first);
|
||||
}
|
||||
|
||||
for (auto &it : nodes[i].edges) {
|
||||
if (it.second != State::S1)
|
||||
log(" egde %s -> %d\n", log_signal(it.second), it.first);
|
||||
else
|
||||
log(" egde -> %d\n", it.first);
|
||||
}
|
||||
|
||||
for (auto &it : nodes[i].links) {
|
||||
if (it.second != State::S1)
|
||||
log(" link %s -> %d\n", log_signal(it.second), it.first);
|
||||
else
|
||||
log(" link -> %d\n", it.first);
|
||||
for (auto &it : nodes[i].links) {
|
||||
if (it.second != State::S1)
|
||||
log(" link %s -> %d\n", log_signal(it.second), it.first);
|
||||
else
|
||||
log(" link -> %d\n", it.first);
|
||||
}
|
||||
}
|
||||
}
|
||||
log("-----------\n");
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -414,7 +414,7 @@ struct VerificSvaImporter
|
|||
Instance *root = nullptr;
|
||||
|
||||
SigBit clock = State::Sx;
|
||||
bool clock_posedge = false;
|
||||
bool clockpol = false;
|
||||
|
||||
SigBit disable_iff = State::S0;
|
||||
|
||||
|
|
@ -453,124 +453,6 @@ struct VerificSvaImporter
|
|||
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 AST Types
|
||||
|
||||
struct svatype_t
|
||||
{
|
||||
bool flag_linear = true;
|
||||
};
|
||||
|
||||
std::map<Instance*, svatype_t> svatype_cache;
|
||||
|
||||
void svatype_visit_child(svatype_t &entry, Instance *inst)
|
||||
{
|
||||
if (inst == nullptr)
|
||||
return;
|
||||
|
||||
const svatype_t &child_entry = svatype(inst);
|
||||
entry.flag_linear &= child_entry.flag_linear;
|
||||
}
|
||||
|
||||
const svatype_t &svatype(Instance *inst)
|
||||
{
|
||||
if (svatype_cache.count(inst) != 0)
|
||||
return svatype_cache.at(inst);
|
||||
|
||||
svatype_t &entry = svatype_cache[inst];
|
||||
|
||||
if (inst == nullptr)
|
||||
return entry;
|
||||
|
||||
if (inst->Type() == PRIM_SVA_SEQ_CONCAT || inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
|
||||
{
|
||||
const char *sva_low_s = inst->GetAttValue("sva:low");
|
||||
const char *sva_high_s = inst->GetAttValue("sva:high");
|
||||
|
||||
int sva_low = atoi(sva_low_s);
|
||||
int sva_high = atoi(sva_high_s);
|
||||
bool sva_inf = !strcmp(sva_high_s, "$");
|
||||
|
||||
if (sva_inf || sva_low != sva_high)
|
||||
entry.flag_linear = false;
|
||||
}
|
||||
|
||||
svatype_visit_child(entry, get_ast_input(inst));
|
||||
svatype_visit_child(entry, get_ast_input1(inst));
|
||||
svatype_visit_child(entry, get_ast_input2(inst));
|
||||
svatype_visit_child(entry, get_ast_input3(inst));
|
||||
svatype_visit_child(entry, get_ast_control(inst));
|
||||
|
||||
return entry;
|
||||
}
|
||||
|
||||
// ----------------------------------------------------------
|
||||
// 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
|
||||
|
||||
|
|
@ -687,6 +569,10 @@ struct VerificSvaImporter
|
|||
module = importer->module;
|
||||
netlist = root->Owner();
|
||||
|
||||
if (verific_verbose)
|
||||
log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
|
||||
LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
|
||||
|
||||
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
|
||||
|
||||
// parse SVA property clock event
|
||||
|
|
@ -717,25 +603,25 @@ struct VerificSvaImporter
|
|||
|
||||
VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
|
||||
clock = clock_edge.clock_sig;
|
||||
clock_posedge = clock_edge.posedge;
|
||||
clockpol = clock_edge.posedge;
|
||||
|
||||
// parse disable_iff expression
|
||||
|
||||
Net *sequence_net = at_node->GetInput2();
|
||||
Net *net = at_node->GetInput2();
|
||||
|
||||
while (1)
|
||||
{
|
||||
Instance *sequence_node = net_to_ast_driver(sequence_net);
|
||||
Instance *sequence_node = net_to_ast_driver(net);
|
||||
|
||||
if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
|
||||
eventually = true;
|
||||
sequence_net = sequence_node->GetInput();
|
||||
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();
|
||||
net = sequence_node->GetInput2();
|
||||
continue;
|
||||
}
|
||||
|
||||
|
|
@ -745,11 +631,11 @@ struct VerificSvaImporter
|
|||
// parse SVA sequence into trigger signal
|
||||
|
||||
SigBit prop_okay;
|
||||
Instance *inst = net_to_ast_driver(sequence_net);
|
||||
Instance *inst = net_to_ast_driver(net);
|
||||
|
||||
if (inst == nullptr)
|
||||
{
|
||||
prop_okay = importer->net_map_at(sequence_net);
|
||||
prop_okay = importer->net_map_at(net);
|
||||
}
|
||||
else
|
||||
if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
|
||||
|
|
@ -759,7 +645,7 @@ struct VerificSvaImporter
|
|||
Net *consequent_net = inst->GetInput2();
|
||||
int node;
|
||||
|
||||
SvaFsm antecedent_fsm(module, clock, clock_posedge, disable_iff);
|
||||
SvaFsm antecedent_fsm(module, clock, clockpol, disable_iff);
|
||||
node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, antecedent_net);
|
||||
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
|
||||
int next_node = antecedent_fsm.createNode();
|
||||
|
|
@ -768,21 +654,50 @@ struct VerificSvaImporter
|
|||
}
|
||||
antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
|
||||
|
||||
SigBit antecedent_accept = antecedent_fsm.getAccept();
|
||||
antecedent_fsm.materialize_ndfsm();
|
||||
antecedent_fsm.dump();
|
||||
SigBit antecedent_match = antecedent_fsm.getAccept();
|
||||
|
||||
SvaFsm consequent_fsm(module, clock, clock_posedge, disable_iff, antecedent_accept);
|
||||
if (verific_verbose) {
|
||||
log(" Antecedent FSM:\n");
|
||||
antecedent_fsm.dump();
|
||||
}
|
||||
|
||||
bool consequent_not = false;
|
||||
Instance *consequent_inst = net_to_ast_driver(consequent_net);
|
||||
|
||||
if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
|
||||
consequent_not = true;
|
||||
consequent_net = consequent_inst->GetInput();
|
||||
}
|
||||
|
||||
SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match);
|
||||
node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net);
|
||||
consequent_fsm.createLink(node, consequent_fsm.acceptNode);
|
||||
|
||||
SigBit consequent_reject = consequent_fsm.getReject();
|
||||
prop_okay = module->Not(NEW_ID, consequent_reject);
|
||||
if (mode_cover) {
|
||||
prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept();
|
||||
} else {
|
||||
SigBit consequent_match = consequent_not ? consequent_fsm.getAccept() : consequent_fsm.getReject();
|
||||
prop_okay = module->Not(NEW_ID, consequent_match);
|
||||
}
|
||||
|
||||
if (consequent_fsm.is_linear())
|
||||
consequent_fsm.materialize_ndfsm();
|
||||
else
|
||||
log_error("Currently only linear sequences are allowed as impliciation consequent.\n");
|
||||
if (verific_verbose) {
|
||||
log(" Consequent FSM:\n");
|
||||
antecedent_fsm.dump();
|
||||
}
|
||||
}
|
||||
else
|
||||
if (inst->Type() == PRIM_SVA_NOT || mode_cover)
|
||||
{
|
||||
SvaFsm fsm(module, clock, clockpol, disable_iff);
|
||||
int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput());
|
||||
fsm.createLink(node, fsm.acceptNode);
|
||||
SigBit accept = fsm.getAccept();
|
||||
prop_okay = module->Not(NEW_ID, accept);
|
||||
|
||||
if (verific_verbose) {
|
||||
log(" Sequence FSM:\n");
|
||||
fsm.dump();
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -798,7 +713,7 @@ struct VerificSvaImporter
|
|||
|
||||
Wire *prop_okay_q = module->addWire(NEW_ID);
|
||||
prop_okay_q->attributes["\\init"] = Const(mode_cover ? 0 : 1, 1);
|
||||
module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clock_posedge);
|
||||
module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clockpol);
|
||||
|
||||
// generate assert/assume/cover cell
|
||||
|
||||
|
|
@ -816,387 +731,8 @@ struct VerificSvaImporter
|
|||
|
||||
importer->import_attributes(c->attributes, root);
|
||||
}
|
||||
|
||||
#if 0
|
||||
// ----------------------------------------------------------
|
||||
// Old SVA Importer
|
||||
|
||||
vector<SigBit> sva_until_list_inclusive;
|
||||
vector<SigBit> sva_until_list_exclusive;
|
||||
vector<vector<SigBit>*> sva_sequence_alive_list;
|
||||
|
||||
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);
|
||||
|
||||
for (auto &expr : sva_until_list_exclusive)
|
||||
seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
|
||||
|
||||
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);
|
||||
|
||||
for (auto list : sva_sequence_alive_list)
|
||||
list->push_back(module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en));
|
||||
|
||||
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);
|
||||
|
||||
if (seq.length >= 0)
|
||||
seq.length++;
|
||||
|
||||
seq.sig_a = sig_a_q;
|
||||
seq.sig_en = sig_en_q;
|
||||
|
||||
for (auto &expr : sva_until_list_inclusive)
|
||||
seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
|
||||
}
|
||||
|
||||
void combine_seq(sequence_t &seq, const sequence_t &other_seq)
|
||||
{
|
||||
if (seq.length != other_seq.length)
|
||||
seq.length = -1;
|
||||
|
||||
SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en);
|
||||
SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_seq.sig_a, other_seq.sig_en);
|
||||
|
||||
seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a);
|
||||
seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_seq.sig_en);
|
||||
}
|
||||
|
||||
void combine_seq(sequence_t &seq, SigBit other_a, SigBit other_en)
|
||||
{
|
||||
SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en);
|
||||
SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_a, other_en);
|
||||
|
||||
seq.length = -1;
|
||||
seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a);
|
||||
seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_en);
|
||||
}
|
||||
|
||||
SigBit make_temporal_one_hot(SigBit enable = State::S1, SigBit *latched = nullptr)
|
||||
{
|
||||
Wire *state = module->addWire(NEW_ID);
|
||||
state->attributes["\\init"] = State::S0;
|
||||
|
||||
SigBit any = module->Anyseq(NEW_ID);
|
||||
if (enable != State::S1)
|
||||
any = module->LogicAnd(NEW_ID, any, enable);
|
||||
|
||||
SigBit next_state = module->LogicOr(NEW_ID, state, any);
|
||||
module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
|
||||
|
||||
if (latched != nullptr)
|
||||
*latched = state;
|
||||
|
||||
SigBit not_state = module->LogicNot(NEW_ID, state);
|
||||
return module->LogicAnd(NEW_ID, next_state, not_state);
|
||||
}
|
||||
|
||||
SigBit make_permanent_latch(SigBit enable, bool async = false)
|
||||
{
|
||||
Wire *state = module->addWire(NEW_ID);
|
||||
state->attributes["\\init"] = State::S0;
|
||||
|
||||
SigBit next_state = module->LogicOr(NEW_ID, state, enable);
|
||||
module->addDff(NEW_ID, clock, next_state, state, clock_posedge);
|
||||
|
||||
return async ? next_state : state;
|
||||
}
|
||||
|
||||
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 ||
|
||||
inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
|
||||
{
|
||||
Instance *consequent = get_ast_input2(inst);
|
||||
bool linear_consequent = svatype(consequent).flag_linear;
|
||||
|
||||
parse_sequence(seq, inst->GetInput1());
|
||||
seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
|
||||
|
||||
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
|
||||
sequence_ff(seq);
|
||||
|
||||
if (!linear_consequent && mode_assume)
|
||||
log_error("Non-linear consequent is currently not supported in SVA assumptions.\n");
|
||||
|
||||
if (linear_consequent)
|
||||
{
|
||||
parse_sequence(seq, inst->GetInput2());
|
||||
}
|
||||
else
|
||||
{
|
||||
SigBit activated;
|
||||
seq.sig_en = make_temporal_one_hot(seq.sig_en, &activated);
|
||||
|
||||
SigBit pass_latch_en = module->addWire(NEW_ID);
|
||||
SigBit pass_latch = make_permanent_latch(pass_latch_en, true);
|
||||
|
||||
vector<SigBit> alive_list;
|
||||
sva_sequence_alive_list.push_back(&alive_list);
|
||||
parse_sequence(seq, inst->GetInput2());
|
||||
sva_sequence_alive_list.pop_back();
|
||||
|
||||
module->addLogicAnd(NEW_ID, seq.sig_a, seq.sig_en, pass_latch_en);
|
||||
alive_list.push_back(pass_latch);
|
||||
|
||||
seq.length = -1;
|
||||
seq.sig_a = module->ReduceOr(NEW_ID, SigSpec(alive_list));
|
||||
seq.sig_en = module->ReduceOr(NEW_ID, activated);
|
||||
}
|
||||
|
||||
return;
|
||||
}
|
||||
|
||||
if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
|
||||
{
|
||||
const char *sva_low_s = inst->GetAttValue("sva:low");
|
||||
const char *sva_high_s = inst->GetAttValue("sva:high");
|
||||
|
||||
int sva_low = atoi(sva_low_s);
|
||||
int sva_high = atoi(sva_high_s);
|
||||
bool sva_inf = !strcmp(sva_high_s, "$");
|
||||
|
||||
parse_sequence(seq, inst->GetInput1());
|
||||
|
||||
for (int i = 0; i < sva_low; i++)
|
||||
sequence_ff(seq);
|
||||
|
||||
if (sva_inf)
|
||||
{
|
||||
SigBit latched_a = module->addWire(NEW_ID);
|
||||
SigBit latched_en = module->addWire(NEW_ID);
|
||||
combine_seq(seq, latched_a, latched_en);
|
||||
|
||||
sequence_t seq_latched = seq;
|
||||
sequence_ff(seq_latched);
|
||||
module->connect(latched_a, seq_latched.sig_a);
|
||||
module->connect(latched_en, seq_latched.sig_en);
|
||||
}
|
||||
else
|
||||
{
|
||||
for (int i = sva_low; i < sva_high; i++)
|
||||
{
|
||||
sequence_t last_seq = seq;
|
||||
sequence_ff(seq);
|
||||
combine_seq(seq, last_seq);
|
||||
}
|
||||
}
|
||||
|
||||
parse_sequence(seq, inst->GetInput2());
|
||||
return;
|
||||
}
|
||||
|
||||
if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
|
||||
{
|
||||
const char *sva_low_s = inst->GetAttValue("sva:low");
|
||||
const char *sva_high_s = inst->GetAttValue("sva:high");
|
||||
|
||||
int sva_low = atoi(sva_low_s);
|
||||
int sva_high = atoi(sva_high_s);
|
||||
bool sva_inf = !strcmp(sva_high_s, "$");
|
||||
|
||||
parse_sequence(seq, inst->GetInput());
|
||||
|
||||
for (int i = 1; i < sva_low; i++) {
|
||||
sequence_ff(seq);
|
||||
parse_sequence(seq, inst->GetInput());
|
||||
}
|
||||
|
||||
if (sva_inf)
|
||||
{
|
||||
SigBit latched_a = module->addWire(NEW_ID);
|
||||
SigBit latched_en = module->addWire(NEW_ID);
|
||||
combine_seq(seq, latched_a, latched_en);
|
||||
|
||||
sequence_t seq_latched = seq;
|
||||
sequence_ff(seq_latched);
|
||||
parse_sequence(seq_latched, inst->GetInput());
|
||||
module->connect(latched_a, seq_latched.sig_a);
|
||||
module->connect(latched_en, seq_latched.sig_en);
|
||||
}
|
||||
else
|
||||
{
|
||||
for (int i = sva_low; i < sva_high; i++)
|
||||
{
|
||||
sequence_t last_seq = seq;
|
||||
sequence_ff(seq);
|
||||
parse_sequence(seq, inst->GetInput());
|
||||
combine_seq(seq, last_seq);
|
||||
}
|
||||
}
|
||||
|
||||
return;
|
||||
}
|
||||
|
||||
if (inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
|
||||
inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
|
||||
{
|
||||
bool flag_with = inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH;
|
||||
|
||||
if (get_ast_input1(inst) != nullptr)
|
||||
log_error("Currently only simple expression properties are supported as first operand to SVA_UNTIL.\n");
|
||||
|
||||
SigBit expr = importer->net_map_at(inst->GetInput1());
|
||||
|
||||
if (flag_with)
|
||||
{
|
||||
seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
|
||||
sva_until_list_inclusive.push_back(expr);
|
||||
parse_sequence(seq, inst->GetInput2());
|
||||
sva_until_list_inclusive.pop_back();
|
||||
}
|
||||
else
|
||||
{
|
||||
sva_until_list_exclusive.push_back(expr);
|
||||
parse_sequence(seq, inst->GetInput2());
|
||||
sva_until_list_exclusive.pop_back();
|
||||
}
|
||||
|
||||
return;
|
||||
}
|
||||
|
||||
// Handle unsupported primitives
|
||||
|
||||
if (!importer->mode_keep)
|
||||
log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name());
|
||||
log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->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);
|
||||
}
|
||||
#endif
|
||||
};
|
||||
|
||||
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;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue