diff options
Diffstat (limited to 'frontends/verific/verificsva.cc')
| -rw-r--r-- | frontends/verific/verificsva.cc | 1860 |
1 files changed, 1860 insertions, 0 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc new file mode 100644 index 000000000..49c0c40ac --- /dev/null +++ b/frontends/verific/verificsva.cc @@ -0,0 +1,1860 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at> + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ + + +// Currently supported SVA sequence and property syntax: +// http://symbiyosys.readthedocs.io/en/latest/verific.html +// +// Next gen property syntax: +// basic_property +// [antecedent_condition] property +// [antecedent_condition] always.. property +// [antecedent_condition] eventually.. basic_property +// [antecedent_condition] property until.. expression +// [antecedent_condition] basic_property until.. basic_property (assert/assume only) +// +// antecedent_condition: +// sequence |-> +// sequence |=> +// +// basic_property: +// sequence +// not basic_property +// nexttime basic_property +// nexttime[N] basic_property +// sequence #-# basic_property +// sequence #=# basic_property +// basic_property or basic_property (cover only) +// basic_property and basic_property (assert/assume only) +// basic_property implies basic_property +// basic_property iff basic_property +// +// sequence: +// expression +// sequence ##N sequence +// sequence ##[*] sequence +// sequence ##[+] sequence +// sequence ##[N:M] sequence +// sequence ##[N:$] sequence +// expression [*] +// expression [+] +// expression [*N] +// expression [*N:M] +// expression [*N:$] +// sequence or sequence +// sequence and sequence +// expression throughout sequence +// sequence intersect sequence +// sequence within sequence +// first_match( sequence ) +// expression [=N] +// expression [=N:M] +// expression [=N:$] +// expression [->N] +// expression [->N:M] +// expression [->N:$] + + +#include "kernel/yosys.h" +#include "frontends/verific/verific.h" + +USING_YOSYS_NAMESPACE + +#ifdef VERIFIC_NAMESPACE +using namespace Verific; +#endif + +PRIVATE_NAMESPACE_BEGIN + +// 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; + bool is_cond_node; +}; + +// 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, cond; + bool reachable; +}; + +// Deterministic FSM +struct SvaDFsmNode +{ + // A DFSM state corresponds to a set of NFSM states. We represent DFSM states as sorted vectors + // of NFSM state node ids. Edge/accept controls are constants matched against the ctrl sigspec. + SigSpec ctrl; + vector<pair<vector<int>, Const>> edges; + vector<Const> accept, reject; + + // additional temp data for getReject() + Wire *ffoutwire; + SigBit statesig; + SigSpec nextstate; + + // additional temp data for getDFsm() + int outnode; +}; + +struct SvaFsm +{ + Module *module; + VerificClocking clocking; + + SigBit trigger_sig = State::S1, disable_sig; + SigBit throughout_sig = State::S1; + bool in_cond_mode = false; + + vector<SigBit> disable_stack; + vector<SigBit> throughout_stack; + + int startNode, acceptNode, condNode; + vector<SvaNFsmNode> nodes; + + vector<SvaUFsmNode> unodes; + dict<vector<int>, SvaDFsmNode> dnodes; + dict<pair<SigSpec, SigSpec>, SigBit> cond_eq_cache; + bool materialized = false; + + SigBit final_accept_sig = State::Sx; + SigBit final_reject_sig = State::Sx; + + SvaFsm(const VerificClocking &clking, SigBit trig = State::S1) + { + module = clking.module; + clocking = clking; + trigger_sig = trig; + + startNode = createNode(); + acceptNode = createNode(); + + in_cond_mode = true; + condNode = createNode(); + in_cond_mode = false; + } + + void pushDisable(SigBit sig) + { + log_assert(!materialized); + + disable_stack.push_back(disable_sig); + + if (disable_sig == State::S0) + disable_sig = sig; + else + disable_sig = module->Or(NEW_ID, disable_sig, sig); + } + + void popDisable() + { + log_assert(!materialized); + log_assert(!disable_stack.empty()); + + disable_sig = disable_stack.back(); + disable_stack.pop_back(); + } + + void pushThroughout(SigBit sig) + { + log_assert(!materialized); + + throughout_stack.push_back(throughout_sig); + + if (throughout_sig == State::S1) + throughout_sig = sig; + else + throughout_sig = module->And(NEW_ID, throughout_sig, sig); + } + + void popThroughout() + { + log_assert(!materialized); + log_assert(!throughout_stack.empty()); + + throughout_sig = throughout_stack.back(); + throughout_stack.pop_back(); + } + + int createNode(int link_node = -1) + { + log_assert(!materialized); + + int idx = GetSize(nodes); + nodes.push_back(SvaNFsmNode()); + nodes.back().is_cond_node = in_cond_mode; + if (link_node >= 0) + createLink(link_node, idx); + return idx; + } + + int createStartNode() + { + return createNode(startNode); + } + + void createEdge(int from_node, int to_node, SigBit ctrl = State::S1) + { + log_assert(!materialized); + log_assert(0 <= from_node && from_node < GetSize(nodes)); + log_assert(0 <= to_node && to_node < GetSize(nodes)); + log_assert(from_node != acceptNode); + log_assert(to_node != acceptNode); + log_assert(from_node != condNode); + log_assert(to_node != condNode); + log_assert(to_node != startNode); + + if (from_node != startNode) + log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node); + + if (throughout_sig != State::S1) { + if (ctrl != State::S1) + ctrl = module->And(NEW_ID, throughout_sig, ctrl); + else + ctrl = throughout_sig; + } + + nodes[from_node].edges.push_back(make_pair(to_node, ctrl)); + } + + void createLink(int from_node, int to_node, SigBit ctrl = State::S1) + { + log_assert(!materialized); + log_assert(0 <= from_node && from_node < GetSize(nodes)); + log_assert(0 <= to_node && to_node < GetSize(nodes)); + log_assert(from_node != acceptNode); + log_assert(from_node != condNode); + log_assert(to_node != startNode); + + if (from_node != startNode) + log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node); + + if (throughout_sig != State::S1) { + if (ctrl != State::S1) + ctrl = module->And(NEW_ID, throughout_sig, ctrl); + else + ctrl = throughout_sig; + } + + nodes[from_node].links.push_back(make_pair(to_node, ctrl)); + } + + void make_link_order(vector<int> &order, int node, int min) + { + order[node] = std::max(order[node], min); + for (auto &it : nodes[node].links) + make_link_order(order, it.first, order[node]+1); + } + + // ---------------------------------------------------- + // Generating NFSM circuit to acquire accept signal + + SigBit getAccept() + { + log_assert(!materialized); + materialized = true; + + vector<Wire*> state_wire(GetSize(nodes)); + vector<SigBit> state_sig(GetSize(nodes)); + vector<SigBit> next_state_sig(GetSize(nodes)); + + // Create state signals + + { + SigBit not_disable = State::S1; + + if (disable_sig != State::S0) + not_disable = module->Not(NEW_ID, disable_sig); + + for (int i = 0; i < GetSize(nodes); i++) + { + Wire *w = module->addWire(NEW_ID); + state_wire[i] = w; + state_sig[i] = w; + + if (i == startNode) + state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig); + + if (disable_sig != State::S0) + state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable); + } + } + + // Follow Links + + { + vector<int> node_order(GetSize(nodes)); + vector<vector<int>> order_to_nodes; + + for (int i = 0; i < GetSize(nodes); i++) + make_link_order(node_order, i, 0); + + for (int i = 0; i < GetSize(nodes); i++) { + if (node_order[i] >= GetSize(order_to_nodes)) + order_to_nodes.resize(node_order[i]+1); + order_to_nodes[node_order[i]].push_back(i); + } + + for (int order = 0; order < GetSize(order_to_nodes); order++) + for (int node : order_to_nodes[order]) + { + for (auto &it : nodes[node].links) + { + int target = it.first; + SigBit ctrl = state_sig[node]; + + if (it.second != State::S1) + ctrl = module->And(NEW_ID, ctrl, it.second); + + state_sig[target] = module->Or(NEW_ID, state_sig[target], ctrl); + } + } + } + + // Construct activations + + { + vector<SigSpec> activate_sig(GetSize(nodes)); + vector<SigBit> activate_bit(GetSize(nodes)); + + for (int i = 0; i < GetSize(nodes); i++) { + for (auto &it : nodes[i].edges) + activate_sig[it.first].append(module->And(NEW_ID, state_sig[i], it.second)); + } + + for (int i = 0; i < GetSize(nodes); i++) { + if (GetSize(activate_sig[i]) == 0) + next_state_sig[i] = State::S0; + else if (GetSize(activate_sig[i]) == 1) + next_state_sig[i] = activate_sig[i]; + else + next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]); + } + } + + // Create state FFs + + for (int i = 0; i < GetSize(nodes); i++) + { + if (next_state_sig[i] != State::S0) { + clocking.addDff(NEW_ID, next_state_sig[i], state_wire[i], State::S0); + } else { + module->connect(state_wire[i], State::S0); + } + } + + final_accept_sig = state_sig[acceptNode]; + return final_accept_sig; + } + + // ---------------------------------------------------- + // Generating quantifier-based NFSM circuit to acquire reject signal + + SigBit getAnyAllRejectWorker(bool /* allMode */) + { + // FIXME + log_abort(); + } + + SigBit getAnyReject() + { + return getAnyAllRejectWorker(false); + } + + SigBit getAllReject() + { + return getAnyAllRejectWorker(true); + } + + // ---------------------------------------------------- + // Generating DFSM circuit to acquire reject signal + + void node_to_unode(int node, int unode, SigSpec ctrl) + { + if (node == acceptNode) + unodes[unode].accept.push_back(ctrl); + + if (node == condNode) + unodes[unode].cond.push_back(ctrl); + + for (auto &it : nodes[node].edges) { + if (it.second != State::S1) { + SigSpec s = {ctrl, it.second}; + s.sort_and_unify(); + unodes[unode].edges.push_back(make_pair(it.first, s)); + } else { + unodes[unode].edges.push_back(make_pair(it.first, ctrl)); + } + } + + for (auto &it : nodes[node].links) { + if (it.second != State::S1) { + SigSpec s = {ctrl, it.second}; + s.sort_and_unify(); + node_to_unode(it.first, unode, s); + } else { + node_to_unode(it.first, unode, ctrl); + } + } + } + + void mark_reachable_unode(int unode) + { + if (unodes[unode].reachable) + return; + + unodes[unode].reachable = true; + for (auto &it : unodes[unode].edges) + mark_reachable_unode(it.first); + } + + void usortint(vector<int> &vec) + { + vector<int> newvec; + std::sort(vec.begin(), vec.end()); + for (int i = 0; i < GetSize(vec); i++) + if (i == GetSize(vec)-1 || vec[i] != vec[i+1]) + newvec.push_back(vec[i]); + vec.swap(newvec); + } + + bool cmp_ctrl(const pool<SigBit> &ctrl_bits, const SigSpec &ctrl) + { + for (int i = 0; i < GetSize(ctrl); i++) + if (ctrl_bits.count(ctrl[i]) == 0) + return false; + return true; + } + + void create_dnode(const vector<int> &state, bool firstmatch, bool condaccept) + { + if (dnodes.count(state) != 0) + return; + + SvaDFsmNode dnode; + dnodes[state] = SvaDFsmNode(); + + for (int unode : state) { + log_assert(unodes[unode].reachable); + for (auto &it : unodes[unode].edges) + dnode.ctrl.append(it.second); + for (auto &it : unodes[unode].accept) + dnode.ctrl.append(it); + for (auto &it : unodes[unode].cond) + dnode.ctrl.append(it); + } + + dnode.ctrl.sort_and_unify(); + + if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) { + if (verific_verbose >= 2) { + log(" detected state explosion in DFSM generation:\n"); + dump(); + log(" ctrl signal: %s\n", log_signal(dnode.ctrl)); + } + log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n", + GetSize(dnode.ctrl), verific_sva_fsm_limit); + } + + for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++) + { + Const ctrl_val(i, GetSize(dnode.ctrl)); + pool<SigBit> ctrl_bits; + + for (int i = 0; i < GetSize(dnode.ctrl); i++) + if (ctrl_val[i] == State::S1) + ctrl_bits.insert(dnode.ctrl[i]); + + vector<int> new_state; + bool accept = false, cond = false; + + for (int unode : state) { + for (auto &it : unodes[unode].accept) + if (cmp_ctrl(ctrl_bits, it)) + accept = true; + for (auto &it : unodes[unode].cond) + if (cmp_ctrl(ctrl_bits, it)) + cond = true; + } + + bool new_state_cond = false; + bool new_state_noncond = false; + + if (accept && condaccept) + accept = cond; + + if (!accept || !firstmatch) { + for (int unode : state) + for (auto &it : unodes[unode].edges) + if (cmp_ctrl(ctrl_bits, it.second)) { + if (nodes.at(it.first).is_cond_node) + new_state_cond = true; + else + new_state_noncond = true; + new_state.push_back(it.first); + } + } + + if (accept) + dnode.accept.push_back(ctrl_val); + + if (condaccept && (!new_state_cond || !new_state_noncond)) + new_state.clear(); + + if (new_state.empty()) { + if (!accept) + dnode.reject.push_back(ctrl_val); + } else { + usortint(new_state); + dnode.edges.push_back(make_pair(new_state, ctrl_val)); + create_dnode(new_state, firstmatch, condaccept); + } + } + + dnodes[state] = dnode; + } + + void optimize_cond(vector<Const> &values) + { + bool did_something = true; + + while (did_something) + { + did_something = false; + + for (int i = 0; i < GetSize(values); i++) + for (int j = 0; j < GetSize(values); j++) + { + if (i == j) + continue; + + log_assert(GetSize(values[i]) == GetSize(values[j])); + + int delta_pos = -1; + bool i_within_j = true; + bool j_within_i = true; + + for (int k = 0; k < GetSize(values[i]); k++) { + if (values[i][k] == State::Sa && values[j][k] != State::Sa) { + i_within_j = false; + continue; + } + if (values[i][k] != State::Sa && values[j][k] == State::Sa) { + j_within_i = false; + continue; + } + if (values[i][k] == values[j][k]) + continue; + if (delta_pos >= 0) + goto next_pair; + delta_pos = k; + } + + if (delta_pos >= 0 && i_within_j && j_within_i) { + did_something = true; + values[i][delta_pos] = State::Sa; + values[j] = values.back(); + values.pop_back(); + goto next_pair; + } + + if (delta_pos < 0 && i_within_j) { + did_something = true; + values[i] = values.back(); + values.pop_back(); + goto next_pair; + } + + if (delta_pos < 0 && j_within_i) { + did_something = true; + values[j] = values.back(); + values.pop_back(); + goto next_pair; + } + next_pair:; + } + } + } + + SigBit make_cond_eq(const SigSpec &ctrl, const Const &value, SigBit enable = State::S1) + { + SigSpec sig_a, sig_b; + + log_assert(GetSize(ctrl) == GetSize(value)); + + for (int i = 0; i < GetSize(ctrl); i++) + if (value[i] != State::Sa) { + sig_a.append(ctrl[i]); + sig_b.append(value[i]); + } + + if (GetSize(sig_a) == 0) + return enable; + + if (enable != State::S1) { + sig_a.append(enable); + sig_b.append(State::S1); + } + + auto key = make_pair(sig_a, sig_b); + + if (cond_eq_cache.count(key) == 0) + { + if (sig_b == State::S1) + cond_eq_cache[key] = sig_a; + else if (sig_b == State::S0) + cond_eq_cache[key] = module->Not(NEW_ID, sig_a); + else + cond_eq_cache[key] = module->Eq(NEW_ID, sig_a, sig_b); + + if (verific_verbose >= 2) { + log(" Cond: %s := %s == %s\n", log_signal(cond_eq_cache[key]), + log_signal(sig_a), log_signal(sig_b)); + } + } + + return cond_eq_cache.at(key); + } + + void getFirstAcceptReject(SigBit *accept_p, SigBit *reject_p) + { + log_assert(!materialized); + materialized = true; + + // Create unlinked NFSM + + unodes.resize(GetSize(nodes)); + + for (int node = 0; node < GetSize(nodes); node++) + node_to_unode(node, node, SigSpec()); + + mark_reachable_unode(startNode); + + // Create DFSM + + create_dnode(vector<int>{startNode}, true, false); + dnodes.sort(); + + // Create DFSM Circuit + + SigSpec accept_sig, reject_sig; + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dnode.ffoutwire = module->addWire(NEW_ID); + dnode.statesig = dnode.ffoutwire; + + if (it.first == vector<int>{startNode}) + dnode.statesig = module->Or(NEW_ID, dnode.statesig, trigger_sig); + } + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dict<vector<int>, vector<Const>> edge_cond; + + for (auto &edge : dnode.edges) + edge_cond[edge.first].push_back(edge.second); + + for (auto &it : edge_cond) { + optimize_cond(it.second); + for (auto &value : it.second) + dnodes.at(it.first).nextstate.append(make_cond_eq(dnode.ctrl, value, dnode.statesig)); + } + + if (accept_p) { + vector<Const> accept_cond = dnode.accept; + optimize_cond(accept_cond); + for (auto &value : accept_cond) + accept_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig)); + } + + if (reject_p) { + vector<Const> reject_cond = dnode.reject; + optimize_cond(reject_cond); + for (auto &value : reject_cond) + reject_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig)); + } + } + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + if (GetSize(dnode.nextstate) == 0) { + module->connect(dnode.ffoutwire, State::S0); + } else + if (GetSize(dnode.nextstate) == 1) { + clocking.addDff(NEW_ID, dnode.nextstate, dnode.ffoutwire, State::S0); + } else { + SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate); + clocking.addDff(NEW_ID, nextstate, dnode.ffoutwire, State::S0); + } + } + + if (accept_p) + { + if (GetSize(accept_sig) == 0) + final_accept_sig = State::S0; + else if (GetSize(accept_sig) == 1) + final_accept_sig = accept_sig; + else + final_accept_sig = module->ReduceOr(NEW_ID, accept_sig); + *accept_p = final_accept_sig; + } + + if (reject_p) + { + if (GetSize(reject_sig) == 0) + final_reject_sig = State::S0; + else if (GetSize(reject_sig) == 1) + final_reject_sig = reject_sig; + else + final_reject_sig = module->ReduceOr(NEW_ID, reject_sig); + *reject_p = final_reject_sig; + } + } + + SigBit getFirstAccept() + { + SigBit accept; + getFirstAcceptReject(&accept, nullptr); + return accept; + } + + SigBit getReject() + { + SigBit reject; + getFirstAcceptReject(nullptr, &reject); + return reject; + } + + void getDFsm(SvaFsm &output_fsm, int output_start_node, int output_accept_node, int output_reject_node = -1, bool firstmatch = true, bool condaccept = false) + { + log_assert(!materialized); + materialized = true; + + // Create unlinked NFSM + + unodes.resize(GetSize(nodes)); + + for (int node = 0; node < GetSize(nodes); node++) + node_to_unode(node, node, SigSpec()); + + mark_reachable_unode(startNode); + + // Create DFSM + + create_dnode(vector<int>{startNode}, firstmatch, condaccept); + dnodes.sort(); + + // Create DFSM Graph + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dnode.outnode = output_fsm.createNode(); + + if (it.first == vector<int>{startNode}) + output_fsm.createLink(output_start_node, dnode.outnode); + + if (output_accept_node >= 0) { + vector<Const> accept_cond = dnode.accept; + optimize_cond(accept_cond); + for (auto &value : accept_cond) + output_fsm.createLink(it.second.outnode, output_accept_node, make_cond_eq(dnode.ctrl, value)); + } + + if (output_reject_node >= 0) { + vector<Const> reject_cond = dnode.reject; + optimize_cond(reject_cond); + for (auto &value : reject_cond) + output_fsm.createLink(it.second.outnode, output_reject_node, make_cond_eq(dnode.ctrl, value)); + } + } + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + dict<vector<int>, vector<Const>> edge_cond; + + for (auto &edge : dnode.edges) + edge_cond[edge.first].push_back(edge.second); + + for (auto &it : edge_cond) { + optimize_cond(it.second); + for (auto &value : it.second) + output_fsm.createEdge(dnode.outnode, dnodes.at(it.first).outnode, make_cond_eq(dnode.ctrl, value)); + } + } + } + + // ---------------------------------------------------- + // State dump for verbose log messages + + void dump_nodes() + { + if (nodes.empty()) + return; + + log(" non-deterministic encoding:\n"); + for (int i = 0; i < GetSize(nodes); i++) + { + log(" node %d:%s\n", i, + i == startNode ? " [start]" : + i == acceptNode ? " [accept]" : + i == condNode ? " [cond]" : ""); + + for (auto &it : nodes[i].edges) { + if (it.second != State::S1) + log(" edge %s -> %d\n", log_signal(it.second), it.first); + else + log(" edge -> %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); + } + } + } + + void dump_unodes() + { + if (unodes.empty()) + return; + + log(" unlinked non-deterministic encoding:\n"); + for (int i = 0; i < GetSize(unodes); i++) + { + if (!unodes[i].reachable) + continue; + + log(" unode %d:%s\n", i, i == startNode ? " [start]" : ""); + + for (auto &it : unodes[i].edges) { + if (!it.second.empty()) + log(" edge %s -> %d\n", log_signal(it.second), it.first); + else + log(" edge -> %d\n", it.first); + } + + for (auto &ctrl : unodes[i].accept) { + if (!ctrl.empty()) + log(" accept %s\n", log_signal(ctrl)); + else + log(" accept\n"); + } + + for (auto &ctrl : unodes[i].cond) { + if (!ctrl.empty()) + log(" cond %s\n", log_signal(ctrl)); + else + log(" cond\n"); + } + } + } + + void dump_dnodes() + { + if (dnodes.empty()) + return; + + log(" deterministic encoding:\n"); + for (auto &it : dnodes) + { + log(" dnode {"); + for (int i = 0; i < GetSize(it.first); i++) + log("%s%d", i ? "," : "", it.first[i]); + log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : ""); + + log(" ctrl %s\n", log_signal(it.second.ctrl)); + + for (auto &edge : it.second.edges) { + log(" edge %s -> {", log_signal(edge.second)); + for (int i = 0; i < GetSize(edge.first); i++) + log("%s%d", i ? "," : "", edge.first[i]); + log("}\n"); + } + + for (auto &value : it.second.accept) + log(" accept %s\n", log_signal(value)); + + for (auto &value : it.second.reject) + log(" reject %s\n", log_signal(value)); + } + } + + void dump() + { + if (!nodes.empty()) + log(" number of NFSM states: %d\n", GetSize(nodes)); + + if (!unodes.empty()) { + int count = 0; + for (auto &unode : unodes) + if (unode.reachable) + count++; + log(" number of reachable UFSM states: %d\n", count); + } + + if (!dnodes.empty()) + log(" number of DFSM states: %d\n", GetSize(dnodes)); + + if (verific_verbose >= 2) { + dump_nodes(); + dump_unodes(); + dump_dnodes(); + } + + if (trigger_sig != State::S1) + log(" trigger signal: %s\n", log_signal(trigger_sig)); + + if (final_accept_sig != State::Sx) + log(" accept signal: %s\n", log_signal(final_accept_sig)); + + if (final_reject_sig != State::Sx) + log(" reject signal: %s\n", log_signal(final_reject_sig)); + } +}; + +PRIVATE_NAMESPACE_END + +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; + Module *module = nullptr; + + Netlist *netlist = nullptr; + Instance *root = nullptr; + + VerificClocking clocking; + + bool mode_assert = false; + bool mode_assume = false; + bool mode_cover = false; + bool mode_trigger = false; + + Instance *net_to_ast_driver(Net *n) + { + if (n == nullptr) + return nullptr; + + if (n->IsMultipleDriven()) + return nullptr; + + Instance *inst = n->Driver(); + + if (inst == nullptr) + return nullptr; + + if (!verific_sva_prims.count(inst->Type())) + return nullptr; + + if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL || + inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || + inst->Type() == PRIM_SVA_PAST || inst->Type() == PRIM_SVA_TRIGGERED) + return nullptr; + + return inst; + } + + Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); } + Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); } + Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); } + 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 Importer + + struct ParserErrorException { + }; + + [[noreturn]] void parser_error(std::string errmsg) + { + if (!importer->mode_keep) + log_error("%s", errmsg.c_str()); + log_warning("%s", errmsg.c_str()); + throw ParserErrorException(); + } + + [[noreturn]] void parser_error(std::string errmsg, linefile_type loc) + { + parser_error(stringf("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc))); + } + + [[noreturn]] void parser_error(std::string errmsg, Instance *inst) + { + parser_error(stringf("%s at %s (%s)", errmsg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile()); + } + + [[noreturn]] void parser_error(Instance *inst) + { + parser_error(stringf("Verific SVA primitive %s (%s) is currently unsupported in this context", + inst->View()->Owner()->Name(), inst->Name()), inst->Linefile()); + } + + dict<Net*, bool, hash_ptr_ops> check_expression_cache; + + bool check_expression(Net *net, bool raise_error = false) + { + while (!check_expression_cache.count(net)) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) { + check_expression_cache[net] = true; + break; + } + + if (inst->Type() == PRIM_SVA_AT) + { + VerificClocking new_clocking(importer, net); + log_assert(new_clocking.cond_net == nullptr); + if (!clocking.property_matches_sequence(new_clocking)) + parser_error("Mixed clocking is currently not supported", inst); + check_expression_cache[net] = check_expression(new_clocking.body_net, raise_error); + break; + } + + if (inst->Type() == PRIM_SVA_FIRST_MATCH || inst->Type() == PRIM_SVA_NOT) + { + check_expression_cache[net] = check_expression(inst->GetInput(), raise_error); + break; + } + + if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_INTERSECT || + inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT || + inst->Type() == PRIM_SVA_OR || inst->Type() == PRIM_SVA_AND) + { + check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error); + break; + } + + 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, "$"); + + if (sva_low == 0 && sva_high == 0 && !sva_inf) + check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error); + else + check_expression_cache[net] = false; + break; + } + + check_expression_cache[net] = false; + } + + if (raise_error && !check_expression_cache.at(net)) + parser_error(net_to_ast_driver(net)); + return check_expression_cache.at(net); + } + + SigBit parse_expression(Net *net) + { + check_expression(net, true); + + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) { + return importer->net_map_at(net); + } + + if (inst->Type() == PRIM_SVA_AT) + { + VerificClocking new_clocking(importer, net); + log_assert(new_clocking.cond_net == nullptr); + if (!clocking.property_matches_sequence(new_clocking)) + parser_error("Mixed clocking is currently not supported", inst); + return parse_expression(new_clocking.body_net); + } + + if (inst->Type() == PRIM_SVA_FIRST_MATCH) + return parse_expression(inst->GetInput()); + + if (inst->Type() == PRIM_SVA_NOT) + return module->Not(NEW_ID, parse_expression(inst->GetInput())); + + if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR) + return module->Or(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2())); + + if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND || inst->Type() == PRIM_SVA_INTERSECT || + inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_SEQ_CONCAT) + return module->And(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2())); + + log_abort(); + } + + bool check_zero_consecutive_repeat(Net *net) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) + return false; + + if (inst->Type() != PRIM_SVA_CONSECUTIVE_REPEAT) + return false; + + const char *sva_low_s = inst->GetAttValue("sva:low"); + int sva_low = atoi(sva_low_s); + + return sva_low == 0; + } + + int parse_consecutive_repeat(SvaFsm &fsm, int start_node, Net *net, bool add_pre_delay, bool add_post_delay) + { + Instance *inst = net_to_ast_driver(net); + + log_assert(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, "$"); + + Net *body_net = inst->GetInput(); + + if (add_pre_delay || add_post_delay) + log_assert(sva_low == 0); + + if (sva_low == 0) { + if (!add_pre_delay && !add_post_delay) + parser_error("Possibly zero-length consecutive repeat must follow or precede a delay of at least one cycle", inst); + sva_low++; + } + + int node = fsm.createNode(start_node); + start_node = node; + + if (add_pre_delay) { + node = fsm.createNode(start_node); + fsm.createEdge(start_node, node); + } + + int prev_node = node; + node = parse_sequence(fsm, node, body_net); + + for (int i = 1; i < sva_low; i++) + { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + + prev_node = node; + node = parse_sequence(fsm, next_node, body_net); + } + + if (sva_inf) + { + log_assert(prev_node >= 0); + fsm.createEdge(node, prev_node); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + + prev_node = node; + node = parse_sequence(fsm, next_node, body_net); + + fsm.createLink(prev_node, node); + } + } + + if (add_post_delay) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + if (add_pre_delay || add_post_delay) + fsm.createLink(start_node, node); + + return node; + } + + int parse_sequence(SvaFsm &fsm, int start_node, Net *net) + { + if (check_expression(net)) { + int node = fsm.createNode(); + fsm.createLink(start_node, node, parse_expression(net)); + return node; + } + + Instance *inst = net_to_ast_driver(net); + + if (inst->Type() == PRIM_SVA_AT) + { + VerificClocking new_clocking(importer, net); + log_assert(new_clocking.cond_net == nullptr); + if (!clocking.property_matches_sequence(new_clocking)) + parser_error("Mixed clocking is currently not supported", inst); + return parse_sequence(fsm, start_node, new_clocking.body_net); + } + + if (inst->Type() == PRIM_SVA_FIRST_MATCH) + { + SvaFsm match_fsm(clocking); + match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode); + + int node = fsm.createNode(); + match_fsm.getDFsm(fsm, start_node, node); + + if (verific_verbose) { + log(" First Match FSM:\n"); + match_fsm.dump(); + } + + return node; + } + + if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME) + { + 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); + log_assert(sva_low == sva_high); + + int node = start_node; + + for (int i = 0; i < sva_low; i++) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + return parse_sequence(fsm, node, inst->GetInput()); + } + + 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, "$"); + + int node = -1; + bool past_add_delay = false; + + if (check_zero_consecutive_repeat(inst->GetInput1()) && sva_low > 0) { + node = parse_consecutive_repeat(fsm, start_node, inst->GetInput1(), false, true); + sva_low--, sva_high--; + } else { + node = parse_sequence(fsm, start_node, inst->GetInput1()); + } + + if (check_zero_consecutive_repeat(inst->GetInput2()) && sva_low > 0) { + past_add_delay = true; + sva_low--, sva_high--; + } + + for (int i = 0; i < sva_low; i++) { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + node = next_node; + } + + if (sva_inf) + { + fsm.createEdge(node, node); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int next_node = fsm.createNode(); + fsm.createEdge(node, next_node); + fsm.createLink(node, next_node); + node = next_node; + } + } + + if (past_add_delay) + node = parse_consecutive_repeat(fsm, node, inst->GetInput2(), true, false); + else + node = parse_sequence(fsm, node, inst->GetInput2()); + + return node; + } + + if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) + { + return parse_consecutive_repeat(fsm, start_node, net, false, false); + } + + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_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, "$"); + + Net *body_net = inst->GetInput(); + int node = fsm.createNode(start_node); + + SigBit cond = parse_expression(body_net); + SigBit not_cond = module->Not(NEW_ID, cond); + + for (int i = 0; i < sva_low; i++) + { + int wait_node = fsm.createNode(); + fsm.createEdge(wait_node, wait_node, not_cond); + + if (i == 0) + fsm.createLink(node, wait_node); + else + fsm.createEdge(node, wait_node); + + int next_node = fsm.createNode(); + fsm.createLink(wait_node, next_node, cond); + + node = next_node; + } + + if (sva_inf) + { + int wait_node = fsm.createNode(); + fsm.createEdge(wait_node, wait_node, not_cond); + fsm.createEdge(node, wait_node); + fsm.createLink(wait_node, node, cond); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int wait_node = fsm.createNode(); + fsm.createEdge(wait_node, wait_node, not_cond); + + if (i == 0) + fsm.createLink(node, wait_node); + else + fsm.createEdge(node, wait_node); + + int next_node = fsm.createNode(); + fsm.createLink(wait_node, next_node, cond); + + fsm.createLink(node, next_node); + node = next_node; + } + } + + if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT) + fsm.createEdge(node, node); + + return node; + } + + if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR) + { + int node = parse_sequence(fsm, start_node, inst->GetInput1()); + int node2 = parse_sequence(fsm, start_node, inst->GetInput2()); + fsm.createLink(node2, node); + return node; + } + + if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND) + { + SvaFsm fsm1(clocking); + fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode); + + SvaFsm fsm2(clocking); + fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode); + + SvaFsm combined_fsm(clocking); + fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); + fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); + + int node = fsm.createNode(); + combined_fsm.getDFsm(fsm, start_node, -1, node); + + if (verific_verbose) + { + log(" Left And FSM:\n"); + fsm1.dump(); + + log(" Right And FSM:\n"); + fsm1.dump(); + + log(" Combined And FSM:\n"); + combined_fsm.dump(); + } + + return node; + } + + if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN) + { + SvaFsm intersect_fsm(clocking); + + if (inst->Type() == PRIM_SVA_INTERSECT) + { + intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput1()), intersect_fsm.acceptNode); + } + else + { + int n = intersect_fsm.createNode(); + intersect_fsm.createLink(intersect_fsm.createStartNode(), n); + intersect_fsm.createEdge(n, n); + + n = parse_sequence(intersect_fsm, n, inst->GetInput1()); + + intersect_fsm.createLink(n, intersect_fsm.acceptNode); + intersect_fsm.createEdge(n, n); + } + + intersect_fsm.in_cond_mode = true; + intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput2()), intersect_fsm.condNode); + intersect_fsm.in_cond_mode = false; + + int node = fsm.createNode(); + intersect_fsm.getDFsm(fsm, start_node, node, -1, false, true); + + if (verific_verbose) { + log(" Intersect FSM:\n"); + intersect_fsm.dump(); + } + + return node; + } + + if (inst->Type() == PRIM_SVA_THROUGHOUT) + { + SigBit expr = parse_expression(inst->GetInput1()); + + fsm.pushThroughout(expr); + int node = parse_sequence(fsm, start_node, inst->GetInput2()); + fsm.popThroughout(); + + return node; + } + + parser_error(inst); + } + + void get_fsm_accept_reject(SvaFsm &fsm, SigBit *accept_p, SigBit *reject_p, bool swap_accept_reject = false) + { + log_assert(accept_p != nullptr || reject_p != nullptr); + + if (swap_accept_reject) + get_fsm_accept_reject(fsm, reject_p, accept_p); + else if (reject_p == nullptr) + *accept_p = fsm.getAccept(); + else if (accept_p == nullptr) + *reject_p = fsm.getReject(); + else + fsm.getFirstAcceptReject(accept_p, reject_p); + } + + bool eventually_property(Net *&net, SigBit &trig) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) + return false; + + if (clocking.cond_net != nullptr) + trig = importer->net_map_at(clocking.cond_net); + else + trig = State::S1; + + if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY) + { + if (mode_cover || mode_trigger) + parser_error(inst); + + net = inst->GetInput(); + clocking.cond_net = nullptr; + + return true; + } + + if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || + inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + { + Net *antecedent_net = inst->GetInput1(); + Net *consequent_net = inst->GetInput2(); + + Instance *consequent_inst = net_to_ast_driver(consequent_net); + + if (consequent_inst == nullptr) + return false; + + if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY) + return false; + + if (mode_cover || mode_trigger) + parser_error(consequent_inst); + + int node; + + SvaFsm antecedent_fsm(clocking, trig); + node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); + if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { + int next_node = antecedent_fsm.createNode(); + antecedent_fsm.createEdge(node, next_node); + node = next_node; + } + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); + + trig = antecedent_fsm.getAccept(); + net = consequent_inst->GetInput(); + clocking.cond_net = nullptr; + + if (verific_verbose) { + log(" Eventually Antecedent FSM:\n"); + antecedent_fsm.dump(); + } + + return true; + } + + return false; + } + + void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p) + { + Instance *inst = net_to_ast_driver(net); + + SigBit trig = State::S1; + + if (clocking.cond_net != nullptr) + trig = importer->net_map_at(clocking.cond_net); + + if (inst == nullptr) + { + log_assert(trig == State::S1); + + if (accept_p != nullptr) + *accept_p = importer->net_map_at(net); + if (reject_p != nullptr) + *reject_p = module->Not(NEW_ID, importer->net_map_at(net)); + } + else + if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || + inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + { + Net *antecedent_net = inst->GetInput1(); + Net *consequent_net = inst->GetInput2(); + int node; + + SvaFsm antecedent_fsm(clocking, trig); + node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); + if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { + int next_node = antecedent_fsm.createNode(); + antecedent_fsm.createEdge(node, next_node); + node = next_node; + } + + Instance *consequent_inst = net_to_ast_driver(consequent_net); + + if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL || + consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH || + consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)) + { + bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH; + + Net *until_net = nullptr; + if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS) + { + consequent_net = consequent_inst->GetInput(); + consequent_inst = net_to_ast_driver(consequent_net); + } + else + { + until_net = consequent_inst->GetInput2(); + consequent_net = consequent_inst->GetInput1(); + consequent_inst = net_to_ast_driver(consequent_net); + } + + SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0; + SigBit not_until_sig = module->Not(NEW_ID, until_sig); + antecedent_fsm.createEdge(node, node, not_until_sig); + + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode, until_with ? State::S1 : not_until_sig); + } + else + { + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); + } + + SigBit antecedent_match = antecedent_fsm.getAccept(); + + if (verific_verbose) { + log(" Antecedent FSM:\n"); + antecedent_fsm.dump(); + } + + bool consequent_not = false; + if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) { + consequent_not = true; + consequent_net = consequent_inst->GetInput(); + consequent_inst = net_to_ast_driver(consequent_net); + } + + SvaFsm consequent_fsm(clocking, antecedent_match); + node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net); + consequent_fsm.createLink(node, consequent_fsm.acceptNode); + + get_fsm_accept_reject(consequent_fsm, accept_p, reject_p, consequent_not); + + if (verific_verbose) { + log(" Consequent FSM:\n"); + consequent_fsm.dump(); + } + } + else + { + bool prop_not = inst->Type() == PRIM_SVA_NOT; + if (prop_not) { + net = inst->GetInput(); + inst = net_to_ast_driver(net); + } + + SvaFsm fsm(clocking, trig); + int node = parse_sequence(fsm, fsm.createStartNode(), net); + fsm.createLink(node, fsm.acceptNode); + + get_fsm_accept_reject(fsm, accept_p, reject_p, prop_not); + + if (verific_verbose) { + log(" Sequence FSM:\n"); + fsm.dump(); + } + } + } + + void import() + { + try + { + 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())); + + bool is_user_declared = root->IsUserDeclared(); + + // FIXME + if (!is_user_declared) { + const char *name = root->Name(); + for (int i = 0; name[i]; i++) { + if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) { + is_user_declared = true; + break; + } + } + } + + RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID); + + // parse SVA sequence into trigger signal + + clocking = VerificClocking(importer, root->GetInput(), true); + SigBit accept_bit = State::S0, reject_bit = State::S0; + + 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) { + reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput())); + } else { + accept_bit = parse_expression(root->GetInput()); + } + } + else + { + Net *net = clocking.body_net; + SigBit trig; + + if (eventually_property(net, trig)) + { + SigBit sig_a, sig_en = trig; + parse_property(net, &sig_a, nullptr); + + // add final FF stage + + 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 fair/live cell + + RTLIL::Cell *c = nullptr; + + if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q); + if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q); + + importer->import_attributes(c->attributes, root); + + return; + } + else + { + if (mode_assert || mode_assume) { + parse_property(net, nullptr, &reject_bit); + } else { + parse_property(net, &accept_bit, nullptr); + } + } + } + + if (mode_trigger) + { + module->connect(importer->net_map_at(root->GetOutput()), accept_bit); + } + else + { + SigBit sig_a = module->Not(NEW_ID, reject_bit); + SigBit sig_en = module->Or(NEW_ID, accept_bit, reject_bit); + + // add final FF stage + + 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 + + RTLIL::Cell *c = nullptr; + + if (mode_assert) c = module->addAssert(root_name, sig_a_q, sig_en_q); + if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q); + if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q); + + importer->import_attributes(c->attributes, root); + } + } + catch (ParserErrorException) + { + } + } +}; + +void verific_import_sva_assert(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assert = true; + worker.import(); +} + +void verific_import_sva_assume(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assume = true; + worker.import(); +} + +void verific_import_sva_cover(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_cover = true; + worker.import(); +} + +void verific_import_sva_trigger(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_trigger = true; + worker.import(); +} + +bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net) +{ + VerificSvaImporter worker; + worker.importer = importer; + return worker.net_to_ast_driver(net) != nullptr; +} + +YOSYS_NAMESPACE_END |