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

电子系统级（ESL）设计，使用高级语言（如SystemC）在行为上指定，提高了硬件设计抽象的层次。这种方法主要依赖于行为综合，它将ESL设计编译为寄存器传输级（RTL）设计。然而，合成工具执行的优化使得它们的实现容易出错，破坏了合成硬件的可信度。 本研究开发了一种机械化的基础设施，用于验证由行为合成产生的硬件设计。它需要开发一个经过认证的合成转换“参考流程”。参考流是从一个productionsynthesis工具的工作，通过新的正式结构称为“时钟控制数据流图”（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.