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

Fixed handling of synchronous and asynchronous assertion/assumption/cover in verific bindings 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-01-23 17:42:40 +01:00
parent 318be8651c
commit 1d8161b432
1 changed files with 29 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
frontends/verific/verific.cc
View File

@ -719,13 +719,13 @@ struct VerificImporter
FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{ {
if (inst->Type() == PRIM_SVA_ASSERT) if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
asserts.push_back(inst); asserts.push_back(inst);
if (inst->Type() == PRIM_SVA_ASSUME) if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
assumes.push_back(inst); assumes.push_back(inst);
if (inst->Type() == PRIM_SVA_COVER) if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
covers.push_back(inst); covers.push_back(inst);
} }
@ -1027,24 +1027,6 @@ struct VerificImporter
if (verbose) if (verbose)
log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name)); log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) {
Net *in = inst->GetInput();
module->addAssert(NEW_ID, net_map_at(in), State::S1);
continue;
}
if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) {
Net *in = inst->GetInput();
module->addAssume(NEW_ID, net_map_at(in), State::S1);
continue;
}
if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER) {
Net *in = inst->GetInput();
module->addCover(NEW_ID, net_map_at(in), State::S1);
continue;
}
if (inst->Type() == PRIM_PWR) { if (inst->Type() == PRIM_PWR) {
module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1); module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
continue; continue;
@ -1131,13 +1113,13 @@ struct VerificImporter
continue; continue;
} }
if (inst->Type() == PRIM_SVA_ASSERT) if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
sva_asserts.insert(inst); sva_asserts.insert(inst);
if (inst->Type() == PRIM_SVA_ASSUME) if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
sva_assumes.insert(inst); sva_assumes.insert(inst);
if (inst->Type() == PRIM_SVA_COVER) if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
sva_covers.insert(inst); sva_covers.insert(inst);
if (inst->Type() == OPER_SVA_STABLE && !mode_nosva) if (inst->Type() == OPER_SVA_STABLE && !mode_nosva)
@ -1336,7 +1318,8 @@ struct VerificSvaPP
if (inst == nullptr) if (inst == nullptr)
return default_net; return default_net;
if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) { 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)); Net *new_net = rewrite(get_ast_input(inst));
if (new_net) { if (new_net) {
inst->Disconnect(inst->View()->GetInput()); inst->Disconnect(inst->View()->GetInput());
@ -1568,9 +1551,30 @@ struct VerificSvaImporter
module = importer->module; module = importer->module;
netlist = root->Owner(); 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 // parse SVA property clock event
Instance *at_node = get_ast_input(root); 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());
if (eventually) {
if (mode_assert) module->addLive(root_name, sig_a, State::S1);
if (mode_assume) module->addFair(root_name, sig_a, State::S1);
} else {
if (mode_assert) module->addAssert(root_name, sig_a, State::S1);
if (mode_assume) module->addAssume(root_name, sig_a, State::S1);
if (mode_cover) module->addCover(root_name, sig_a, State::S1);
}
return;
}
log_assert(at_node && at_node->Type() == PRIM_SVA_AT); log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
@ -1608,8 +1612,6 @@ struct VerificSvaImporter
// generate assert/assume/cover cell // generate assert/assume/cover cell
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
if (eventually) { if (eventually) {
if (mode_assert) module->addLive(root_name, seq.sig_a, seq.sig_en); if (mode_assert) module->addLive(root_name, seq.sig_a, seq.sig_en);
if (mode_assume) module->addFair(root_name, seq.sig_a, seq.sig_en); if (mode_assume) module->addFair(root_name, seq.sig_a, seq.sig_en);