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.
if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
break;
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)
- 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();
if (!verific_is_sva_net(importer, sva_net))
break;
body_net = sva_net;
cond_net = inst_mux->GetControl();
} while (0);
clock_net = net;
} while (0);
clock_net = net;
SigBit disable_sig = State::S0;
bool posedge = true;
bool gclk = false;
SigBit disable_sig = State::S0;
bool posedge = true;
bool gclk = false;
VerificClocking() { }
VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
VerificClocking() { }
VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
if (inst == nullptr)
return false;
if (inst == nullptr)
return false;
- if (clocking.cond_net != nullptr)
+ if (clocking.cond_net != nullptr) {
trig = importer->net_map_at(clocking.cond_net);
trig = importer->net_map_at(clocking.cond_net);
+ if (!clocking.cond_pol)
+ trig = module->Not(NEW_ID, trig);
+ } else {
if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
{
if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
{
- if (clocking.cond_net != nullptr)
+ if (clocking.cond_net != nullptr) {
trig = importer->net_map_at(clocking.cond_net);
trig = importer->net_map_at(clocking.cond_net);
+ if (!clocking.cond_pol)
+ trig = module->Not(NEW_ID, trig);
+ }
--- /dev/null
+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