Wille, Robert

Due to the ever increasing complexity of hardware and hardware/software co-designs, developers strive for higher levels of abstractions in the early stages of the design flow. To address these demands, design at the Electronic System Level (ESL) has been introduced. SystemC currently is the "de-facto standard" for ESL design. The extraction of data from system designs written in SystemC is thereby crucial e.g. for the proper understanding of a given system. However, no satisfactory support of reflection/introspection of SystemC has been provided yet. Previously proposed methods for this purpose %introduced to achieve the goal nonetheless either focus on static aspects only, restrict the language means of SystemC, or rely on modifications of the compiler and/or parser. In this thesis, approaches that overcome these limitations are introduced, allowing the extraction of information from a given SystemC design without changing the SystemC library or the compiler. The proposed approaches retrieve both, static and dynamic (i.e. run-time) information.

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.

Wille, Robert

Filter

Einstellungen

Sortieren nach

Ergebnisse pro Seite