The Study Of Digital Systems Verification In The Orem Prover

With the continuous development of the integrated circuit industry, the size of the hardware circuit is growing more and more complex, hardware verification as an important part of the hardware design, but also become the research focus. The traditional means of verification simulation, emulation, etc., but these methods have their limitations, researchers formalized means used in the verification of hardware circuit, there is a formal verification technique.On the other hand, with the technology and design capabilities continue to improve, in order to meet the market requirements of cost and cycle, system-on-a-chip has been gradually towards the SoC development. SoC design can not be separated from the IP library, where IP is the most widely used form of soft-core, so more and more demand on the the IP soft-core. Also, because the developers need functional verification IP soft core, which will increase the SoC development cycle, so the paper proposes an authentication scheme based on the theorem prover, reducing the IP soft-core users to check IP function of time.This article uses the the Coq platform, a hardware circuit logical model is constructed, and to establish the rules of conversion from RTL to Coq language, so that the IP provider can prove RTL-level code function according to the requirements specification, IP users can then use the Coq tool quickly check the proofs correctness of the function, which can make the IP user to accelerate SoC development cycle. This article also uses some classic synchronization circuit according to the transformation rules we developed to convert need to prove theorems, and circuit extraction, and then converted assumptions to complete the proof of the theorem, which proved the feasibility of the program. And we use the reusable code and proof code as a reference to ensure the compatibility of the later.At the end of this article, we do the8051classic instruction-level functional verification. We will do a complete conversion, and then use the Coq language writing instruction function theorem. At last, we use the RTL conversion assumptions to prove instruction function theorem.The results show that we can use the conversion rules and the hardware circuit model to verify the8051instruction-level functional.