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
- Our benchmark collection for VCEGAR: vcegar-benchmarks.tgz
- We also have a collection of sequential equivalence checking benchmarks.
- Fixed Points in Multi-Cycle Path Detection
- Strengthening Properties using Abstraction Refinement
- Race Analysis for SystemC using Model Checking
- Deciding Bit-Vector Arithmetic with Abstraction
- Word Level Predicate Abstraction and Refinement for Verifying RTL Verilog
- Computational Challenges in Bounded Model Checking