projects
/
yosys.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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 == 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;
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();
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;
} while (0);
clock_net = net;