Publication
Towards Automatic Hardware Synthesis from Formal Specification to Implementation
Fritjof Bornebusch; Christoph Lüth; Robert Wille; Rolf Drechsler
In: 25th Asia and South Pacific Design Automation Conference (ASP-DAC). Asia and South Pacific Design Automation Conference (ASP-DAC-2020), 25th, January 13-16, Beijing, China, 2020.
Abstract
In this work, we sketch an automated design flow for hardware synthesis based on a formal specification. Verification results are propagated from the FSL level through the proposed flow to generate an ESL model as well as an RTL implementation automatically. In contrast, the established design flow relies on manual implementations at the ESL and RTL level. The proposed design flow combines proof assistants with functional hardware description languages. This combination decreases the implementation effort significantly and the generation of testbenches is no longer needed. We illustrate our design flow by specifying and synthesizing a set of benchmarks that contain sequential and combinational hardware designs. We compare them with implementations required by the established hardware design flow.