Combining Software and Hardware Verification Techniques

Combining verification methods developed separately for software and hardware is motivated by the industry's need for a technology that would make formal verification of realistic software/hardware co-designs practical. We focus on techniques that have proved successful in each of the two domains: BDD-based symbolic model checking for hardware verification and partial order reduction for the verification of concurrent software programs. In this paper, we first suggest a modification of partial order reduction, allowing its combination with any BDD-based verification tool, and then describe a co-verification methodology developed using these techniques jointly. Our experimental results demonstrate the efficiency of this combined verification technique, and suggest that for moderate

• Type: Journal
• Year: 2002
• Where: FMSD
• Authors: Robert P. Kurshan, Vladimir Levin, Marius Minea, Doron Peled, Hüsnü Yenigün
• Keywords: FMSD 2002, Formal Verification, Partial Order Reduction, Verification Methods