TY - GEN
T1 - Towards Automatic Hardware Synthesis from Formal Specification to Implementation
AU - Bornebusch, Fritjof
AU - Luth, Christoph
AU - Wille, Robert
AU - Drechsler, Rolf
N1 - Publisher Copyright:
© 2020 IEEE.
PY - 2020/1
Y1 - 2020/1
N2 - 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 test benches 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.
AB - 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 test benches 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.
UR - http://www.scopus.com/inward/record.url?scp=85082987611&partnerID=8YFLogxK
U2 - 10.1109/ASP-DAC47756.2020.9045406
DO - 10.1109/ASP-DAC47756.2020.9045406
M3 - Conference contribution
AN - SCOPUS:85082987611
T3 - Proceedings of the Asia and South Pacific Design Automation Conference, ASP-DAC
SP - 375
EP - 380
BT - ASP-DAC 2020 - 25th Asia and South Pacific Design Automation Conference, Proceedings
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 25th Asia and South Pacific Design Automation Conference, ASP-DAC 2020
Y2 - 13 January 2020 through 16 January 2020
ER -