Lecture Notes in Computer Science, 1994, Volume 818/1994, 182-193, DOI: 10.1007/3-540-58179-0_53

Methodology and system for practical formal verification of reactive hardware

Ilan Beer, Shoham Ben-David, Daniel Geist, Raanan Gewirtzman and Michael Yoeli

View Related Documents

Abstract

Making formal verification a practicality in industrial environments is still difficult. The capacity of most verification tools is too small, their integration in a design process is difficult and the methodology that should guide their usage is unclear.
This paper describes a step-by-step methodology which was developed for the practical application of formal verification. The methodology was successfully realized in a production environment of hardware design. The realization involved the development of a system consisting of several tools, while using the SMV [McM93] verification tool as the system core.
This system was used in the verification of eight designs. We specifically elaborate on the verification of a bus-bridge design, which was particularly successful in uncovering and eliminating many hardware design errors.

Fulltext Preview

Image of the first page of the fulltext document