Formal verification based on assume and guarantee approach: a case study
Subir Kumar Roy, H. Iwashita, Tsuneo Nakata · 2002
In this paper, we present a verification case study of the Audio Output Interface (AOF) subsystem based on a compositional verification approach known as the Assume-Guarantee approach. We illustrate how designers can leverage their detailed knowledge of a design to partition it at the module level, and, thereby, enable the Assume-Guarantee approach to overcome intrinsic limitations of a formal verification tool to successfully verify large designs.