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)