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 .
TC: Small: Collaborative Research: Trustworthy Hardware from Certified Behavioral Synthesis