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 .
This research develops a mechanized infrastructure for certifying hardware designs generated by behavioral synthesis. The work 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 the semantics of the internal representation of a hardware design during the synthesis process. Given an Electronic System Level (ESL) design and its synthesized Register Transfer Level (RTL) implementation, certification of a behavioral synthesis flow entails the following automatic steps: (1) extracting the initial CCDFG from the high-level description; (2) applying certified sequence of 'primitive transformations' from the reference flow (which follow the application sequence by the synthesis tool), and (3) checking sequential 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. By ensuring correct-by-construction hardware from behavioral synthesis, our framework obviates expensive case-by-case analysis of an RTL or netlist design. This permits the designer to focus on high-level behavioral properties. Our framework is independent of the internal workings of a specific synthesis tool, and can thus be applied to certify hardware designs synthesized by different tools from a broad class of ESL descriptions. This makes our approach particularly suitable for certifying security-critical hardware designs (which are often synthesized from domain-specific high-level languages). Our approach produces a certified reference flow, which identifies and makes explicit generic invariants that must be preserved by different behavioral synthesis transformations. This reference flow thereby provides a careful, formal specification for reliable, aggressive synthesis tools.
