From 5c6247dfa6a5a0b8f1dfbec2810db54deb42deb3 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 18 Feb 2018 16:35:06 +0100 Subject: [PATCH] Add support for SVA sequence concatenation ranges via verific Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 140 ++++++++++++++++++++++++++++---- tests/sva/runtest.sh | 1 + tests/sva/sva_range.sv | 19 +++++ 3 files changed, 144 insertions(+), 16 deletions(-) create mode 100644 tests/sva/sva_range.sv diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 760f03e2f..c32095927 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -128,16 +128,16 @@ struct VerificSvaImporter 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")); + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); - if (sva_low != sva_high) + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); + + if (sva_inf || sva_low != sva_high) entry.flag_linear = false; } @@ -222,6 +222,7 @@ struct VerificSvaImporter vector sva_until_list_inclusive; vector sva_until_list_exclusive; + vector*> sva_sequence_alive_list; struct sequence_t { int length = 0; @@ -248,10 +249,15 @@ struct VerificSvaImporter Wire *sig_en_q = module->addWire(NEW_ID); sig_en_q->attributes["\\init"] = Const(0, 1); + for (auto list : sva_sequence_alive_list) + list->push_back(module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en)); + module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge); module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge); - seq.length++; + if (seq.length >= 0) + seq.length++; + seq.sig_a = sig_a_q; seq.sig_en = sig_en_q; @@ -259,6 +265,58 @@ struct VerificSvaImporter seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr); } + void combine_seq(sequence_t &seq, const sequence_t &other_seq) + { + if (seq.length != other_seq.length) + seq.length = -1; + + SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en); + SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_seq.sig_a, other_seq.sig_en); + + seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a); + seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_seq.sig_en); + } + + void combine_seq(sequence_t &seq, SigBit other_a, SigBit other_en) + { + SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en); + SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_a, other_en); + + seq.length = -1; + seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a); + seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_en); + } + + SigBit make_temporal_one_hot(SigBit enable = State::S1, SigBit *latched = nullptr) + { + Wire *state = module->addWire(NEW_ID); + state->attributes["\\init"] = State::S0; + + SigBit any = module->Anyseq(NEW_ID); + if (enable != State::S1) + any = module->LogicAnd(NEW_ID, any, enable); + + SigBit next_state = module->LogicOr(NEW_ID, state, any); + module->addDff(NEW_ID, clock, next_state, state, clock_posedge); + + if (latched != nullptr) + *latched = state; + + SigBit not_state = module->LogicNot(NEW_ID, state); + return module->LogicAnd(NEW_ID, next_state, not_state); + } + + SigBit make_permanent_latch(SigBit enable, bool async = false) + { + Wire *state = module->addWire(NEW_ID); + state->attributes["\\init"] = State::S0; + + SigBit next_state = module->LogicOr(NEW_ID, state, enable); + module->addDff(NEW_ID, clock, next_state, state, clock_posedge); + + return async ? next_state : state; + } + void parse_sequence(sequence_t &seq, Net *n) { Instance *inst = net_to_ast_driver(n); @@ -287,33 +345,83 @@ struct VerificSvaImporter if (!linear_consequent && mode_assume) log_error("Non-linear consequent is currently not supported in SVA assumptions.\n"); - parse_sequence(seq, inst->GetInput2()); + if (linear_consequent) + { + parse_sequence(seq, inst->GetInput2()); + } + else + { + SigBit activated; + seq.sig_en = make_temporal_one_hot(seq.sig_en, &activated); + + SigBit pass_latch_en = module->addWire(NEW_ID); + SigBit pass_latch = make_permanent_latch(pass_latch_en, true); + + vector alive_list; + sva_sequence_alive_list.push_back(&alive_list); + parse_sequence(seq, inst->GetInput2()); + sva_sequence_alive_list.pop_back(); + + module->addLogicAnd(NEW_ID, seq.sig_a, seq.sig_en, pass_latch_en); + alive_list.push_back(pass_latch); + + seq.length = -1; + seq.sig_a = module->ReduceOr(NEW_ID, SigSpec(alive_list)); + seq.sig_en = module->ReduceOr(NEW_ID, activated); + } + return; } if (inst->Type() == PRIM_SVA_SEQ_CONCAT) { - int sva_low = atoi(inst->GetAttValue("sva:low")); - int sva_high = atoi(inst->GetAttValue("sva:high")); + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); - if (sva_low != sva_high) - log_error("Ranges on SVA sequence concatenation operator are not supported at the moment.\n"); + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); parse_sequence(seq, inst->GetInput1()); for (int i = 0; i < sva_low; i++) sequence_ff(seq); + if (sva_inf) + { + SigBit latched_a = module->addWire(NEW_ID); + SigBit latched_en = module->addWire(NEW_ID); + combine_seq(seq, latched_a, latched_en); + + sequence_t seq_latched = seq; + sequence_ff(seq_latched); + module->connect(latched_a, seq_latched.sig_a); + module->connect(latched_en, seq_latched.sig_en); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + sequence_t last_seq = seq; + sequence_ff(seq); + combine_seq(seq, last_seq); + } + } + parse_sequence(seq, inst->GetInput2()); return; } if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) { - int sva_low = atoi(inst->GetAttValue("sva:low")); - int sva_high = atoi(inst->GetAttValue("sva:high")); + 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); + bool sva_inf = !strcmp(sva_high_s, "$"); - if (sva_low != sva_high) + if (sva_inf || sva_low != sva_high) log_error("Ranges on SVA consecutive repeat operator are not supported at the moment.\n"); parse_sequence(seq, inst->GetInput()); diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh index 4c8e16542..1b65ca9c9 100644 --- a/tests/sva/runtest.sh +++ b/tests/sva/runtest.sh @@ -35,6 +35,7 @@ generate_sby() { cat <<- EOT verific -import -extnets -all top prep -top top + chformal -early -assume [files] EOT diff --git a/tests/sva/sva_range.sv b/tests/sva/sva_range.sv new file mode 100644 index 000000000..38199bff1 --- /dev/null +++ b/tests/sva/sva_range.sv @@ -0,0 +1,19 @@ +module top ( + input clk, + input a, b, c, d +); + default clocking @(posedge clk); endclocking + + assert property ( + a ##[*] b |=> c until ##[*] d + ); + +`ifndef FAIL + assume property ( + b |=> ##5 d + ); + assume property ( + b || (c && !d) |=> c + ); +`endif +endmodule -- 2.30.2