From 261cf706f4d8eb1bcb3d9e6915930667073fdbe6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 4 Mar 2018 13:48:53 +0100 Subject: [PATCH] Add VerificClocking class and refactor Verific DFF handling Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 203 +++++++++++++++++++++++++------- frontends/verific/verific.h | 17 ++- frontends/verific/verificsva.cc | 104 ++++------------ 3 files changed, 197 insertions(+), 127 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index b7c99e4a3..2e669dc45 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -277,16 +277,18 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr if (inst->Type() == PRIM_DFFRS) { + VerificClocking clocking(this, inst->GetClock()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); else if (inst->GetSet()->IsGnd()) - module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), - net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false); + clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S0); else if (inst->GetReset()->IsGnd()) - module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), - net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true); + clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S1); else - module->addDffsrGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), + clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } @@ -358,16 +360,18 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr if (inst->Type() == PRIM_DFFRS) { + VerificClocking clocking(this, inst->GetClock()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); + if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); else if (inst->GetSet()->IsGnd()) - module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), - net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0); + clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0); else if (inst->GetReset()->IsGnd()) - module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), - net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1); + clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1); else - module->addDffsr(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), + clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } @@ -594,13 +598,20 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr return true; } - if (inst->Type() == OPER_WIDE_DFFRS) { + if (inst->Type() == OPER_WIDE_DFFRS) + { + VerificClocking clocking(this, inst->GetClock()); + log_assert(clocking.disable_sig == State::S0); + log_assert(clocking.body_net == nullptr); + RTLIL::SigSpec sig_set = operatorInport(inst, "set"); RTLIL::SigSpec sig_reset = operatorInport(inst, "reset"); + if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool()) - module->addDff(inst_name, net_map_at(inst->GetClock()), IN, OUT); + clocking.addDff(inst_name, IN, OUT); else - module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT); + clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT); + return true; } @@ -1097,7 +1108,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == OPER_SVA_STABLE) { - VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver()); + VerificClocking clocking(this, inst->GetInput2Bit(0)); log_assert(inst->Input1Size() == inst->OutputSize()); @@ -1110,13 +1121,13 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se } 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(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); } - module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); + clocking.addDff(NEW_ID, sig_d, sig_q); module->addXnor(NEW_ID, sig_d, sig_q, sig_o); if (!mode_keep) @@ -1125,20 +1136,20 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == PRIM_SVA_STABLE) { - VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); + VerificClocking clocking(this, inst->GetInput2()); SigSpec sig_d = net_map_at(inst->GetInput1()); SigSpec sig_o = net_map_at(inst->GetOutput()); SigSpec sig_q = module->addWire(NEW_ID); 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(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); } - module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); + clocking.addDff(NEW_ID, sig_d, sig_q); module->addXnor(NEW_ID, sig_d, sig_q, sig_o); if (!mode_keep) @@ -1147,16 +1158,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == PRIM_SVA_PAST) { - VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); + VerificClocking clocking(this, inst->GetInput2()); SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_q = net_map_at(inst->GetOutput()); 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(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); - past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge)); + past_ffs.insert(clocking.addDff(NEW_ID, sig_d, sig_q)); if (!mode_keep) continue; @@ -1164,17 +1175,17 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL)) { - VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); + VerificClocking clocking(this, inst->GetInput2()); SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_o = net_map_at(inst->GetOutput()); SigBit sig_q = module->addWire(NEW_ID); 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(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg", + log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig)); - module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); + clocking.addDff(NEW_ID, sig_d, sig_q); module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o); if (!mode_keep) @@ -1259,26 +1270,130 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se // ================================================================== -VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) +VerificClocking::VerificClocking(VerificImporter *importer, Net *net) { + module = importer->module; + log_assert(importer != nullptr); - log_assert(inst != nullptr); + log_assert(net != nullptr); - // SVA posedge/negedge - if (inst->Type() == PRIM_SVA_POSEDGE) + Instance *inst = net->Driver(); + + if (inst != nullptr && inst->Type() == PRIM_SVA_AT) { - clock_net = inst->GetInput(); - posedge = true; + net = inst->GetInput1(); + body_net = inst->GetInput2(); - Instance *driver = clock_net->Driver(); - if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) { - clock_net = driver->GetInput(); - posedge = false; + inst = net->Driver(); + + Instance *body_inst = body_net->Driver(); + if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) { + disable_net = body_inst->GetInput1(); + disable_sig = importer->net_map_at(disable_net); + body_net = body_inst->GetInput2(); } - - clock_sig = importer->net_map_at(clock_net); - return; } + + if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE) + { + net = inst->GetInput(); + inst = net->Driver();; + } + + if (inst != nullptr && inst->Type() == PRIM_INV) + { + net = inst->GetInput(); + inst = net->Driver();; + posedge = false; + } + + // Detect clock-enable circuit + do { + if (inst == nullptr || inst->Type() != PRIM_AND) + break; + + Net *net_dlatch = inst->GetInput1(); + Instance *inst_dlatch = net_dlatch->Driver(); + + if (inst_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS) + break; + + if (!inst_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd()) + break; + + Net *net_enable = inst_dlatch->GetInput(); + Net *net_not_clock = inst_dlatch->GetControl(); + + if (net_enable == nullptr || net_not_clock == nullptr) + break; + + Instance *inst_not_clock = net_not_clock->Driver(); + + if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV) + break; + + Net *net_clock1 = inst_not_clock->GetInput(); + Net *net_clock2 = inst->GetInput2(); + + if (net_clock1 == nullptr || net_clock1 != net_clock2) + break; + + enable_net = net_enable; + enable_sig = importer->net_map_at(enable_net); + + net = net_clock1; + inst = net->Driver();; + } while (0); + + clock_net = net; + clock_sig = importer->net_map_at(clock_net); +} + +Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value) +{ + log_assert(GetSize(sig_d) == GetSize(sig_q)); + + if (GetSize(init_value) != 0) { + log_assert(GetSize(sig_q) == GetSize(init_value)); + if (sig_q.is_wire()) { + sig_q.as_wire()->attributes["\\init"] = init_value; + } else { + Wire *w = module->addWire(NEW_ID, GetSize(sig_q)); + w->attributes["\\init"] = init_value; + module->connect(sig_q, w); + sig_q = w; + } + } + + if (enable_sig != State::S1) + sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig); + + if (disable_sig != State::S0) { + log_assert(GetSize(sig_q) == GetSize(init_value)); + return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge); + } + + return module->addDff(name, clock_sig, sig_d, sig_q, posedge); +} + +Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value) +{ + log_assert(disable_sig == State::S0); + + if (enable_sig != State::S1) + sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig); + + return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge); +} + +Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q) +{ + log_assert(disable_sig == State::S0); + + if (enable_sig != State::S1) + sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig); + + return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge); } // ================================================================== diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 2ca01072f..63d81fc3e 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -29,11 +29,22 @@ extern pool verific_sva_prims; struct VerificImporter; -struct VerificClockEdge { +struct VerificClocking { + RTLIL::Module *module = nullptr; Verific::Net *clock_net = nullptr; + Verific::Net *enable_net = nullptr; + Verific::Net *disable_net = nullptr; + Verific::Net *body_net = nullptr; SigBit clock_sig = State::Sx; - bool posedge = false; - VerificClockEdge(VerificImporter *importer, Verific::Instance *inst); + SigBit enable_sig = State::S1; + SigBit disable_sig = State::S0; + bool posedge = true; + + VerificClocking() { } + VerificClocking(VerificImporter *importer, Verific::Net *net); + RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const()); + RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value); + RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q); }; struct VerificImporter diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 05d5b6577..801f61cb7 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -37,7 +37,9 @@ // 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] +// ##[N:M] includes ##N, ##[*], ##[+] +// [*N:M] includes [*N], [*], [+] +// [=N:M], [->N:M] includes [=N], [->N] // // ------------------------------------------------------- // @@ -117,8 +119,7 @@ struct SvaDFsmNode struct SvaFsm { Module *module; - SigBit clock; - bool clockpol; + VerificClocking clocking; SigBit trigger_sig = State::S1, disable_sig; SigBit throughout_sig = State::S1; @@ -133,12 +134,10 @@ struct SvaFsm SigBit final_accept_sig = State::Sx; SigBit final_reject_sig = State::Sx; - SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1) + SvaFsm(const VerificClocking &clking, SigBit trig = State::S1) { - module = mod; - clock = clk; - clockpol = clkpol; - disable_sig = dis; + module = clking.module; + clocking = clking; trigger_sig = trig; startNode = createNode(); @@ -326,8 +325,7 @@ struct SvaFsm for (int i = 0; i < GetSize(nodes); i++) { 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); + clocking.addDff(NEW_ID, next_state_sig[i], state_wire[i], Const(0, 1)); } else { module->connect(state_wire[i], State::S0); } @@ -501,7 +499,6 @@ struct SvaFsm { 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}) @@ -533,10 +530,10 @@ struct SvaFsm module->connect(dnode.ffoutwire, State::S0); } else if (GetSize(dnode.nextstate) == 1) { - module->addDff(NEW_ID, clock, dnode.nextstate, dnode.ffoutwire, clockpol); + clocking.addDff(NEW_ID, dnode.nextstate, dnode.ffoutwire, State::S0); } else { SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate); - module->addDff(NEW_ID, clock, nextstate, dnode.ffoutwire, clockpol); + clocking.addDff(NEW_ID, nextstate, dnode.ffoutwire, State::S0); } } @@ -717,16 +714,12 @@ struct VerificSvaImporter Netlist *netlist = nullptr; Instance *root = nullptr; - SigBit clock = State::Sx; - bool clockpol = false; - - SigBit disable_iff = State::S0; + VerificClocking clocking; bool mode_assert = false; bool mode_assume = false; bool mode_cover = false; bool eventually = false; - bool did_something = false; Instance *net_to_ast_driver(Net *n) { @@ -887,62 +880,16 @@ struct VerificSvaImporter RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); - // parse SVA property clock event + clocking = VerificClocking(importer, root->GetInput()); - 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; - clockpol = clock_edge.posedge; - - // parse disable_iff expression - - Net *net = at_node->GetInput2(); - - while (1) - { - Instance *sequence_node = net_to_ast_driver(net); - - if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { - eventually = true; - net = sequence_node->GetInput(); - continue; - } - - if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { - disable_iff = importer->net_map_at(sequence_node->GetInput1()); - net = sequence_node->GetInput2(); - continue; - } - - break; - } + if (clocking.body_net == nullptr) + log_error("Failed to parse SVA clocking at %s (%s) at %s:%d.", root->Name(), root->View()->Owner()->Name(), + LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); // parse SVA sequence into trigger signal SigBit prop_okay; + Net *net = clocking.body_net; Instance *inst = net_to_ast_driver(net); if (inst == nullptr) @@ -957,7 +904,7 @@ struct VerificSvaImporter Net *consequent_net = inst->GetInput2(); int node; - SvaFsm antecedent_fsm(module, clock, clockpol, disable_iff); + SvaFsm antecedent_fsm(clocking); node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { int next_node = antecedent_fsm.createNode(); @@ -996,7 +943,7 @@ struct VerificSvaImporter until_net = until_inst->GetInput(); } - SvaFsm until_fsm(module, clock, clockpol, disable_iff); + SvaFsm until_fsm(clocking); node = parse_sequence(&until_fsm, until_fsm.startNode, until_net); until_fsm.createLink(node, until_fsm.acceptNode); @@ -1008,13 +955,11 @@ struct VerificSvaImporter until_fsm.dump(); } - Wire *antecedent_match_q = module->addWire(NEW_ID); - antecedent_match_q->attributes["\\init"] = Const(0, 1); - + SigBit antecedent_match_q = module->addWire(NEW_ID); antecedent_match = module->Or(NEW_ID, antecedent_match, antecedent_match_q); SigBit antecedent_match_filtered = module->And(NEW_ID, antecedent_match, not_until_match); - module->addDff(NEW_ID, clock, antecedent_match_filtered, antecedent_match_q, clockpol); + clocking.addDff(NEW_ID, antecedent_match_filtered, antecedent_match_q, State::S0); if (!until_with) antecedent_match = antecedent_match_filtered; @@ -1027,7 +972,7 @@ struct VerificSvaImporter consequent_inst = net_to_ast_driver(consequent_net); } - SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match); + SvaFsm consequent_fsm(clocking, antecedent_match); node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net); consequent_fsm.createLink(node, consequent_fsm.acceptNode); @@ -1046,7 +991,7 @@ struct VerificSvaImporter else if (inst->Type() == PRIM_SVA_NOT || mode_cover) { - SvaFsm fsm(module, clock, clockpol, disable_iff); + SvaFsm fsm(clocking); int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput()); fsm.createLink(node, fsm.acceptNode); SigBit accept = fsm.getAccept(); @@ -1069,9 +1014,8 @@ struct VerificSvaImporter // 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, clockpol); + SigBit prop_okay_q = module->addWire(NEW_ID); + clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1)); // generate assert/assume/cover cell