"Accessible Formal Verification for Safety-Critical FPGA Design"
John Lach1, Scott Bingham1, Carl Elks1, Travis Lenhart1, Thuy Nguyen2, Patrick Salaun2
1University of Virginia
2Electricité de France
While safety-critical systems depend on the functionality of both software and hardware, recent efforts on the development of verification techniques have focused almost exclusively on software. While verification techniques for hardware design should certainly draw from those developed for software, inherent differences between hardware and software require new approaches. Even within hardware design, the diversity of design entry abstraction levels (behavioral level, register-transfer level (RTL), circuit/transistor level), implementation platforms (application-specific integrated circuits (ASICs), field programmable gate arrays (FPGAs), programmable logic devices (PLDs)), and design reuse options (full custom, hard and soft intellectual property (IP) blocks) require a broad exploration of verification techniques. We are developing an accessible formal-verification-based hardware design methodology for safety-critical FPGA-based systems. While some of the methodology must be grounded in formal verification techniques (e.g. model checking, equivalence checking, theorem proving), they are highly abstract and mathematical in nature and remain conceptually inaccessible to most specification and design engineers.
We are developing approaches that make formal verification more accessible to engineers so that the techniques become a natural, transparent part of the design methodology. Therefore, the people who specify and design the hardware will be the same people who ensure its safety. In addition, the methodology must be general enough to account for the various abstraction levels and design reuse options in FPGA design. The core element of this methodology is a verified library of operations and components (at various levels of abstraction) from which designers can specify their designs.
2005 MAPLD International Conference Home Page