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

电子系统级(ESL)设计，使用高级语言(如SystemC)指定的行为，提高了硬件设计抽象的级别。这一方法关键依赖于行为综合，它将ESL设计编译为寄存器传输级(RTL)设计。然而，由合成工具执行的优化使得它们的实现容易出错，破坏了合成硬件的可信性。这项研究开发了一个机械化的基础设施，用于验证由行为综合生成的硬件设计。它需要开发一个经过认证的合成转换的“参考流程”。参考流程通过一种新的形式化结构“时钟控制数据流图”(CCDFG)从产品综合工具的工作中分离出来，CCDFG用于形式化内部设计表示。在给定ESL设计及其综合RTL的情况下，验证需要以下自动步骤：(1)提取初始CCDFG；(2)根据综合工具的应用顺序，从参考流中应用经证明的“原语变换”；以及(3)检查变换后的CCDFG和RTL之间的等价性。定理证明用于离线证明原语转换；等价性检查用于低级转换和手动调整。变换后的CCDFG与合成的硬件之间的对应关系使得等价性检查变得高效。该项目促进了可扩展和值得信赖的硬件的开发：采用ESL方法加快了设计周期，而形式分析保证了对合成硬件的信任。引用流使得合成工具隐含地假定了显式的键设计不变量，从而促进了更激进的合成器的开发。最后，两种互补技术-模型检验和定理证明--在认证中的紧密结合也适用于其他领域。

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 .