SAT Verification

[renau]

extend ezSAT and interface with lgraph to
-check equivalence of lgraphs
-Reduce port in SRAMs
-Check parallel cases in muxes

PAPER:
-Use the net names from incremental synthesis to partition design (if partition verifies, we are done)
-Use structural traversal to remove search space (from inputs/outputs)
-Use parallel SAT checks (each output cone, partition of cones, after synth)
-Mark "boundaries" for equivalence in lgraph. Faster synthesis, verification...
-Different SAT solvers in parallel (ezsat, CVC4, SPT) and pick fastest

Maybe use https://github.com/Boolector/boolector