Research And Implementation Of Formal Verification Method Of Memory Controller

The memory controller is a key interface component of many chips.The correct and stable operation of the memory controller is the prerequisite for the stable operation of the entire chip.When verifying the correctness of the memory controller,if a single analog verification method is used,it will encounter the problem that the stimulus cannot traverse all state spaces,so that it cannot be proved whether the interface signals output by the design fully comply with memory interface standards such as DDR4.Not only that,in order to improve the efficiency of memory access,designers need to optimize the scheduling method of memory controller read and write requests,so the arbitration method of read and write requests has a high complexity.Therefore,this paper mainly analyzes and studies the correctness of the read-write request queue arbitration logic of the memory controller and the correctness of the temporal relation between the output commands of the memory controller.This article first analyzes the difficulties encountered in the verification process of memory controllers,and introduces the current common methods for verifying memory controllers at home and abroad and the automatic generation of assertions for verifying the correctness of the timing relationship between several memory controller commands.Then it introduces three commonly used formal verification methods,explains the model checking principle and environment creation method,and briefly explains the verification method based on assertion used in verification.The structure and functions of the memory controller are explained by introducing the working principle,structural composition,timing relationship between output commands,and request arbitration strategy.The formal verification method is to use mathematical principles to verify the correctness of the design.It can automatically traverse all the state spaces that need to be verified.It shows better completeness and efficiency than simulation verification,so this paper proposes a formal verification method based on model checking to verify the correctness of the memory controller.This article first builds reference model for two functional modules,constrains module input,writes formal verification assertions,and thenuses formal verification tools to verify the correctness of the corresponding function of the memory controller,and based on summary and analysis the formal verification results,the formal verification environment is adjusted to improve the coverage.The coverage is verified,and the correctness verification of the arbitration logic of the read and write request queue of the memory controller and the correctness of the timing relationship between the output commands of the memory controller are completed.When verifying the correctness of the timing relationship between the output commands of the memory controller,due to the complexity of the DDR4 standard,there may be a problem that the manually written formal verification assertion cannot be quickly standardized and accurate,so this article has developed a tool for automatically generating formal verification assertions.Write a script by summarizing the calculation method of the delay between commands,and use the script to process the data in the DDR4 standard to generate assertion.The tool can generate corresponding assertions based on the basic values set by the current verification mode,further improving the efficiency of formal verification and verification accuracy.