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

Add verific support for eventually properties 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-06-29 19:21:04 +02:00
parent ebf0f003d3
commit 0404cf61d5
1 changed files with 105 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

110
frontends/verific/verificsva.cc
View File

@ -980,7 +980,6 @@ struct VerificSvaImporter
bool mode_assume = false;
bool mode_cover = false;
bool mode_trigger = false;
bool eventually = false;
Instance *net_to_ast_driver(Net *n)
{
@ -1487,6 +1486,69 @@ struct VerificSvaImporter
fsm.getFirstAcceptReject(accept_p, reject_p);
}
bool eventually_property(Net *&net, SigBit &trig)
{
if (clocking.cond_net != nullptr)
trig = importer->net_map_at(clocking.cond_net);
else
trig = State::S1;
Instance *inst = net_to_ast_driver(net);
if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
{
if (mode_cover || mode_trigger)
parser_error(inst);
net = inst->GetInput();
clocking.cond_net = nullptr;
return true;
}
if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
{
Net *antecedent_net = inst->GetInput1();
Net *consequent_net = inst->GetInput2();
Instance *consequent_inst = net_to_ast_driver(consequent_net);
if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY) {
return false;
}
if (mode_cover || mode_trigger)
parser_error(consequent_inst);
int node;
log_dump(trig);
SvaFsm antecedent_fsm(clocking, trig);
node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
int next_node = antecedent_fsm.createNode();
antecedent_fsm.createEdge(node, next_node);
node = next_node;
}
antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
trig = antecedent_fsm.getAccept();
net = consequent_inst->GetInput();
clocking.cond_net = nullptr;
if (verific_verbose) {
log(" Eventually Antecedent FSM:\n");
antecedent_fsm.dump();
log_dump(trig);
}
return true;
}
return false;
}
void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
{
Instance *inst = net_to_ast_driver(net);
@ -1620,10 +1682,48 @@ struct VerificSvaImporter
}
else
{
if (mode_assert || mode_assume) {
parse_property(clocking.body_net, nullptr, &reject_bit);
} else {
parse_property(clocking.body_net, &accept_bit, nullptr);
Net *net = clocking.body_net;
SigBit trig;
if (eventually_property(net, trig))
{
SigBit sig_a, sig_en = trig;
parse_property(net, &sig_a, nullptr);
log_dump(trig, sig_a, sig_en);
// add final FF stage
SigBit sig_a_q, sig_en_q;
if (clocking.body_net == nullptr) {
sig_a_q = sig_a;
sig_en_q = sig_en;
} else {
sig_a_q = module->addWire(NEW_ID);
sig_en_q = module->addWire(NEW_ID);
clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
}
// generate fair/live cell
RTLIL::Cell *c = nullptr;
if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);
importer->import_attributes(c->attributes, root);
return;
}
else
{
if (mode_assert || mode_assume) {
parse_property(net, nullptr, &reject_bit);
} else {
parse_property(net, &accept_bit, nullptr);
}
}
}