In recent years, due to the continuous expansion of the scale and complexity of integrated circuits, the verification technology that is the most important part of ensuring the correctness and integrity of chip functions has faced a series of huge challenges. How to ensure the rapid and efficient realization of larger-scale circuits and comprehensive and effective verification is a pain point that the chip design industry has to face and solve. Traditional circuit-based simulation technology has always had many problems that cannot be effectively solved, such as the inability to cover extreme situations, excessive simulation time, and test environment construction. The industry is also constantly exploring some more effective verification methodologies, such as formal verification, portable incentive standards (PSS) and so on.
The formal method is a verification methodology based on rigorous mathematics and algorithms. In chip verification, users use SVA assertions to describe design specifications that need to be proven, and build a Formal model by compiling RTL and SVA-based assertion languages. On the one hand, according to the requirements of the design spec, the function points that need to be verified are extracted, and then the function scenarios to be checked are described and defined one by one through the SVA assertion language. On the other hand, it constrains the occurrence of illegal scenes and automatically performs mathematical analysis and proof, ensuring that the logic has no dead ends by traversing all possible excitation spaces. Compared with dynamic verification, formal verification has at least four irreplaceable important advantages.
Formal verification of the four major advantages
01 Verify spatial completeness
When each signal at all inputs has only 0 or 1 values per clock cycle, then any test scenario is a two-dimensional subset of space-time in the complete test space. By transforming RTL into a formal verification model, the functional verification problem is transformed into a mathematical derivation of a given behavior, and the complete verification space is traversed.
02 Accurately locate the wrong scene
Once there is a design scenario that causes the assertion to be unsuccessful, the specific waveform at a specific clock is given precisely. The traditional dynamic verification is based on Log for debug, which needs to be deduced from the transaction level and located possible design problems step by step.
03 Verify that the environment is simple and efficient
There is no need to build a complex and hierarchical verification environment, and the Property is accurately described for the tested scenario, and then the input scene traversal and derivation proof are performed.
04 Coverage collection is off-engineer human risk
The formal verification coverage collection scheme is based on algorithms and models spontaneously completed by tools, and the whole process does not rely on manual definition of function coverage, which greatly avoids the risk of low coverage accuracy due to human error.
In general, formal verification technology is efficient and complete, and is a sharp tool for discovering kernel bugs other than human normal thinking, which is conducive to finding and assisting in correcting errors in circuit design as soon as possible and as soon as possible, improving design quality, and shortening the chip design cycle.
The GalaxyFV is such a formal verification tool for HDL circuit design, which can mathematically and completely prove that "the implementation scheme of the circuit meets the functions described in the design specifications". On the basis of retaining the completeness of formal verification, GalaxFV relies on the FusionVerify Platform, which is integrated with other verification tools in terms of compilation, debugging, coverage, etc., further accelerates the convergence of design verification, and helps chip design to complete simple and efficient complete verification at a higher stage, thereby greatly improving the verification efficiency.
Use a validated instance of GalaxyFV
The following example is the excellent work of Shenzhen University participating in the proposition of "error correction codec algorithm implementation and verification" in the Chinese graduate student "core" competition.
Channel error correction codec algorithm implementation module based on Verilog language design
Below we implement a channel error correction codec algorithm based on the Verilog language design, using GalaxyFV to build a formal verification process.
This module is a channel error correction design in the communication field chip in order to ensure that the information transmission is continuous and not distorted. It encodes the original five channels into seven channels, and in the event that at most two of these seven channels are damaged, it is able to decode to recover the data of the five channels at the original input.
The design has a variety of design specifications, each of which can be described by an SVA attribute (as shown in the figure), and finally corresponds to a verification target (Goals).
In formal verification, we construct the verification excitation with a constrained property, where 'asm_ch' corresponds to the first design specification, which can be described as follows: the channel error enable (low-effective) signal 'channel' needs to have at least 5 bits with a value of 1, that is, the number of channels in which damage occurs is up to 2.
Formal validation implements functional checking by asserting attributes. The 'ast_sym_data_0' corresponds to the second design specification, which can be described as: for each clock cycle after the end of the reset, if the input data of channel 0 is label data, then after four cycles from the beginning of the current cycle, the output data of channel 0 will be equal to the label data. Where the labeled data is a constant, the waveform plot below shows the expected behavior of the property.
Presentation of the formal validation environment in the instance
First, we need to circumvent incentives that don't meet design requirements by constraining attributes. Second, we need to define special signals, such as clock and reset signals, to ensure that the tool can process these signals appropriately. In addition to this, we check the data consistency through the self-developed scoreboard.
GalaxFV relies on its self-developed word-level modeling method to convert millions of lines of design code into mathematical models, transform verification problems into mathematical solutions, and then rely on solvers to solve them. The solver, on the other hand, is like an "operating system" that decomposes a mathematically complex system and gives the final proof.
At the same time, GalaxyFV has dynamic intelligent scheduling, just like having a "control center", which can match the best solution according to the characteristics of the verification target, and select different "operating systems" to solve according to local conditions. Finally, distributed computing will be designed to "divide and conquer". For a large-scale computing problem, GalaxFV can divide it into small tasks that can be performed at the same time, let multiple computers process them separately, and finally get the verification results.
Product Highlights
Built using a high-performance Word-Level Modeling approach
Compared with bit-level modeling methods, word-level modeling methods have the following advantages:
I. Large granularity of modeling
II. Good performance
III. Word-level solvers and bit-level solvers can be called at the same time
IV. Strong scalability
V. Proprietary, efficient application-level assertion library developed in-house
GalaxFV builds a dedicated, efficient application-level assertion library for standard components commonly used in design, parameterizing them, improving configurability, and reducing the difficulty of users building assertions and constraints. It can make full use of computing power, improve parallel efficiency, improve ease of use and use efficiency, and reduce the threshold for formal verification to be applied to the industry.
Equipped with a self-developed high concurrency, high performance solver
GalaxFV unleashes the power of distributed computing on server clusters or cloud platforms to enable fast proof solving. In addition, GalaxFV has developed an intelligent grouping and scheduling prediction algorithm for solvers, combined with the algorithms and characteristics of each engine, in the face of different design and assertion types, combined scheduling of each solver unit to solve, to further improve the solving efficiency.
Combining these technical features, GalaxFV delivers impressive performance on some customer designs, surpassing approximately 20% of the measured performance compared to existing industry-renowned formal verification tools. (Measured only for an AsyncFIFO design)
The GalaxyFV uses mathematical methods to solve verification problems, which is a strong supplement to simulation technology, advanced modeling methods and scheduling algorithms, in our rtllib module performance measurement, excellent performance, has high value for engineering applications.
—— Zhou Xiaobin, a form verification expert of Tianshu Zhixin
Formal verification is based on mathematical thinking for verification and solution, which has high reliability and can greatly shorten the development cycle. Faced with the difficulty of using a high threshold for the use of formal verification tools, the R&D team of XinHuazhang adopts word-level modeling methods to build, and is equipped with a special assertion library and solver developed by itself, so that the formal verification tools with high completeness advantages can help more chip R&D engineers to find problems and quickly repair them as soon as possible in the early stage of project development.
—— Qi Zhenghua, Vice President of R&D of Xinhuazhang Technology