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

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