IODINE: a tool to automatically infer dynamic invariants for hardware designs

We describe IODINE, a tool to automatically extract likely design properties using dynamic analysis. A practical bottleneck in the formal verification of hardware designs is the need to manually specify design-specific properties. IODINE presents a way to automatically extract properties such as state machine protocols, request-acknowledge pairs, and mutual exclusion between signals from design simulations. We show that dynamic invariant detection for hardware designs can infer relevant and accurate properties. Categories and Subject Descriptors: B.5.2 Hardware Register-Transfer-Level Implementation Verification F.3.1 Theory of Computation Logics and Meanings of Programs Invariants General Terms: Verification, Algorithms

• Type: Conference
• Year: 2005
• Where: DAC
• Authors: Sudheendra Hangal, Naveen Chandra, Sridhar Narayanan, Sandeep Chakravorty
• Keywords: DAC 2005, Design Automation, Dynamic Invariant Detection, Likely Design Properties, Register-Transfer-Level Implementation Verification