verific: Fix conditions of SVAs with explicit clocks within procedures

[yosys.git] / frontends / verific / verific.cc

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index d19d837ffcca33316b8271ffb1d664c32ad06f36..4eb66851d0421e7d852396be96aa1ee6f18bcfa4 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1873,15 +1873,19 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
                if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
                        break;
 
-               if (!inst_mux->GetInput1()->IsPwr())
+               bool pwr1 = inst_mux->GetInput1()->IsPwr();
+               bool pwr2 = inst_mux->GetInput2()->IsPwr();
+
+               if (!pwr1 && !pwr2)
                        break;
 
-               Net *sva_net = inst_mux->GetInput2();
+               Net *sva_net = pwr1 ? inst_mux->GetInput2() : inst_mux->GetInput1();
                if (!verific_is_sva_net(importer, sva_net))
                        break;
 
                body_net = sva_net;
                cond_net = inst_mux->GetControl();
+               cond_pol = pwr1;
        } while (0);
 
        clock_net = net;