EverLost

EverLost is our platform for industrial-strength abstraction-guided simulation. EverLost takes an RTL Verilog design and preimage/abstraction information from any BDD-based abstraction/model-checking tool, and automatically generates code that implements abstraction-guided simulation and directly compiles with the design under the widely-used Synopsys VCS simulator. The platform enables flexible exploration of abstraction-guided simulation --- different formal tools and guidance heuristics are easily inserted --- while providing the capacity, speed, and Verilog compatibility of a leading industry-standard tool.

EverLost Benchmarks

This is a set of examples used in our DAC007 paper that are compatible w/ the following formal verification tools:

VCEGAR-based benchmark (Last updated on Jun-05-2007)

VIS-based benchmark (Last updated on Jun-05-2007)