Add support for SVA until statements via Verific

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

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 4925389aeae171b84d9b4e4bc7cd421994feae4f..3d24b64cd0e25baddcb49bf8c0906f9649e7ca8f 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -60,29 +60,6 @@ using namespace Verific;
 #ifdef YOSYS_ENABLE_VERIFIC
 YOSYS_NAMESPACE_BEGIN
 
-pool<int> verific_sva_prims = {
-       // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
-       PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
-       PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
-       PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
-       PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
-       PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
-       PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
-       PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
-       PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
-       PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
-       PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
-       PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
-       PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
-       PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
-       PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
-       PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
-       PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
-       PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
-       PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
-       PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
-};
-
 string verific_error_msg;
 
 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 5a56b2fe0fa6883813b5616e11dae421a92c1236..760f03e2f2c6b5c7149e518052de7abc63068554 100644 (file)
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -28,6 +28,29 @@ using namespace Verific;
 
 YOSYS_NAMESPACE_BEGIN
 
+pool<int> verific_sva_prims = {
+       // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
+       PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
+       PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
+       PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
+       PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
+       PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
+       PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
+       PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
+       PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
+       PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
+       PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
+       PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
+       PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
+       PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
+       PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
+       PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
+       PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
+       PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
+       PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
+       PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
+};
+
 struct VerificSvaImporter
 {
        VerificImporter *importer = nullptr;
@@ -76,6 +99,57 @@ struct VerificSvaImporter
        Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
        Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
 
+       // ----------------------------------------------------------
+       // SVA AST Types
+
+       struct svatype_t
+       {
+               bool flag_linear = true;
+       };
+
+       std::map<Instance*, svatype_t> svatype_cache;
+
+       void svatype_visit_child(svatype_t &entry, Instance *inst)
+       {
+               if (inst == nullptr)
+                       return;
+
+               const svatype_t &child_entry = svatype(inst);
+               entry.flag_linear &= child_entry.flag_linear;
+       }
+
+       const svatype_t &svatype(Instance *inst)
+       {
+               if (svatype_cache.count(inst) != 0)
+                       return svatype_cache.at(inst);
+
+               svatype_t &entry = svatype_cache[inst];
+
+               if (inst == nullptr)
+                       return entry;
+
+               if (inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
+                               inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
+                       entry.flag_linear = false;
+
+               if (inst->Type() == PRIM_SVA_SEQ_CONCAT || inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
+               {
+                       int sva_low = atoi(inst->GetAttValue("sva:low"));
+                       int sva_high = atoi(inst->GetAttValue("sva:high"));
+
+                       if (sva_low != sva_high)
+                               entry.flag_linear = false;
+               }
+
+               svatype_visit_child(entry, get_ast_input(inst));
+               svatype_visit_child(entry, get_ast_input1(inst));
+               svatype_visit_child(entry, get_ast_input2(inst));
+               svatype_visit_child(entry, get_ast_input3(inst));
+               svatype_visit_child(entry, get_ast_control(inst));
+
+               return entry;
+       }
+
        // ----------------------------------------------------------
        // SVA Preprocessor
 
@@ -146,6 +220,9 @@ struct VerificSvaImporter
        // ----------------------------------------------------------
        // SVA Importer
 
+       vector<SigBit> sva_until_list_inclusive;
+       vector<SigBit> sva_until_list_exclusive;
+
        struct sequence_t {
                int length = 0;
                SigBit sig_a = State::S1;
@@ -162,6 +239,9 @@ struct VerificSvaImporter
                if (disable_iff != State::S0)
                        seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff);
 
+               for (auto &expr : sva_until_list_exclusive)
+                       seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
+
                Wire *sig_a_q = module->addWire(NEW_ID);
                sig_a_q->attributes["\\init"] = Const(0, 1);
 
@@ -174,6 +254,9 @@ struct VerificSvaImporter
                seq.length++;
                seq.sig_a = sig_a_q;
                seq.sig_en = sig_en_q;
+
+               for (auto &expr : sva_until_list_inclusive)
+                       seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
        }
 
        void parse_sequence(sequence_t &seq, Net *n)
@@ -189,19 +272,21 @@ struct VerificSvaImporter
 
                // SVA Primitives
 
-               if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION)
+               if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+                               inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
                {
-                       parse_sequence(seq, inst->GetInput1());
-                       seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
-                       parse_sequence(seq, inst->GetInput2());
-                       return;
-               }
+                       Instance *consequent = get_ast_input2(inst);
+                       bool linear_consequent = svatype(consequent).flag_linear;
 
-               if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
-               {
                        parse_sequence(seq, inst->GetInput1());
                        seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
-                       sequence_ff(seq);
+
+                       if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+                               sequence_ff(seq);
+
+                       if (!linear_consequent && mode_assume)
+                               log_error("Non-linear consequent is currently not supported in SVA assumptions.\n");
+
                        parse_sequence(seq, inst->GetInput2());
                        return;
                }
@@ -209,7 +294,7 @@ struct VerificSvaImporter
                if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
                {
                        int sva_low = atoi(inst->GetAttValue("sva:low"));
-                       int sva_high = atoi(inst->GetAttValue("sva:low"));
+                       int sva_high = atoi(inst->GetAttValue("sva:high"));
 
                        if (sva_low != sva_high)
                                log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n");
@@ -226,7 +311,7 @@ struct VerificSvaImporter
                if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
                {
                        int sva_low = atoi(inst->GetAttValue("sva:low"));
-                       int sva_high = atoi(inst->GetAttValue("sva:low"));
+                       int sva_high = atoi(inst->GetAttValue("sva:high"));
 
                        if (sva_low != sva_high)
                                log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n");
@@ -240,6 +325,29 @@ struct VerificSvaImporter
                        return;
                }
 
+               if (inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
+                               inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
+               {
+                       bool flag_with = inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH;
+                       SigBit expr = importer->net_map_at(inst->GetInput1());
+
+                       if (flag_with)
+                       {
+                               seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr);
+                               sva_until_list_inclusive.push_back(expr);
+                               parse_sequence(seq, inst->GetInput2());
+                               sva_until_list_inclusive.pop_back();
+                       }
+                       else
+                       {
+                               sva_until_list_exclusive.push_back(expr);
+                               parse_sequence(seq, inst->GetInput2());
+                               sva_until_list_exclusive.pop_back();
+                       }
+
+                       return;
+               }
+
                // Handle unsupported primitives
 
                if (!importer->mode_keep)

diff --git a/tests/sva/sva_until.sv b/tests/sva/sva_until.sv
new file mode 100644 (file)
index 0000000..a721e44
--- /dev/null
+++ b/tests/sva/sva_until.sv
@@ -0,0 +1,19 @@
+module top (
+       input clk,
+       input a, b, c, d
+);
+       default clocking @(posedge clk); endclocking
+
+       assert property (
+               a |=> b until_with (c ##1 d)
+       );
+
+`ifndef FAIL
+       assume property (
+               a |=> b && c
+       );
+       assume property (
+               b && c |=> b && d
+       );
+`endif
+endmodule