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

点击翻译按钮获取中文摘要

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