This paper describes how model checking has been integrated into an industrial hardware design process. We present an application oriented specification language for assumption/commitment style properties and an abstraction algorithm that generates an intuitive and efficient representation of synchronous circuits. These approaches are embedded in our Circuit Verification Environment CVE. They are demonstrated on two industrial applications.

A novel transformational technique for designin hardware by theorem-proving is presented. '-Jq sign aspects like parameterized retiming of sync ronous sy tems and constrained refinement are formalized in a unifor framework. We create a space of valid solutions from an abstract specification rather than a specific implementation. Our methodology has been applied to a complex VLSI design of 250,000 transistors.