- Daniel Kroening
- SMT Lists/Sets/Maps
- Google groups:
Hardware Verification
Our Hardware Verification Tools
We specialize in high-level hardware verification, that is, verification at the word-level or for transaction level modeling (TLM). Our Model Checking tools accept synthesizable Verilog or SystemC as input.
- Predicate abstraction for Verilog:
- An enhanced Bounded Model Checker:
- Formal analysis for SystemC: Scoot
Benchmarks
- Our benchmark collection for VCEGAR: vcegar-benchmarks.tgz
- We also have a collection of sequential equivalence checking benchmarks.
Relevant Publications
- Efficient Verification of Multi-Property Designs (best paper in the design track)
- Formal Techniques for Effective Co-verification of Hardware/Software Co-designs
- Equivalence Checking of a Floating-point Unit Against a High-level C Model
- Unbounded Safety Verification for Hardware Using Software Analyzers
- Hardware Verification using Software Analyzers
- Computing Mutation Coverage in Interpolation-based Model Checking
- Race Analysis for SystemC using Model Checking
- Deciding Bit-Vector Arithmetic with Abstraction
- Computational Challenges in Bounded Model Checking