论文部分内容阅读
一、引言 验证逻辑设计正确性的传统方法是模拟(Simulation),然而随着数字电路规模和功能扩大,模拟方法已不能保证设计的正确性。与此相对,形式验证(formal verification)方法通过对电路结构的形式进行检查和比较来完成验证。它不需要模拟,因而,避开了模拟信号指数上升的问题。形式验证是一个静态分析,它比动态的逻辑模拟具有更大的潜力。 形式验证的一种方法是将其视为自动定理证明:已知一些公理和已成立的引理,证明某一表达式与另一表达式是等价的。美国Illinois技术研究所的A.S.Wojcik用AURA自动定理证明系统进行了逻辑设计的形式验证,AURA用归结原理作自动定理证明,由于归结法会产生大量子句,因此,证明的效率不是很高。
I. INTRODUCTION The traditional method of verifying the correctness of logic design is Simulation. However, as the scale and function of digital circuits expand, the simulation method can not guarantee the correctness of the design. In contrast, the formal verification method verifies the form of a circuit by checking and comparing it. It does not require simulation, thus avoiding the problem of an exponential rise in the analog signal. Formal verification is a static analysis that has more potential than dynamic logic simulation. One way of formal verification is to treat it as an automatic theorem proving that some axioms and established lemmas are known to prove that one expression is equivalent to another. A.S. Wojcik of the Illinois Institute of Technology in the United States used AURA automatic theorem to prove that the system was formally verified by logic design. AURA proved by automatic theorem with the principle of reasoning that the efficiency of proof is not very high due to the large number of clauses generated by the summing method.