Fix handling of unclocked immediate assertions in Verific front-end

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

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 9f61d69a46ed91d138ab8ef638b09b53005cdb73..793e296f449e3ed014db1b4b526f211c4b53e455 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1297,7 +1297,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 // ==================================================================
 
-VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
+VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
 {
        module = importer->module;
 
@@ -1320,6 +1320,11 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
                        body_net = body_inst->GetInput2();
                }
        }
+       else
+       {
+               if (sva_at_only)
+                       return;
+       }
 
        if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
        {

diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 877d790579d63e41073ebfaa06299e0c4d8c6589..9e3e39695b8bbebcddf3ea790d15f5c3e1d790c8 100644 (file)
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -42,7 +42,7 @@ struct VerificClocking {
        bool posedge = true;
 
        VerificClocking() { }
-       VerificClocking(VerificImporter *importer, Verific::Net *net);
+       VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
        RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
        RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
        RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index c9c341516fb1e29d2e3d31e799494bec4fd9db4e..1a1000b1966154b89361bf023a9734bca20cf080 100644 (file)
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1543,20 +1543,33 @@ struct VerificSvaImporter
 
                        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)
-                               parser_error(stringf("Failed to parse SVA clocking"), root);
-
                        // parse SVA sequence into trigger signal
 
-                       Net *net = clocking.body_net;
-                       SigBit accept_bit = State::S0, reject_bit =  State::S0;
+                       clocking = VerificClocking(importer, root->GetInput(), true);
+                       SigBit accept_bit = State::S0, reject_bit = State::S0;
 
-                       if (mode_assert || mode_assume) {
-                               parse_property(net, nullptr, &reject_bit);
-                       } else {
-                               parse_property(net, &accept_bit, nullptr);
+                       if (clocking.body_net == nullptr)
+                       {
+                               if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr ||  clocking.cond_net != nullptr)
+                                       parser_error(stringf("Failed to parse SVA clocking"), root);
+
+                               if (mode_assert || mode_assume) {
+                                       log_ping();
+                                       reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
+                               } else {
+                                       log_ping();
+                                       accept_bit = parse_expression(root->GetInput());
+                               }
+                       }
+                       else
+                       {
+                               if (mode_assert || mode_assume) {
+                                       log_ping();
+                                       parse_property(clocking.body_net, nullptr, &reject_bit);
+                               } else {
+                                       log_ping();
+                                       parse_property(clocking.body_net, &accept_bit, nullptr);
+                               }
                        }
 
                        if (mode_trigger)
@@ -1570,10 +1583,17 @@ struct VerificSvaImporter
 
                                // add final FF stage
 
-                               SigBit sig_a_q = module->addWire(NEW_ID);
-                               SigBit 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);
+                               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 assert/assume/cover cell