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

Refactor Verific SVA importer property parser 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-04 14:29:48 +01:00
parent 261cf706f4
commit 9ab2498c55
1 changed files with 82 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

138
frontends/verific/verificsva.cc
View File

@ -29,7 +29,7 @@
// seq |-> not seq until seq.triggered // seq |-> not seq until seq.triggered
// //
// Currently supported sequence operators: // Currently supported sequence operators:
// expr ##[N:M] seq // seq ##[N:M] seq
// seq or seq // seq or seq
// expr throughout seq // expr throughout seq
// seq [*N:M] // seq [*N:M]
@ -753,6 +753,31 @@ struct VerificSvaImporter
// ---------------------------------------------------------- // ----------------------------------------------------------
// SVA Importer // SVA Importer
struct ParserErrorException {
};
[[noreturn]] void parser_error(std::string errmsg)
{
if (!importer->mode_keep)
log_error("%s", errmsg.c_str());
log_warning("%s", errmsg.c_str());
throw ParserErrorException();
}
[[noreturn]] void parser_error(std::string errmsg, linefile_type loc)
{
if (!importer->mode_keep)
log_error("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc));
log_warning("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc));
throw ParserErrorException();
}
[[noreturn]] void parser_error(Instance *inst)
{
parser_error(stringf("Verific SVA primitive %s (%s) is currently unsupported in this context",
inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
}
int parse_sequence(SvaFsm *fsm, int start_node, Net *net) int parse_sequence(SvaFsm *fsm, int start_node, Net *net)
{ {
Instance *inst = net_to_ast_driver(net); Instance *inst = net_to_ast_driver(net);
@ -860,41 +885,16 @@ struct VerificSvaImporter
return node; return node;
} }
// Handle unsupported primitives parser_error(inst);
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());
return start_node;
} }
void import() SigBit parse_property(Net *net)
{ {
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);
clocking = VerificClocking(importer, root->GetInput());
if (clocking.body_net == nullptr)
log_error("Failed to parse SVA clocking at %s (%s) at %s:%d.", root->Name(), root->View()->Owner()->Name(),
LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
// parse SVA sequence into trigger signal
SigBit prop_okay;
Net *net = clocking.body_net;
Instance *inst = net_to_ast_driver(net); Instance *inst = net_to_ast_driver(net);
if (inst == nullptr) if (inst == nullptr)
{ {
prop_okay = importer->net_map_at(net); return importer->net_map_at(net);
} }
else else
if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
@ -934,12 +934,8 @@ struct VerificSvaImporter
consequent_inst = net_to_ast_driver(consequent_net); consequent_inst = net_to_ast_driver(consequent_net);
if (until_inst != nullptr) { if (until_inst != nullptr) {
if (until_inst->Type() != PRIM_SVA_TRIGGERED) { if (until_inst->Type() != PRIM_SVA_TRIGGERED)
if (!importer->mode_keep) parser_error("Currently only boolean expressions or sequence.triggered is allowed in SVA_UNTIL condition", until_inst->Linefile());
log_error("Currently only boolean expressions or sequence.triggered is alowed in SVA_UNTIL condition.\n");
log_warning("Currently only boolean expressions or sequence.triggered is alowed in SVA_UNTIL condition.\n");
return;
}
until_net = until_inst->GetInput(); until_net = until_inst->GetInput();
} }
@ -976,6 +972,7 @@ struct VerificSvaImporter
node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net); node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net);
consequent_fsm.createLink(node, consequent_fsm.acceptNode); consequent_fsm.createLink(node, consequent_fsm.acceptNode);
SigBit prop_okay;
if (mode_cover) { if (mode_cover) {
prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept(); prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept();
} else { } else {
@ -987,6 +984,8 @@ struct VerificSvaImporter
log(" Consequent FSM:\n"); log(" Consequent FSM:\n");
consequent_fsm.dump(); consequent_fsm.dump();
} }
return prop_okay;
} }
else else
if (inst->Type() == PRIM_SVA_NOT || mode_cover) if (inst->Type() == PRIM_SVA_NOT || mode_cover)
@ -995,43 +994,70 @@ struct VerificSvaImporter
int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput()); int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput());
fsm.createLink(node, fsm.acceptNode); fsm.createLink(node, fsm.acceptNode);
SigBit accept = fsm.getAccept(); SigBit accept = fsm.getAccept();
prop_okay = module->Not(NEW_ID, accept); SigBit prop_okay = module->Not(NEW_ID, accept);
if (verific_verbose) { if (verific_verbose) {
log(" Sequence FSM:\n"); log(" Sequence FSM:\n");
fsm.dump(); fsm.dump();
} }
return prop_okay;
} }
else else
{ {
// Handle unsupported primitives // Handle unsupported primitives
parser_error(inst);
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());
return;
} }
}
// add final FF stage void import()
{
try
{
module = importer->module;
netlist = root->Owner();
SigBit prop_okay_q = module->addWire(NEW_ID); if (verific_verbose)
clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1)); 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()));
// generate assert/assume/cover cell RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
RTLIL::Cell *c = nullptr; clocking = VerificClocking(importer, root->GetInput());
if (eventually) { if (clocking.body_net == nullptr)
log_error("No support for eventually in Verific SVA bindings yet.\n"); parser_error(stringf("Failed to parse SVA clocking at %s (%s) at %s:%d.", root->Name(), root->View()->Owner()->Name(),
// if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q); LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())));
// if (mode_assume) c = module->addFair(root_name, prop_okay_q, prop_start_q);
} else { // parse SVA sequence into trigger signal
if (mode_assert) c = module->addAssert(root_name, prop_okay_q, State::S1);
if (mode_assume) c = module->addAssume(root_name, prop_okay_q, State::S1); Net *net = clocking.body_net;
if (mode_cover) c = module->addCover(root_name, prop_okay_q, State::S1); SigBit prop_okay = parse_property(net);
// add final FF stage
SigBit prop_okay_q = module->addWire(NEW_ID);
clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1));
// generate assert/assume/cover cell
RTLIL::Cell *c = nullptr;
if (eventually) {
parser_error("No support for eventually in Verific SVA bindings yet.\n");
// if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q);
// if (mode_assume) c = module->addFair(root_name, prop_okay_q, prop_start_q);
} else {
if (mode_assert) c = module->addAssert(root_name, prop_okay_q, State::S1);
if (mode_assume) c = module->addAssume(root_name, prop_okay_q, State::S1);
if (mode_cover) c = module->addCover(root_name, prop_okay_q, State::S1);
}
importer->import_attributes(c->attributes, root);
}
catch (ParserErrorException)
{
} }
importer->import_attributes(c->attributes, root);
} }
}; };