@User @User @User @User @User @User Performance Aspects of Correctness-oriented Synthesis Flows https://user.informatik.uni-bremen.de/fritjof/pdfs/performance-aspects-of-correctness-oriented-synthesis-flows.pdf Fritjof Bornebusch1 , Christoph L¨uth1,2 , Robert Wille1,3,4 , Rolf Drechsler1,2 1 Cyber-Physical Systems, DFKI GmbH, Bremen, Germany 2 Mathematics and Computer Science, University of Bremen, Germany 3 Integrated Circuit and System Design, Johannes Kepler University Linz, Austria 4 Software Competence Center Hagenberg GmbH (SCCH), Hagenberg, Austria {fritjof.bornebusch,christoph.lueth}@dfki.de, robert.wille@jku.at, drechsler@uni-bremen.de Keywords: Hardware Designs, Proof Assistants, Functional HDLs, Hardware Synthesis, MIPS processor Abstract: When designing electronic circuits, available synthesis flows either focus on accelerating the synthesized circuit or correctness. In the quest for ever-faster hardware designs, the correctness of these designs is often neglected. Thus, designers need to trade-off between correctness and performance. The question is how large the trade-off is? This work presents a systematic comparison of two representative synthesis flows, the LegUp HLS framework as a representative for flows focusing on hardware acceleration, and a flow based on the proof assistant Coq focusing on correctness. For evaluation purposes, a 32-bit MIPS processor synthesized using the two flows, and the final HDL implementations are compared regarding their performance. Our evaluation allows a quantitative analysis of the trade-off, showing that correctness-oriented synthesis flows are competitive concerning performance.