mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 03:32:29 +00:00
Code Activity

verific: Fix conditions of SVAs with explicit clocks within procedures

Browse source 
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.
This commit is contained in:
Jannis Harder 2022-05-03 13:22:18 +02:00
parent 11e75bc27c
commit 96f64f4788
4 changed files with 27 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

8
frontends/verific/verific.cc
View file

@ -1873,15 +1873,19 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX) if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
break; break;
if (!inst_mux->GetInput1()->IsPwr()) bool pwr1 = inst_mux->GetInput1()->IsPwr();
bool pwr2 = inst_mux->GetInput2()->IsPwr();
if (!pwr1 && !pwr2)
break; 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)) if (!verific_is_sva_net(importer, sva_net))
break; break;
body_net = sva_net; body_net = sva_net;
cond_net = inst_mux->GetControl(); cond_net = inst_mux->GetControl();
cond_pol = pwr1;
} while (0); } while (0);
clock_net = net; clock_net = net;

1
frontends/verific/verific.h
View file

@ -44,6 +44,7 @@ struct VerificClocking {
SigBit disable_sig = State::S0; SigBit disable_sig = State::S0;
bool posedge = true; bool posedge = true;
bool gclk = false; bool gclk = false;
bool cond_pol = true;
VerificClocking() { } VerificClocking() { }
VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false); VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);

12
frontends/verific/verificsva.cc
View file

@ -1522,10 +1522,13 @@ struct VerificSvaImporter
if (inst == nullptr) if (inst == nullptr)
return false; 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);
else if (!clocking.cond_pol)
trig = module->Not(NEW_ID, trig);
} else {
trig = State::S1; trig = State::S1;
}
if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY) if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
{ {
@ -1587,8 +1590,11 @@ struct VerificSvaImporter
SigBit trig = State::S1; SigBit trig = State::S1;
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);
}
if (inst == nullptr) if (inst == nullptr)
{ {

11
tests/sva/nested_clk_else.sv Normal file
View file

@ -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