search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
379 stars 74 forks source link

Update sby_engine_abc.py #268

Closed KrystalDelusion closed 4 months ago

KrystalDelusion commented 4 months ago

ABC will sometimes return negative frame numbers when proving by convergence, e.g.

engine_0: Proved output 1 in frame -698905656 (converged).
engine_0: Proved output 4 in frame -698905656 (converged).

This change fixes these properties being missed and causing the engine status to return UNKNOWN due to proved_count != len(proved).

jix commented 4 months ago

That should be fixed in abc instead of working around it in SBY (or in addition to, the workaround itself is fine and shouldn't cause any additional issues even with it fixed in abc), can you share a project to reproduce this?