Add verific support for eventually properties

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 4e440b4caadde8f306fa4c1b7f9ecf92972c01c8..9312fd6e64dfe9eb565be51c84404ecaee54517e 100644 (file)
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -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);
+                                       }
                                }
                        }