GaloisInc / jvm-verifier

The Java Symbolic Simulator, part of SAW.
BSD 3-Clause "New" or "Revised" License
10 stars 2 forks source link

AIG generation depends on backend #1

Open robdockins opened 9 years ago

robdockins commented 9 years ago

Using the word backend results in different AIG output than the SAW backend. This is related, I believe, to different assumptions regarding bit-order; the word backend operates least-significant-bit-first, but the SAW backend conforms to the Cryptol 2 semantics, which is most-significant-bit-first.

There may be other related issues where bit-ordering assumptions affect the results; these should also be teased out.