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

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.