Merge pull request #1517 from YosysHQ/clifford/optmem
Add "opt_mem" pass
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index de41e1a..843e7b9 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -789,7 +789,7 @@
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 @@
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 909e9b4..49c0c40 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 @@
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 @@
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);
