diff options
| -rw-r--r-- | frontends/verific/verific.cc | 8 | ||||
| -rw-r--r-- | frontends/verific/verific.h | 1 | ||||
| -rw-r--r-- | frontends/verific/verificsva.cc | 12 | ||||
| -rw-r--r-- | tests/sva/nested_clk_else.sv | 11 |
4 files changed, 27 insertions, 5 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index d19d837ff..4eb66851d 100644 --- 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 416b26396..695c04f3b 100644 --- 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 1bbdcf016..12bac2a3d 100644 --- 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 index 000000000..4421cb36a --- /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 |