4 ms·
is this formally verified? I'm not sure whats going on but from a quick glance its just comparing the output of two implementations?
by easytiger 13y ago
is this formally verified? I'm not sure whats going on but from a quick glance its just comparing the output of two implementations?
- panic 13y agoInstead of brute force, it looks like it's comparing automatically-generated models of the two implementations symbolically. Success! Amazingly, this proof systems scales to large values of n where exhaustive checking is not feasible: $ time make n=1000 Proving function equivalent to reference: encode_aig : [1000][8] -> [1336][8] Q.E.D. real: 17.882s user: 16.31s cpu: 1.50s*
- pjscott 13y agoModern SMT solvers are astonishingly fast for most real-world inputs. Not bad, considering that the problem they solve is NP-complete!
- dons 13y agoIt's doing symbolic equivalence checking via an SMT solver, iirc.