A Case-Study in Property-Based Synthesis: Generating a Cache Controller from a Property-Set

Abstract—Property-based synthesis has become a more prominent topic during the last years, being used in multiple areas like e.g. formal verification and design automation. We will show how a property-based formal specification of a cache controller for a MIPS core can be used to automatically generate a functional implementation of that controller and how additional performance information about the complete system can be gained from doing so.

• Type: Conference
• Year: 2007
• Where: FDL
• Authors: Martin Schickel, Martin Oberkönig, Martin Schweikert, Hans Eveking
• Keywords: FDL 2007, Formal Verification, Prominent Topic, Property-based Formal Specification