From 25e33d7ab8ebeb96d6a7fb842e33f35770367587 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 27 Feb 2018 20:33:15 +0100 Subject: [PATCH 1/4] Major redesign of Verific SVA importer Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 578 +++++++++++++++++++++++++++++++- tests/sva/sva_range.sv | 2 +- 2 files changed, 574 insertions(+), 6 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 94443cd3e..ceaca287d 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -24,7 +24,6 @@ // not prop // prop or prop // prop and prop -// seq |-> prop // seq |=> prop // if (expr) prop [else prop] // prop until prop @@ -35,7 +34,6 @@ // // seq: // expr -// expr ##N seq // expr ##[N:M] seq // seq or seq // seq and seq @@ -43,12 +41,24 @@ // first_match (seq) // expr throughout seq // seq within seq -// seq [*N] // seq [*N:M] -// expr [=N] // expr [=N:M] -// expr [->N] // expr [->N:M] +// +// Notes: +// |=> is a placeholder for |-> and |=> +// "until" is a placeholder for all until operators +// ##[N:M], [*N:M], [=N:M], [->N:M] includes ##N, [*N], [=N], [->N] +// +// Currently supported property styles: +// not seq +// seq |=> seq +// seq |=> seq until seq +// +// Currently supported sequence operators: +// ##[N:M] +// [*N:M] +// throughout #include "kernel/yosys.h" @@ -60,6 +70,316 @@ USING_YOSYS_NAMESPACE using namespace Verific; #endif +PRIVATE_NAMESPACE_BEGIN + +struct SvaFsmNode +{ + vector> edges, links; +}; + +struct SvaFsm +{ + Module *module; + SigBit clock; + bool clockpol; + + SigBit trigger_sig = State::S1, disable_sig; + SigBit accept_sig = State::Sz, reject_sig = State::Sz; + SigBit throughout_sig = State::S1; + bool materialized = false; + + vector disable_stack; + vector throughout_stack; + + int startNode, acceptNode, rejectNode; + vector nodes; + + SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1) + { + module = mod; + clock = clk; + clockpol = clkpol; + disable_sig = dis; + trigger_sig = trig; + + startNode = createNode(); + acceptNode = createNode(); + rejectNode = createNode(); + } + + 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(); + } + + 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()); + return idx; + } + + 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)); + + 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)); + + 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 &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); + } + + void materialize_ndfsm() + { + log_assert(!materialized); + materialized = true; + + vector next_state_sig(GetSize(nodes)); + vector state_sig(GetSize(nodes)); + + // Create state FFs + + { + 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++) + { + next_state_sig[i] = module->addWire(NEW_ID); + + Wire *w = module->addWire(NEW_ID); + w->attributes["\\init"] = Const(0, 1); + 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); + + if (disable_sig != State::S0) + state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable); + } + } + + // Follow Links + + { + vector node_order(GetSize(nodes)); + vector> 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 activate_sig(GetSize(nodes)); + vector 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) + activate_bit[i] = State::S0; + else if (GetSize(activate_sig[i]) == 1) + activate_bit[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]); + } + } + + // Construct output signals + + if (accept_sig != State::Sz) { + module->connect(accept_sig, state_sig[acceptNode]); + } + + if (reject_sig != State::Sz) + { + 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); + } + } + + void materialize_dfsm() + { + // FIXME + log_abort(); + } + + bool is_linear() + { + for (int i = 0; i < GetSize(nodes); i++) + if (GetSize(nodes[i].edges) + GetSize(nodes[i].links) > 1) + return false; + return true; + } + + void dump() + { + log("-----------\n"); + for (int i = 0; i < GetSize(nodes); i++) + { + log("node %d:\n", i); + + if (i == startNode) + log(" startNode\n"); + + if (i == rejectNode) + log(" rejectNode\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].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"); + } +}; + +PRIVATE_NAMESPACE_END + YOSYS_NAMESPACE_BEGIN pool verific_sva_prims = { @@ -254,6 +574,253 @@ struct VerificSvaImporter // ---------------------------------------------------------- // SVA Importer + int parse_sequence(SvaFsm *fsm, int start_node, Net *net) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) { + int node = fsm->createNode(); + fsm->createLink(start_node, node, importer->net_map_at(net)); + return node; + } + + 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 = parse_sequence(fsm, start_node, inst->GetInput1()); + + 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; + } + } + + node = parse_sequence(fsm, node, inst->GetInput2()); + + return node; + } + + 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, "$"); + + int node = parse_sequence(fsm, start_node, inst->GetInput()); + + for (int i = 1; i < sva_low; i++) + { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + node = parse_sequence(fsm, next_node, inst->GetInput()); + } + + if (sva_inf) + { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + next_node = parse_sequence(fsm, next_node, inst->GetInput()); + fsm->createLink(next_node, node); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + next_node = parse_sequence(fsm, next_node, inst->GetInput()); + fsm->createLink(node, next_node); + node = next_node; + } + } + + return node; + } + + if (inst->Type() == PRIM_SVA_THROUGHOUT) + { + log_assert(get_ast_input1(inst) == nullptr); + SigBit expr = importer->net_map_at(inst->GetInput1()); + + fsm->pushThroughout(expr); + int node = parse_sequence(fsm, start_node, inst->GetInput2()); + fsm->popThroughout(); + + return node; + } + + // 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()); + + return start_node; + } + + 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 + + SigBit prop_okay; + Instance *inst = net_to_ast_driver(sequence_net); + + if (inst == nullptr) + { + prop_okay = importer->net_map_at(sequence_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(module, clock, clock_posedge, 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(); + antecedent_fsm.createEdge(node, next_node); + node = next_node; + } + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); + + SigBit antecedent_accept = antecedent_fsm.getAccept(); + antecedent_fsm.materialize_ndfsm(); + antecedent_fsm.dump(); + + SvaFsm consequent_fsm(module, clock, clock_posedge, disable_iff, antecedent_accept); + 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 (consequent_fsm.is_linear()) + consequent_fsm.materialize_ndfsm(); + else + log_error("Currently only linear sequences are allowed as impliciation consequent.\n"); + } + else + { + // 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()); + return; + } + + // add final FF stage + + 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); + + // generate assert/assume/cover cell + + RTLIL::Cell *c = nullptr; + + if (eventually) { + log_error("No support for eventually in Verific SVA bindings yet.\n"); + // if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q); + // if (mode_assume) c = module->addFair(root_name, prop_okay_q, prop_start_q); + } else { + if (mode_assert) c = module->addAssert(root_name, prop_okay_q, State::S1); + if (mode_assume) c = module->addAssume(root_name, prop_okay_q, State::S1); + if (mode_cover) c = module->addCover(root_name, prop_okay_q, State::S1); + } + + importer->import_attributes(c->attributes, root); + } + +#if 0 + // ---------------------------------------------------------- + // Old SVA Importer + vector sva_until_list_inclusive; vector sva_until_list_exclusive; vector*> sva_sequence_alive_list; @@ -603,6 +1170,7 @@ struct VerificSvaImporter importer->import_attributes(c->attributes, root); } +#endif }; void svapp_assert(Instance *inst) diff --git a/tests/sva/sva_range.sv b/tests/sva/sva_range.sv index 38199bff1..d1569fc83 100644 --- a/tests/sva/sva_range.sv +++ b/tests/sva/sva_range.sv @@ -5,7 +5,7 @@ module top ( default clocking @(posedge clk); endclocking assert property ( - a ##[*] b |=> c until ##[*] d + a ##[*] b |=> c until d ); `ifndef FAIL From 15902d495f8767fe86bbac1826cbedd1202264ef Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 28 Feb 2018 11:45:04 +0100 Subject: [PATCH 2/4] Continue refactoring of Verific SVA importer code Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 91 ++-- frontends/verific/verific.h | 10 +- frontends/verific/verificsva.cc | 742 ++++++-------------------------- 3 files changed, 172 insertions(+), 671 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index e85e6cf71..fc0f72be8 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -60,6 +60,7 @@ using namespace Verific; #ifdef YOSYS_ENABLE_VERIFIC YOSYS_NAMESPACE_BEGIN +bool verific_verbose; 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) @@ -97,9 +98,9 @@ string get_full_netlist_name(Netlist *nl) // ================================================================== -VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) : +VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names) : mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), - mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose) + mode_names(mode_names) { } @@ -642,13 +643,13 @@ void VerificImporter::merge_past_ffs_clock(pool &candidates, SigBi SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d)); RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol); - if (verbose) + if (verific_verbose) log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff)); for (int i = 0; i < GetSize(sig_d); i++) for (auto old_ff : dbits_db[sig_d[i]]) { - if (verbose) + if (verific_verbose) log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i); SigBit old_q = old_ff->getPort("\\Q"); @@ -711,38 +712,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se Instance *inst; PortRef *pr; - if (!mode_nosvapp) - { - vector asserts, assumes, covers; - - FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) - { - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) - asserts.push_back(inst); - - if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) - assumes.push_back(inst); - - if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER) - covers.push_back(inst); - } - - for (auto inst : asserts) - svapp_assert(inst); - - for (auto inst : assumes) - svapp_assume(inst); - - for (auto inst : covers) - svapp_cover(inst); - } - FOREACH_PORT_OF_NETLIST(nl, mi, port) { if (port->Bus()) continue; - if (verbose) + if (verific_verbose) log(" importing port %s.\n", port->Name()); RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name())); @@ -768,7 +743,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus) { - if (verbose) + if (verific_verbose) log(" importing portbus %s.\n", portbus->Name()); RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size()); @@ -882,7 +857,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se anyseq_nets.insert(net); if (net_map.count(net)) { - if (verbose) + if (verific_verbose) log(" skipping net %s.\n", net->Name()); continue; } @@ -892,7 +867,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID); - if (verbose) + if (verific_verbose) log(" importing net %s as %s.\n", net->Name(), log_id(wire_name)); RTLIL::Wire *wire = module->addWire(wire_name); @@ -916,7 +891,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se { RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID); - if (verbose) + if (verific_verbose) log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name)); RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size()); @@ -958,7 +933,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se } else { - if (verbose) + if (verific_verbose) log(" skipping netbus %s.\n", netbus->Name()); } @@ -1022,7 +997,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se { RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID); - if (verbose) + if (verific_verbose) log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name)); if (inst->Type() == PRIM_PWR) { @@ -1134,7 +1109,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se sig_o.append(net_map_at(inst->GetOutputBit(i))); } - if (verbose) { + if (verific_verbose) { log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", @@ -1156,7 +1131,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se SigSpec sig_o = net_map_at(inst->GetOutput()); SigSpec sig_q = module->addWire(NEW_ID); - if (verbose) { + if (verific_verbose) { log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", @@ -1177,7 +1152,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_q = net_map_at(inst->GetOutput()); - if (verbose) + if (verific_verbose) log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); @@ -1188,7 +1163,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se } if (!mode_keep && verific_sva_prims.count(inst->Type())) { - if (verbose) + if (verific_verbose) log(" skipping SVA cell in non k-mode\n"); continue; } @@ -1215,11 +1190,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se dict> cell_port_conns; - if (verbose) + if (verific_verbose) log(" ports in verific db:\n"); FOREACH_PORTREF_OF_INST(inst, mi2, pr) { - if (verbose) + if (verific_verbose) log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name()); const char *port_name = pr->GetPort()->Name(); int port_offset = 0; @@ -1238,11 +1213,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se sigvec[port_offset] = net_map_at(pr->GetNet()); } - if (verbose) + if (verific_verbose) log(" ports in yosys db:\n"); for (auto &it : cell_port_conns) { - if (verbose) + if (verific_verbose) log(" .%s(%s)\n", log_id(it.first), log_signal(it.second)); cell->setPort(it.first, it.second); } @@ -1292,7 +1267,6 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) struct VerificExtNets { int portname_cnt = 0; - bool verbose = false; // a map from Net to the same Net one level up in the design hierarchy std::map net_level_up; @@ -1347,7 +1321,7 @@ struct VerificExtNets if (!net->IsExternalTo(nl)) continue; - if (verbose) + if (verific_verbose) log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name()); while (net->IsExternalTo(nl)) @@ -1355,12 +1329,12 @@ struct VerificExtNets Net *newnet = get_net_level_up(net); if (newnet == net) break; - if (verbose) + if (verific_verbose) log(" external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name()); net = newnet; } - if (verbose) + if (verific_verbose) log(" final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : ""); todo_connect.push_back(tuple(inst, port, net)); } @@ -1444,9 +1418,6 @@ struct VerificPass : public Pass { log(" -nosva\n"); log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); - log(" -nosvapp\n"); - log(" Disable SVA properties pre-processing pass. This implies -nosva.\n"); - log("\n"); log(" -n\n"); log(" Keep all Verific names on instances and nets. By default only\n"); log(" user-declared names are preserved.\n"); @@ -1469,6 +1440,8 @@ struct VerificPass : public Pass { veri_file::DefineCmdLineMacro("VERIFIC"); veri_file::DefineCmdLineMacro("SYNTHESIS"); + verific_verbose = false; + const char *release_str = Message::ReleaseString(); time_t release_time = Message::ReleaseDate(); char *release_tmstr = ctime(&release_time); @@ -1581,8 +1554,8 @@ struct VerificPass : public Pass { { std::set nl_todo, nl_done; bool mode_all = false, mode_gates = false, mode_keep = false; - bool mode_nosva = false, mode_nosvapp = false, mode_names = false; - bool verbose = false, flatten = false, extnets = false; + bool mode_nosva = false, mode_names = false; + bool flatten = false, extnets = false; string dumpfile; for (argidx++; argidx < GetSize(args); argidx++) { @@ -1610,17 +1583,12 @@ struct VerificPass : public Pass { mode_nosva = true; continue; } - if (args[argidx] == "-nosvapp") { - mode_nosva = true; - mode_nosvapp = true; - continue; - } if (args[argidx] == "-n") { mode_names = true; continue; } if (args[argidx] == "-v") { - verbose = true; + verific_verbose = true; continue; } if (args[argidx] == "-d" && argidx+1 < GetSize(args)) { @@ -1697,7 +1665,6 @@ struct VerificPass : public Pass { if (extnets) { VerificExtNets worker; - worker.verbose = verbose; for (auto nl : nl_todo) worker.run(nl); } @@ -1710,7 +1677,7 @@ struct VerificPass : public Pass { while (!nl_todo.empty()) { Netlist *nl = *nl_todo.begin(); if (nl_done.count(nl) == 0) { - VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose); + VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names); importer.import_netlist(design, nl, nl_todo); } nl_todo.erase(nl); diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 4f1cb5d0f..28a0c174b 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -23,6 +23,8 @@ YOSYS_NAMESPACE_BEGIN +extern bool verific_verbose; + extern pool verific_sva_prims; struct VerificImporter; @@ -42,9 +44,9 @@ struct VerificImporter std::map net_map; std::map sva_posedge_map; - bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose; + bool mode_gates, mode_keep, mode_nosva, mode_names; - VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose); + VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names); RTLIL::SigBit net_map_at(Verific::Net *net); @@ -70,10 +72,6 @@ void import_sva_assert(VerificImporter *importer, Verific::Instance *inst); void import_sva_assume(VerificImporter *importer, Verific::Instance *inst); void import_sva_cover(VerificImporter *importer, Verific::Instance *inst); -void svapp_assert(Verific::Instance *inst); -void svapp_assume(Verific::Instance *inst); -void svapp_cover(Verific::Instance *inst); - YOSYS_NAMESPACE_END #endif 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> 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> edges; + vector accept; +}; + struct SvaFsm { Module *module; @@ -91,8 +103,11 @@ struct SvaFsm vector disable_stack; vector throughout_stack; - int startNode, acceptNode, rejectNode; - vector nodes; + int startNode, acceptNode; + vector 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 next_state_sig(GetSize(nodes)); + vector state_wire(GetSize(nodes)); vector state_sig(GetSize(nodes)); + vector 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 + // Create state FFs - if (accept_sig != State::Sz) { - module->connect(accept_sig, state_sig[acceptNode]); - } - - 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); + log(" non-deterministic encoding:\n"); + for (int i = 0; i < GetSize(nodes); i++) + { + log(" node %d:\n", i); - if (i == startNode) - log(" startNode\n"); + if (i == startNode) + log(" startNode\n"); - if (i == rejectNode) - log(" rejectNode\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; @@ -453,124 +453,6 @@ 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_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 @@ -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 (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(" 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 (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 sva_until_list_inclusive; - vector sva_until_list_exclusive; - vector*> 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 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; From 8a1d6ccf0c1b0c7e84cd160dd2572eabebcd67cc Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 28 Feb 2018 15:05:33 +0100 Subject: [PATCH 3/4] Add DFSM generator to verific SVA importer Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 291 +++++++++++++++++++++++++++++--- 1 file changed, 272 insertions(+), 19 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 5857c4496..14b989493 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -53,6 +53,7 @@ // Currently supported property styles: // not seq // seq |=> seq +// seq |=> not seq // seq |=> seq until seq // // Currently supported sequence operators: @@ -87,6 +88,22 @@ struct SvaUFsmNode // Accept: This node functions as an accept node if all bits in ctrl signal are true vector> edges; vector accept; + 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, Const>> edges; + vector accept, reject; + + // additional temp data for getReject() + Wire *ffoutwire; + SigBit statesig; + SigSpec nextstate; }; struct SvaFsm @@ -106,9 +123,6 @@ struct SvaFsm int startNode, acceptNode; vector nodes; - // ---------------------------------------------------- - // API for creating FSM - SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1) { module = mod; @@ -212,7 +226,7 @@ struct SvaFsm } // ---------------------------------------------------- - // API for generating NFSM circuit to acquire accept signal + // Generating NFSM circuit to acquire accept signal SigBit getAccept() { @@ -313,7 +327,7 @@ struct SvaFsm } // ---------------------------------------------------- - // API for generating quantifier-based NFSM circuit to acquire reject signal + // Generating quantifier-based NFSM circuit to acquire reject signal SigBit getAnyAllRejectWorker(bool allMode) { @@ -332,14 +346,206 @@ struct SvaFsm } // ---------------------------------------------------- - // API for generating DFSM circuit to acquire reject signal + // Generating DFSM circuit to acquire reject signal - SigBit getReject() + vector unodes; + dict, SvaDFsmNode> dnodes; + + void node_to_unode(int node, int unode, SigSpec ctrl) { - // FIXME - log("-----------------\n"); - dump(); - log_abort(); + if (node == acceptNode) + unodes[unode].accept.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 &vec) + { + vector 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 &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 &state, bool firstmatch) + { + 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); + } + + dnode.ctrl.sort_and_unify(); + + if (GetSize(dnode.ctrl) > 10) + log_error("SVA property DFSM state ctrl signal has over 10 bits. Stopping to prevent exponential design size explosion.\n"); + + for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++) + { + Const ctrl_val(i, GetSize(dnode.ctrl)); + pool ctrl_bits; + + for (int i = 0; i < GetSize(dnode.ctrl); i++) + if (ctrl_val[i] == State::S1) + ctrl_bits.insert(dnode.ctrl[i]); + + vector new_state; + bool accept = false; + + for (int unode : state) + for (auto &it : unodes[unode].accept) + if (cmp_ctrl(ctrl_bits, it)) + accept = true; + + if (!accept || !firstmatch) { + for (int unode : state) + for (auto &it : unodes[unode].edges) + if (cmp_ctrl(ctrl_bits, it.second)) + new_state.push_back(it.first); + } + + if (accept) + dnode.accept.push_back(ctrl_val); + + 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); + } + } + + dnodes[state] = dnode; + } + + SigBit getReject(SigBit *accept_sigptr = nullptr) + { + // 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{startNode}, true); + 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.ffoutwire->attributes["\\init"] = Const(0, 1); + dnode.statesig = dnode.ffoutwire; + + if (it.first == vector{startNode}) + dnode.statesig = module->Or(NEW_ID, dnode.statesig, trigger_sig); + } + + for (auto &it : dnodes) + { + SvaDFsmNode &dnode = it.second; + + for (auto &edge : dnode.edges) { + SigBit trig = module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {edge.second, State::S1}); + dnodes.at(edge.first).nextstate.append(trig); + } + + if (accept_sigptr) { + for (auto &value : dnode.accept) + accept_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1})); + } + + for (auto &value : dnode.reject) + reject_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1})); + } + + 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) { + module->addDff(NEW_ID, clock, dnode.nextstate, dnode.ffoutwire, clockpol); + } else { + SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate); + module->addDff(NEW_ID, clock, nextstate, dnode.ffoutwire, clockpol); + } + } + + if (accept_sigptr) + { + if (GetSize(reject_sig) == 0) + *accept_sigptr = State::S0; + else if (GetSize(reject_sig) == 1) + *accept_sigptr = reject_sig; + else + *accept_sigptr = module->ReduceOr(NEW_ID, reject_sig); + } + + if (GetSize(reject_sig) == 0) + return State::S0; + + if (GetSize(reject_sig) == 1) + return reject_sig; + + return module->ReduceOr(NEW_ID, reject_sig); } // ---------------------------------------------------- @@ -352,13 +558,7 @@ struct SvaFsm log(" non-deterministic encoding:\n"); for (int i = 0; i < GetSize(nodes); i++) { - log(" node %d:\n", i); - - if (i == startNode) - log(" startNode\n"); - - if (i == acceptNode) - log(" acceptNode\n"); + log(" node %d:%s\n", i, i == startNode ? " [start]" : i == acceptNode ? " [accept]" : ""); for (auto &it : nodes[i].edges) { if (it.second != State::S1) @@ -375,6 +575,59 @@ struct SvaFsm } } } + + if (!unodes.empty()) + { + 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(" egde %s -> %d\n", log_signal(it.second), it.first); + else + log(" egde -> %d\n", it.first); + } + + for (auto &ctrl : unodes[i].accept) { + if (!ctrl.empty()) + log(" accept %s\n", log_signal(ctrl)); + else + log(" accept\n"); + } + } + } + + if (!dnodes.empty()) + { + 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)); + } + } } }; @@ -682,7 +935,7 @@ struct VerificSvaImporter if (verific_verbose) { log(" Consequent FSM:\n"); - antecedent_fsm.dump(); + consequent_fsm.dump(); } } else From 5ac3ee858a35bf4dd20c02a3cfcd9c0e23db9ecc Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 28 Feb 2018 15:32:17 +0100 Subject: [PATCH 4/4] Add support for PRIM_SVA_UNTIL to new SVA importer Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 14b989493..2185e4596 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -922,6 +922,33 @@ struct VerificSvaImporter consequent_net = consequent_inst->GetInput(); } + 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)) + { + bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH; + consequent_net = consequent_inst->GetInput1(); + Net *until_net = consequent_inst->GetInput2(); + + SvaFsm until_fsm(module, clock, clockpol, disable_iff); + node = parse_sequence(&until_fsm, until_fsm.startNode, until_net); + if (until_with) { + int next_node = until_fsm.createNode(); + until_fsm.createEdge(node, next_node); + node = next_node; + } + until_fsm.createLink(node, until_fsm.acceptNode); + + SigBit until_match = until_fsm.getAccept(); + SigBit not_until_match = module->Not(NEW_ID, until_match); + + Wire *extend_antecedent_match_q = module->addWire(NEW_ID); + extend_antecedent_match_q->attributes["\\init"] = Const(0, 1); + antecedent_match = module->Or(NEW_ID, antecedent_match, extend_antecedent_match_q); + + SigBit extend_antecedent_match = module->And(NEW_ID, not_until_match, antecedent_match); + module->addDff(NEW_ID, clock, extend_antecedent_match, extend_antecedent_match_q, clockpol); + } + 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);