verific: Fix conditions of SVAs with explicit clocks within procedures

For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.

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;

diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 416b26396c84952ec0f8f7ec382bb409c609d121..695c04f3bcba3ae5451008ef8d7c196f91ff73fe 100644 (file)
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -44,6 +44,7 @@ struct VerificClocking {
        SigBit disable_sig = State::S0;
        bool posedge = true;
        bool gclk = false;
+       bool cond_pol = true;
 
        VerificClocking() { }
        VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 1bbdcf0167f061005b674b02735e0886e8064c92..12bac2a3d058b7b586b25fe7577842051a98a09a 100644 (file)
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1522,10 +1522,13 @@ struct VerificSvaImporter
                if (inst == nullptr)
                        return false;
 
-               if (clocking.cond_net != nullptr)
+               if (clocking.cond_net != nullptr) {
                        trig = importer->net_map_at(clocking.cond_net);
-               else
+                       if (!clocking.cond_pol)
+                               trig = module->Not(NEW_ID, trig);
+               } else {
                        trig = State::S1;
+               }
 
                if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
                {
@@ -1587,8 +1590,11 @@ struct VerificSvaImporter
 
                SigBit trig = State::S1;
 
-               if (clocking.cond_net != nullptr)
+               if (clocking.cond_net != nullptr) {
                        trig = importer->net_map_at(clocking.cond_net);
+                       if (!clocking.cond_pol)
+                               trig = module->Not(NEW_ID, trig);
+               }
 
                if (inst == nullptr)
                {

diff --git a/tests/sva/nested_clk_else.sv b/tests/sva/nested_clk_else.sv
new file mode 100644 (file)
index 0000000..4421cb3
--- /dev/null
+++ b/tests/sva/nested_clk_else.sv
@@ -0,0 +1,11 @@
+module top (input clk, a, b);
+       always @(posedge clk) begin
+        if (a);
+        else assume property (@(posedge clk) b);
+       end
+
+`ifndef FAIL
+    assume property (@(posedge clk) !a);
+`endif
+    assert property (@(posedge clk) b);
+endmodule