Combining Software and Hardware Verification Techniques |
| |
Authors: | Robert P. Kurshan Vladimir Levin Marius Minea Doron Peled Hüsnü Yenigün |
| |
Affiliation: | (1) Bell Laboratories, Lucent Technologies, Murray Hill, NJ 07974, USA;(2) Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213, USA |
| |
Abstract: | 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–size systems the method is ready for industrial application. |
| |
Keywords: | formal verification model checking hardware/software co-design partial order reduction |
本文献已被 SpringerLink 等数据库收录! |
|