Coq meets CλaSH: proposing a hardware design synthesis flow that combines proof assistants with functional hardware description languages

Abstract

Over the last few decades, electronic circuits have more and more become a part of our lives, and their area of application expands continuously. As a result, these circuits are getting more and more complex through these areas of application. They are synthesized from hardware designs, which describe their functional and timing behavior at a higher level of abstraction. Since safety-critical systems such as cars rely on these designs, it is essential to address the increasing complexity as it directly impacts the design’s correctness. This dissertation investigates the increasing complexity of hardware designs by proposing and evaluating a hardware design synthesis flow that automatically propagates verification results from a formal specification to an implementation. A model at the Electronic System Level (ESL) is automatically extracted from a specification at the Formal Specification Level (FSL), and this model is synthesized into an implementation at the Register-Transfer Level (RTL). This automatic propagation contrasts with the established hardware design flow, which relies on manual realizations at the ESL and RTL levels. Due to the missing propagation of verification results, these manual realizations rely on the required test benches’ quality. Consequently, similar verifi- cation tasks are repeated at different levels. The proposed synthesis flow combines the proof assistant Coq with the functional hardware description language CλaSH to achieve the automatic propagation of verification results. This combination avoids test bench generation for the model and the implementation. Furthermore, the proposed flow allows the investigation of problems in the model or the implementation already at the FSL level, e.g., arithmetic overflows for finite integer types. The established hardware design flow models infinite integer types at the FSL level, which do not realize an overflow behavior. To specify finite integer types at the FSL level, dependent types are used. Based on these types, a generalizable overflow detection scheme is presented to detect arbitrary arithmetic overflows. The scheme’s impact on the final implementation’s performance and consumed space is evaluated by comparing implementations that realize operations using this scheme with those that do not. To investigate the general implementation’s performance synthesized by the pro- posed flow, a 32-bit MIPS processor is formally specified and verified. Its final implementation is compared with a functional equivalent processor synthesized by a state- of-the-art hardware acceleration framework. This comparison shows the proposed synthesis flows’ potential and opens the door for further research on synthesizing hardware implementations that satisfy correctness properties and take performance Over the last few decades, electronic circuits have more and more become a part of our lives, and their area of application expands continuously. As a result, these circuits are getting more and more complex through these areas of application. They are synthesized from hardware designs, which describe their functional and timing behavior at a higher level of abstraction. Since safety-critical systems such as cars rely on these designs, it is essential to address the increasing complexity as it directly impacts the design’s correctness. This dissertation investigates the increasing complexity of hardware designs by proposing and evaluating a hardware design synthesis flow that automatically propa- gates verification results from a formal specification to an implementation. A model at the Electronic System Level (ESL) is automatically extracted from a specification at the Formal Specification Level (FSL), and this model is synthesized into an implemen- tation at the Register-Transfer Level (RTL). This automatic propagation contrasts with the established hardware design flow, which relies on manual realizations at the ESL and RTL levels. Due to the missing propagation of verification results, these manual realizations rely on the required test benches’ quality. Consequently, similar verifi- cation tasks are repeated at different levels. The proposed synthesis flow combines the proof assistant Coq with the functional hardware description language CλaSH to achieve the automatic propagation of verification results. This combination avoids test bench generation for the model and the implementation. Furthermore, the proposed flow allows the investigation of problems in the model or the implementation already at the FSL level, e.g., arithmetic overflows for finite integer types. The established hardware design flow models infinite integer types at the FSL level, which do not realize an overflow behavior. To specify finite integer types at the FSL level, dependent types are used. Based on these types, a generalizable overflow detection scheme is presented to detect arbitrary arithmetic overflows. The scheme’s impact on the final implementation’s performance and consumed space is evaluated by comparing implementations that realize operations using this scheme with those that do not. To investigate the general implementation’s performance synthesized by the pro- posed flow, a 32-bit MIPS processor is formally specified and verified. Its final imple- mentation is compared with a functional equivalent processor synthesized by a state- of-the-art hardware acceleration framework. This comparison shows the proposed synthesis flows’ potential and opens the door for further research on synthesizing hardware implementations that satisfy correctness properties and take performance under consideration.