From 9d963cd29c499530bc4bcc66f298a6e56142c509 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 18 Feb 2018 14:57:52 +0100 Subject: [PATCH] Add support for SVA until statements via Verific Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 23 ------ frontends/verific/verificsva.cc | 130 +++++++++++++++++++++++++++++--- tests/sva/sva_until.sv | 19 +++++ 3 files changed, 138 insertions(+), 34 deletions(-) create mode 100644 tests/sva/sva_until.sv diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 4925389ae..3d24b64cd 100644 --- 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 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 5a56b2fe0..760f03e2f 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -28,6 +28,29 @@ using namespace Verific; YOSYS_NAMESPACE_BEGIN +pool 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 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 sva_until_list_inclusive; + vector 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 index 000000000..a721e44b5 --- /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 -- 2.30.2