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.


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.


towards_automatic_hardware_synthesis_from_formal_specification_to_implementation.pdf (pdf, 569 KB )

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz