diff options
Diffstat (limited to 'frontends/verific/verificsva.cc')
-rw-r--r-- | frontends/verific/verificsva.cc | 742 |
1 files changed, 139 insertions, 603 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index ceaca287d..5857c4496 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -72,11 +72,23 @@ using namespace Verific; PRIVATE_NAMESPACE_BEGIN -struct SvaFsmNode +// Non-deterministic FSM +struct SvaNFsmNode { + // Edge: Activate the target node if ctrl signal is true, consumes clock cycle + // Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle vector<pair<int, SigBit>> edges, links; }; +// Non-deterministic FSM after resolving links +struct SvaUFsmNode +{ + // Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle + // Accept: This node functions as an accept node if all bits in ctrl signal are true + vector<pair<int, SigSpec>> edges; + vector<SigSpec> accept; +}; + struct SvaFsm { Module *module; @@ -91,8 +103,11 @@ struct SvaFsm vector<SigBit> disable_stack; vector<SigBit> throughout_stack; - int startNode, acceptNode, rejectNode; - vector<SvaFsmNode> nodes; + int startNode, acceptNode; + vector<SvaNFsmNode> nodes; + + // ---------------------------------------------------- + // API for creating FSM SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1) { @@ -104,7 +119,6 @@ struct SvaFsm startNode = createNode(); acceptNode = createNode(); - rejectNode = createNode(); } void pushDisable(SigBit sig) @@ -149,32 +163,12 @@ struct SvaFsm throughout_stack.pop_back(); } - SigBit getAccept() - { - if (accept_sig != State::Sz) - return accept_sig; - - log_assert(!materialized); - accept_sig = module->addWire(NEW_ID); - return accept_sig; - } - - SigBit getReject() - { - if (reject_sig != State::Sz) - return reject_sig; - - log_assert(!materialized); - reject_sig = module->addWire(NEW_ID); - return reject_sig; - } - int createNode() { log_assert(!materialized); int idx = GetSize(nodes); - nodes.push_back(SvaFsmNode()); + nodes.push_back(SvaNFsmNode()); return idx; } @@ -217,15 +211,19 @@ struct SvaFsm make_link_order(order, it.first, order[node]+1); } - void materialize_ndfsm() + // ---------------------------------------------------- + // API for generating NFSM circuit to acquire accept signal + + SigBit getAccept() { log_assert(!materialized); materialized = true; - vector<SigBit> next_state_sig(GetSize(nodes)); + vector<Wire*> state_wire(GetSize(nodes)); vector<SigBit> state_sig(GetSize(nodes)); + vector<SigBit> next_state_sig(GetSize(nodes)); - // Create state FFs + // Create state signals { SigBit not_disable = State::S1; @@ -235,14 +233,10 @@ struct SvaFsm for (int i = 0; i < GetSize(nodes); i++) { - next_state_sig[i] = module->addWire(NEW_ID); - Wire *w = module->addWire(NEW_ID); - w->attributes["\\init"] = Const(0, 1); + state_wire[i] = w; state_sig[i] = w; - module->addDff(NEW_ID, clock, next_state_sig[i], state_sig[i], clockpol); - if (i == startNode) state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig); @@ -295,86 +289,92 @@ struct SvaFsm for (int i = 0; i < GetSize(nodes); i++) { if (GetSize(activate_sig[i]) == 0) - activate_bit[i] = State::S0; + next_state_sig[i] = State::S0; else if (GetSize(activate_sig[i]) == 1) - activate_bit[i] = activate_sig[i]; + next_state_sig[i] = activate_sig[i]; else - activate_bit[i] = module->ReduceOr(NEW_ID, activate_sig[i]); - } - - if (activate_bit[rejectNode] != State::S0) - { - SigBit not_rej = module->Not(NEW_ID, next_state_sig[rejectNode]); - for (int i = 0; i < GetSize(nodes); i++) - if (i != rejectNode && activate_bit[i] != State::S0) - activate_bit[i] = module->And(NEW_ID, activate_bit[i], not_rej); - activate_bit[rejectNode] = State::S0; - } - - for (int i = 0; i < GetSize(nodes); i++) { - module->connect(next_state_sig[i], activate_bit[i]); + next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]); } } - // Construct output signals - - if (accept_sig != State::Sz) { - module->connect(accept_sig, state_sig[acceptNode]); - } + // Create state FFs - if (reject_sig != State::Sz) + for (int i = 0; i < GetSize(nodes); i++) { - SigBit fsm_active = module->ReduceOr(NEW_ID, state_sig); - SigBit fsm_next_active = module->ReduceOr(NEW_ID, next_state_sig); - module->addEq(NEW_ID, {state_sig[acceptNode], fsm_next_active, fsm_active}, SigSpec(1, 3), reject_sig); + if (next_state_sig[i] != State::S0) { + state_wire[i]->attributes["\\init"] = Const(0, 1); + module->addDff(NEW_ID, clock, next_state_sig[i], state_wire[i], clockpol); + } else { + module->connect(state_wire[i], State::S0); + } } + + return state_sig[acceptNode]; } - void materialize_dfsm() + // ---------------------------------------------------- + // API for generating quantifier-based NFSM circuit to acquire reject signal + + SigBit getAnyAllRejectWorker(bool allMode) { // FIXME log_abort(); } - bool is_linear() + SigBit getAnyReject() { - for (int i = 0; i < GetSize(nodes); i++) - if (GetSize(nodes[i].edges) + GetSize(nodes[i].links) > 1) - return false; - return true; + return getAnyAllRejectWorker(false); + } + + SigBit getAllReject() + { + return getAnyAllRejectWorker(true); + } + + // ---------------------------------------------------- + // API for generating DFSM circuit to acquire reject signal + + SigBit getReject() + { + // FIXME + log("-----------------\n"); + dump(); + log_abort(); } + // ---------------------------------------------------- + // State dump for verbose log messages + void dump() { - log("-----------\n"); - for (int i = 0; i < GetSize(nodes); i++) + if (!nodes.empty()) { - log("node %d:\n", i); - - if (i == startNode) - log(" startNode\n"); + log(" non-deterministic encoding:\n"); + for (int i = 0; i < GetSize(nodes); i++) + { + log(" node %d:\n", i); - if (i == rejectNode) - log(" rejectNode\n"); + if (i == startNode) + log(" startNode\n"); - if (i == acceptNode) - log(" acceptNode\n"); + if (i == acceptNode) + log(" acceptNode\n"); - for (auto &it : nodes[i].edges) { - if (it.second != State::S1) - log(" egde %s -> %d\n", log_signal(it.second), it.first); - else - log(" egde -> %d\n", it.first); - } + for (auto &it : nodes[i].edges) { + if (it.second != State::S1) + log(" egde %s -> %d\n", log_signal(it.second), it.first); + else + log(" egde -> %d\n", it.first); + } - for (auto &it : nodes[i].links) { - if (it.second != State::S1) - log(" link %s -> %d\n", log_signal(it.second), it.first); - else - log(" link -> %d\n", it.first); + for (auto &it : nodes[i].links) { + if (it.second != State::S1) + log(" link %s -> %d\n", log_signal(it.second), it.first); + else + log(" link -> %d\n", it.first); + } } } - log("-----------\n"); } }; @@ -414,7 +414,7 @@ struct VerificSvaImporter Instance *root = nullptr; SigBit clock = State::Sx; - bool clock_posedge = false; + bool clockpol = false; SigBit disable_iff = State::S0; @@ -454,124 +454,6 @@ struct VerificSvaImporter 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_SEQ_CONCAT || inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) - { - 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_inf || 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 - - Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); } - Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); } - Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); } - Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); } - Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); } - - Net *rewrite(Instance *inst, Net *default_net = nullptr) - { - if (inst == nullptr) - return default_net; - - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME || - inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) { - Net *new_net = rewrite(get_ast_input(inst)); - if (new_net) { - inst->Disconnect(inst->View()->GetInput()); - inst->Connect(inst->View()->GetInput(), new_net); - } - return default_net; - } - - if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) { - Net *new_net = rewrite(get_ast_input2(inst)); - if (new_net) { - inst->Disconnect(inst->View()->GetInput2()); - inst->Connect(inst->View()->GetInput2(), new_net); - } - return default_net; - } - - if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) - { - if (mode_cover) { - did_something = true; - Net *new_in1 = rewrite_input1(inst); - Net *new_in2 = rewrite_input2(inst); - return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile()); - } - return default_net; - } - - if (inst->Type() == PRIM_SVA_NOT) - { - if (mode_assert || mode_assume) { - did_something = true; - Net *new_in = rewrite_input(inst); - Net *net_zero = netlist->Gnd(inst->Linefile()); - return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile()); - } - return default_net; - } - - return default_net; - } - - void rewrite() - { - netlist = root->Owner(); - do { - did_something = false; - rewrite(root); - } while (did_something); - } - - // ---------------------------------------------------------- // SVA Importer int parse_sequence(SvaFsm *fsm, int start_node, Net *net) @@ -687,6 +569,10 @@ struct VerificSvaImporter module = importer->module; netlist = root->Owner(); + if (verific_verbose) + log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(), + LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); + RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); // parse SVA property clock event @@ -717,25 +603,25 @@ struct VerificSvaImporter VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); clock = clock_edge.clock_sig; - clock_posedge = clock_edge.posedge; + clockpol = clock_edge.posedge; // parse disable_iff expression - Net *sequence_net = at_node->GetInput2(); + Net *net = at_node->GetInput2(); while (1) { - Instance *sequence_node = net_to_ast_driver(sequence_net); + Instance *sequence_node = net_to_ast_driver(net); if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { eventually = true; - sequence_net = sequence_node->GetInput(); + net = sequence_node->GetInput(); continue; } if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { disable_iff = importer->net_map_at(sequence_node->GetInput1()); - sequence_net = sequence_node->GetInput2(); + net = sequence_node->GetInput2(); continue; } @@ -745,11 +631,11 @@ struct VerificSvaImporter // parse SVA sequence into trigger signal SigBit prop_okay; - Instance *inst = net_to_ast_driver(sequence_net); + Instance *inst = net_to_ast_driver(net); if (inst == nullptr) { - prop_okay = importer->net_map_at(sequence_net); + prop_okay = importer->net_map_at(net); } else if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || @@ -759,7 +645,7 @@ struct VerificSvaImporter Net *consequent_net = inst->GetInput2(); int node; - SvaFsm antecedent_fsm(module, clock, clock_posedge, disable_iff); + SvaFsm antecedent_fsm(module, clock, clockpol, disable_iff); node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { int next_node = antecedent_fsm.createNode(); @@ -768,21 +654,50 @@ struct VerificSvaImporter } antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); - SigBit antecedent_accept = antecedent_fsm.getAccept(); - antecedent_fsm.materialize_ndfsm(); - antecedent_fsm.dump(); + SigBit antecedent_match = antecedent_fsm.getAccept(); - SvaFsm consequent_fsm(module, clock, clock_posedge, disable_iff, antecedent_accept); + if (verific_verbose) { + log(" Antecedent FSM:\n"); + antecedent_fsm.dump(); + } + + bool consequent_not = false; + Instance *consequent_inst = net_to_ast_driver(consequent_net); + + if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) { + consequent_not = true; + consequent_net = consequent_inst->GetInput(); + } + + SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match); node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net); consequent_fsm.createLink(node, consequent_fsm.acceptNode); - SigBit consequent_reject = consequent_fsm.getReject(); - prop_okay = module->Not(NEW_ID, consequent_reject); + if (mode_cover) { + prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept(); + } else { + SigBit consequent_match = consequent_not ? consequent_fsm.getAccept() : consequent_fsm.getReject(); + prop_okay = module->Not(NEW_ID, consequent_match); + } + + if (verific_verbose) { + log(" Consequent FSM:\n"); + antecedent_fsm.dump(); + } + } + else + if (inst->Type() == PRIM_SVA_NOT || mode_cover) + { + SvaFsm fsm(module, clock, clockpol, disable_iff); + int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput()); + fsm.createLink(node, fsm.acceptNode); + SigBit accept = fsm.getAccept(); + prop_okay = module->Not(NEW_ID, accept); - if (consequent_fsm.is_linear()) - consequent_fsm.materialize_ndfsm(); - else - log_error("Currently only linear sequences are allowed as impliciation consequent.\n"); + if (verific_verbose) { + log(" Sequence FSM:\n"); + fsm.dump(); + } } else { @@ -798,7 +713,7 @@ struct VerificSvaImporter Wire *prop_okay_q = module->addWire(NEW_ID); prop_okay_q->attributes["\\init"] = Const(mode_cover ? 0 : 1, 1); - module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clock_posedge); + module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clockpol); // generate assert/assume/cover cell @@ -816,387 +731,8 @@ struct VerificSvaImporter importer->import_attributes(c->attributes, root); } - -#if 0 - // ---------------------------------------------------------- - // Old SVA Importer - - vector<SigBit> sva_until_list_inclusive; - vector<SigBit> sva_until_list_exclusive; - vector<vector<SigBit>*> sva_sequence_alive_list; - - struct sequence_t { - int length = 0; - SigBit sig_a = State::S1; - SigBit sig_en = State::S1; - }; - - void sequence_cond(sequence_t &seq, SigBit cond) - { - seq.sig_a = module->And(NEW_ID, seq.sig_a, cond); - } - - void sequence_ff(sequence_t &seq) - { - 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); - - 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); - - if (seq.length >= 0) - 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 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); - - // Regular expression - - if (inst == nullptr) { - sequence_cond(seq, importer->net_map_at(n)); - return; - } - - // SVA Primitives - - if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || - inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) - { - Instance *consequent = get_ast_input2(inst); - bool linear_consequent = svatype(consequent).flag_linear; - - parse_sequence(seq, inst->GetInput1()); - seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a); - - 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"); - - 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<SigBit> 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) - { - 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, "$"); - - 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) - { - 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, "$"); - - parse_sequence(seq, inst->GetInput()); - - for (int i = 1; i < sva_low; i++) { - sequence_ff(seq); - parse_sequence(seq, inst->GetInput()); - } - - 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); - parse_sequence(seq_latched, inst->GetInput()); - 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); - parse_sequence(seq, inst->GetInput()); - combine_seq(seq, last_seq); - } - } - - return; - } - - if (inst->Type() == PRIM_SVA_THROUGHOUT || 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_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH; - - if (get_ast_input1(inst) != nullptr) - log_error("Currently only simple expression properties are supported as first operand to SVA_UNTIL.\n"); - - 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) - log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); - log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); - } - - void import() - { - module = importer->module; - netlist = root->Owner(); - - RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); - - // parse SVA property clock event - - Instance *at_node = get_ast_input(root); - - // asynchronous immediate assertion/assumption/cover - if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT || - root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME)) - { - SigSpec sig_a = importer->net_map_at(root->GetInput()); - RTLIL::Cell *c = nullptr; - - if (eventually) { - if (mode_assert) c = module->addLive(root_name, sig_a, State::S1); - if (mode_assume) c = module->addFair(root_name, sig_a, State::S1); - } else { - if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1); - if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1); - if (mode_cover) c = module->addCover(root_name, sig_a, State::S1); - } - - importer->import_attributes(c->attributes, root); - return; - } - - log_assert(at_node && at_node->Type() == PRIM_SVA_AT); - - VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); - clock = clock_edge.clock_sig; - clock_posedge = clock_edge.posedge; - - // parse disable_iff expression - - Net *sequence_net = at_node->GetInput2(); - - while (1) - { - Instance *sequence_node = net_to_ast_driver(sequence_net); - - if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { - eventually = true; - sequence_net = sequence_node->GetInput(); - continue; - } - - if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { - disable_iff = importer->net_map_at(sequence_node->GetInput1()); - sequence_net = sequence_node->GetInput2(); - continue; - } - - break; - } - - // parse SVA sequence into trigger signal - - sequence_t seq; - parse_sequence(seq, sequence_net); - sequence_ff(seq); - - // generate assert/assume/cover cell - - RTLIL::Cell *c = nullptr; - - if (eventually) { - if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en); - if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en); - } else { - if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en); - if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en); - if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en); - } - - importer->import_attributes(c->attributes, root); - } -#endif }; -void svapp_assert(Instance *inst) -{ - VerificSvaImporter worker; - worker.root = inst; - worker.mode_assert = true; - worker.rewrite(); -} - -void svapp_assume(Instance *inst) -{ - VerificSvaImporter worker; - worker.root = inst; - worker.mode_assume = true; - worker.rewrite(); -} - -void svapp_cover(Instance *inst) -{ - VerificSvaImporter worker; - worker.root = inst; - worker.mode_cover = true; - worker.rewrite(); -} - void import_sva_assert(VerificImporter *importer, Instance *inst) { VerificSvaImporter worker; |