Add VerificClocking class and refactor Verific DFF handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index b7c99e4a3d1ecdf9ab1960e1e9877ed1e25869b6..2e669dc45d20a48b76d00028b2a6842cec69c46b 100644 (file)
--- 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();
+
+               inst = net->Driver();
 
-               Instance *driver = clock_net->Driver();
-               if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) {
-                       clock_net = driver->GetInput();
-                       posedge = false;
+               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 2ca01072fbc4847bd9ce8af58a621054a9f3490c..63d81fc3e154d6bb2f60e0e9d39e8730932f7a09 100644 (file)
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -29,11 +29,22 @@ extern pool<int> 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 05d5b6577e53d6fd94b80447259f35c4cdbff9e9..801f61cb7ae3625ed87061c2de3a7e2eec387f12 100644 (file)
--- 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<int>{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
-
-               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
+               clocking = VerificClocking(importer, root->GetInput());
 
-               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