A Toolbox For Property Checking From Simulation Using Incremental SAT (Extended Abstract)
This addresses verification challenges for hardware designers, but appears incremental as it builds on existing incremental SAT methods.
The paper presents a tool for checking bounded properties in hardware designs starting from simulation runs, using incremental SAT solving with clause addition and simplification. It demonstrates the approach on some Verilog RTL examples.
We present a tool that primarily supports the ability to check bounded properties starting from a sequence of states in a run. The target design is compiled into an AIGNET which is then selectively and iteratively translated into an incremental SAT instance in which clauses are added for new terms and simplified by the assignment of existing literals. Additional applications of the tool can be derived by the user providing alternative attachments of constrained functions which guide the iterations and SAT checks performed. Some Verilog RTL examples are included for reference.