diff options
| author | Clifford Wolf <clifford@clifford.at> | 2019-11-22 18:10:34 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-22 18:10:34 +0100 |
| commit | caa3b21f8bc6af4a9e2115c9b599676a4dd11a2d (patch) | |
| tree | 9f4ec5ae19c28ff6c54fa01fd464cce130acafe2 | |
| parent | 72d2ef6fd071a8b2b9e1a77ddab3a9d632aa0f3d (diff) | |
| parent | db323685a4357ae0a04a8def9de29ef3a8ba16c2 (diff) | |
| download | yosys-caa3b21f8bc6af4a9e2115c9b599676a4dd11a2d.tar.gz yosys-caa3b21f8bc6af4a9e2115c9b599676a4dd11a2d.tar.bz2 yosys-caa3b21f8bc6af4a9e2115c9b599676a4dd11a2d.zip | |
Merge pull request #1515 from YosysHQ/clifford/svastuff
Add Verific/SVA support for "always" and "nexttime" properties
| -rw-r--r-- | frontends/verific/verific.cc | 4 | ||||
| -rw-r--r-- | frontends/verific/verificsva.cc | 42 |
2 files changed, 39 insertions, 7 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index de41e1a5c..843e7b9b4 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -789,7 +789,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name(); std::string module_name = netlist_name; - if (nl->IsOperator()) { + if (nl->IsOperator() || nl->IsPrimitive()) { module_name = "$verific$" + module_name; } else { if (!norename && *nl->Name()) { @@ -1409,7 +1409,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se std::string inst_type = inst->View()->Owner()->Name(); - if (inst->View()->IsOperator()) { + if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) { inst_type = "$verific$" + inst_type; } else { if (*inst->View()->Name()) { diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 909e9b4f1..49c0c40ac 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -36,6 +36,8 @@ // basic_property: // sequence // not basic_property +// nexttime basic_property +// nexttime[N] basic_property // sequence #-# basic_property // sequence #=# basic_property // basic_property or basic_property (cover only) @@ -1264,6 +1266,26 @@ struct VerificSvaImporter return node; } + if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME) + { + 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); + log_assert(sva_low == sva_high); + + int node = start_node; + + for (int i = 0; i < sva_low; i++) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + return parse_sequence(fsm, node, inst->GetInput()); + } + if (inst->Type() == PRIM_SVA_SEQ_CONCAT) { const char *sva_low_s = inst->GetAttValue("sva:low"); @@ -1590,15 +1612,25 @@ struct VerificSvaImporter Instance *consequent_inst = net_to_ast_driver(consequent_net); if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL || - consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH)) + consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH || + consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)) { bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH; - Net *until_net = consequent_inst->GetInput2(); - consequent_net = consequent_inst->GetInput1(); - consequent_inst = net_to_ast_driver(consequent_net); + Net *until_net = nullptr; + if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS) + { + consequent_net = consequent_inst->GetInput(); + consequent_inst = net_to_ast_driver(consequent_net); + } + else + { + until_net = consequent_inst->GetInput2(); + consequent_net = consequent_inst->GetInput1(); + consequent_inst = net_to_ast_driver(consequent_net); + } - SigBit until_sig = parse_expression(until_net); + SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0; SigBit not_until_sig = module->Not(NEW_ID, until_sig); antecedent_fsm.createEdge(node, node, not_until_sig); |