TC: Small: Collaborative Research: Trustworthy Hardware from Certified Behavioral Synthesis

University Of Texas At Austin, Austin TX

Investigators

Abstract

Electronic System Level (ESL) designs, specified behaviorally using high-level languages such as SystemC, raise the level of hardware design abstraction. This approach crucially depends on behavioral synthesis, which compiles ESL designs to Register Transfer Level (RTL) designs. However, optimizations performed by synthesis tools make their implementation error-prone, undermining the trustworthiness of synthesized hardware. This research develops a mechanized infrastructure for certifying hardware designs generated by behavioral synthesis. It entails developing a certified "reference flow" of synthesis transformations. The reference flow is disentangled from the workings of a production synthesis tool through new formal structure called "clocked control data flow graph" (CCDFG) formalizing internal design representation. Given an ESL design and its synthesized RTL, certification entails the following automatic steps: (1) extracting initial CCDFG; (2) applying certified "primitive transformations" from the reference flow, following the application sequence by the synthesis tool, and (3) checking equivalence between the transformed CCDFG and RTL. Theorem proving is used to certify primitive transformations off-line; equivalence checking accounts for low-level transformations and manual tweaks. The correspondence between the transformed CCDFG and the synthesized hardware makes equivalence checking efficient. The project facilitates development of scalable and trustworthy hardware: adoption of ESL approach expedites design cycle while formal analysis guarantees trust in the synthesized hardware. The reference flow makes explicit key design invariants implicitly assumed by synthesis tools, facilitating development of more aggressive synthesis tools. Finally, the tight integration of two complementary techniques --- model checking and theorem proving --- in the certification is applicable to other domains.