Formal Verification System by using Hardware Compiler Fusioning of Theorem Prover and Model Checker on the Grid Environment

一个对网格计算环境实现的定理证明器，融合了输出硬件编译器目标实现的各种代码。建立一个与上游下游功能高度一致的形式化验证系统，从而大大提高异步并联电路系统的验证能力。在功能语言系统上描述了目标电路的配置信息。作为语言系统的编译输出，我们可以得到目标实现代码和对证明检查器的证明类型。基于异步逻辑门元件的4值逻辑双线模型，用消息传递并行计算机对目标电路进行了建模。最后，校验器利用电路连接校验其正确性。

A theorem prover that implements to the grid computing environment fuses the output hardware compiler target implementation various code. To build a formal verification system which is consistent high to function downstream from the upstream, thereby dramatically improving the ability for verification of asynchronous parallel circuit system. The configuration informations of the target circuit has been described on the functional language system. As compiler output of the language system, we can get the target implementation code and the type of proof to proof checker. The target circuit has been modeled by message passing parallel computer based on the 4-valued logic two-wire model of asynchronous logic gate element. Finally, proof checker can verify its correctness proof by using of the circuit connection.