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.