Proof-aided design of verified hardware
Holger Busch, Gerd Venzl · 1991
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.