galls2 / OMG

Implementation of the OMG model checker
3 stars 0 forks source link

Handling Latch initialization #42

Closed galls2 closed 5 years ago

galls2 commented 5 years ago

According to the new AIGER format, latches are not necessarily initialized to zero. See this (section 1) for an explanation.

This results in bug in the files (may be more): tstrst.aig rrobin.aig

swap (1st) ChandyMisra fifteen
blackjack

It should be solved by some AVY command (or some python script).

galls2 commented 5 years ago

Handled in #45