CN114896922A - Chip IO multiplexing verification method based on formal verification - Google Patents

Abstract

The invention discloses a chip IO multiplexing verification method based on formal verification, which comprises the following steps: s1, refining the chip IO multiplexing relation file according to the chip specified definition; s2, automatically forming an IO description file according to the chip IO multiplexing relation file; s3, performing open form verification, and importing a chip file and an IO description file to a verification tool; s4, starting formal verification and outputting a verification result; and S5, analyzing the result and judging whether the design BUG is adopted. Compared with the traditional Uvm verification, the IO multiplexing verification technology based on the formal verification is simple to use and concise in steps, and the workload is greatly reduced; the method does not need chip system-level simulation operation, so the operation time is short, and the verification efficiency is greatly improved.

Description

Verification method of chip IO multiplexing based on formal verification

technical field

The invention relates to a chip IO multiplexing verification method based on formal verification.

Background technique

Verification is a very important and indispensable link in the development of modern chips. Its mission is to ensure that the design functions as designed and is free of failures. Usually in a chip development project, the time and human resources spent on chip verification can account for 70%.

The mainstream traditional verification methods are mainly the verification methodologies represented by UVM (Universal Verification Methodology) and SystemVerilog. Usually, a combination of random constraints and directional excitation is used to automatically generate excitation in circuit simulation, drive the circuit to run, and complete the verification function. .

At present, formal verification is attracting more and more attention. Its main idea is to describe the properties of the design function according to the design specification, and automatically perform mathematical analysis and proof based on the mathematical expression and model abstracted from the chip design.

The shortcomings of the traditional verification method are: 1. The UVM verification simulation time is long; 2. The workload is large and the completeness is difficult to guarantee. Since UVM verification needs to drive the chip simulation operation, and the scale of modern chips has increased dramatically, the current large-scale server-level CPU chips can reach the scale of tens of billions of gates. Under certain simulation computing resource conditions, with the increase of chip scale, its system The time to run high-level simulations is greatly improved. Due to the traditional UVM verification method, it is necessary to build a verification scenario for each functional item, provide verification incentives, analyze the output results and judge whether it meets the expectations. Now the chip scale has increased sharply, the integration level has become higher and higher, and the interconnection between internal components has become more and more Complicated, the functional items that need to be verified have also exploded, and the required labor costs are extremely high, and it is easy to have a lack of scenarios, incentives, or result analysis, resulting in insufficient functional verification.

For large-scale and complex chips, there are often multi-function multiplexing on the IO pins, and the IO pins can flexibly implement different interface functions through different configurations of registers. For the verification of this multiplexing technology, if the traditional UVM verification method is used, it is necessary to build a verification environment, perform relevant configurations for each function of each pin, and provide different incentives on the IO pins or inside the chip. The internal or IO pins are observed and the results are judged. First, the large-scale chip runs for a long time. The SoC chip only consumes a long time to start the boot of the CPU core. Second, the workload is very large. For a typical mcu chip, If there are 40 pins, with an average of 5 functional reuses per pin, the verification process needs to be written 200 times.

SUMMARY OF THE INVENTION

The present invention proposes a chip IO multiplexing verification method based on formal verification, which can greatly improve the efficiency of such verification. The formal verification method does not require the simulation of the chip. After compiling, calling a formal verification tool (commonly known as VC Formal or Japer Gold), and combining with the provided IO multiplexing relational table, automated analysis and verification can be performed. Verification, the final output results, firstly can greatly improve work efficiency, reduce labor cost and time cost consumption, and secondly condense the complete source of testing into the IO multiplexing relationship file written according to the chip spec, reducing the risk of completeness decline .

The technical solutions adopted are as follows:

A chip IO multiplexing verification method based on formal verification, comprising the following steps:

S1. Refine the chip IO multiplexing relationship file according to the chip specification definition;

S2. According to the chip IO multiplexing relationship file, the IO description file is automatically formed;

S3. Turn on formal verification, and import the chip file and IO description file into the verification tool at the same time;

S4, start the formal verification, and output the verification result;

S5. Analyze the results to determine whether it is a design bug.

For the optimization of the technical solution of the present invention, in S1, according to the chip design document, write a chip IO multiplexing relationship file, the chip IO multiplexing relationship file includes type and signal name, and the type is input item input, output type output or both input and output. inout; the signal name includes the signal name of the function multiplexing item and the signal name after each multiplexing.

For the optimization of the technical solution of the present invention, in S2, the IO description file is to write a corresponding script configuration file according to the information in the chip IO multiplexing relationship file; for each pin in the IO description file, each input type and Each output-type multiplexing function point is expanded into one entry, and each inout-type multiplexing function point is expanded into two entries.

Preferably, each table entry includes the hierarchical path of the pin in the chip code, the signal that drives the multiplexed function point inside the chip or is driven by it, the enable condition and the test name.

For the optimization of the technical solution of the present invention, in S3, the verification tool is VC Formal.

For the optimization of the technical solution of the present invention, in S3, open the formal verification tool, perform related function configuration, import the chip source code file, compile and synthesize into a netlist, and then import the IO multiplexing description file to obtain each table to be tested. Item, set initialization state, clock, reset signal.

The optimization of the technical solution of the present invention, in S4, start the verification, carry out the connectivity test through the input, output and enabling conditions of each entry of the IO description file, judge the correctness of the IO multiplexing, and output the results, and the results are analyzed. analysis.

For the optimization of the technical solution of the present invention, in S5, the IO multiplexing method does not match the design document, and the error information is printed to carry out result analysis; when the printed information indicates that a certain pin is wrong, it means that under the conditions set by the current script, The multiplexing of pins in the chip file is inconsistent with the script settings; when the above inconsistency occurs, there may be two cases, one is that the chip file has errors, that is, the design is BUG, and the other is that the script is written incorrectly, even if the conditions are enabled Settings are not accurate.

For the optimization of the technical solution of the present invention, when a problem occurs in the verification result, it is judged whether it is a design bug of chip IO multiplexing, or the enabling condition setting of the table entry is not accurate; if the latter, then modify the table entry of iteration S2 and restart. S3 and S4, go to the next round of testing until all design bugs are found.

The beneficial effects of the present invention compared with the prior art are:

1. Compared with the traditional UVm verification, the verification method of the present invention, the IO multiplex verification technology based on formal verification is simple to use, the steps are concise, and the workload is greatly reduced.

2. The verification method of the present invention does not require chip system-level simulation operation, so the running time is short, and the verification efficiency is greatly improved.

Description of drawings

FIG. 1 is a flow chart of the verification method of the present invention.

FIG. 2 is a schematic diagram of an IO multiplexing relationship file of the present embodiment.

Detailed ways

The technical solutions of the present invention are described in detail below, but the protection scope of the present invention is not limited to the embodiments.

In order to make the content of the present invention more obvious and comprehensible, further description will be made below with reference to FIGS. 1 to 2 and the specific embodiments.

In order to make the objectives, technical solutions and advantages of the present invention clearer, the present invention will be further described in detail below with reference to the accompanying drawings and embodiments. It should be understood that the specific embodiments described herein are only used to explain the present invention, but not to limit the present invention.

A formal verification-based chip IO multiplexing verification method of the present embodiment includes the following steps:

S1. Refine the chip IO multiplexing relationship file according to the chip specification definition;

S2. According to the chip IO multiplexing relationship file, the IO description file is automatically formed;

S3. Turn on formal verification, and import the chip file and IO description file into the verification tool at the same time;

S4, start the formal verification, and output the verification result;

S5. Analyze the results to determine whether it is a design bug.

In this embodiment, in S1, according to the chip design document, write a chip IO multiplexing relationship file, the chip IO multiplexing relationship file includes type and signal name, and the type is input item input, output type output or both input and output inout; The signal name includes the signal name of the function multiplexing item and the signal name after each multiplexing.

As shown in Figure 2, for example, the first chip pin P0[6] can be multiplexed into the following 4 functions, I2S_RX_SDA type is input, SSP1_SSEL input and output type, T2_MAT0 output type and U1_RTS output type.

In this embodiment, in S2, the IO description file is to write a corresponding script configuration file according to the information in the chip IO multiplexing relationship file; for each pin in the IO description file, each input type and each The multiplexed function points of the output type are expanded into one entry, and each multiplexed function point of the inout type is expanded into two entries.

Each table entry includes the hierarchical path of the pin in the chip code, the signal that drives the multiplexed function point in the chip or is driven by it, the enable condition and the test name. Specifically: each entry covers the following parts:

a) The hierarchical path of the pin in the chip code is convenient for the formal tool to analyze and locate the pin in the netlist in the chip;

b) The multiplexed function point is driven internally by the chip, or the signal driven by it (module-level output);

c) Enable condition (generally, the configuration pin is the register configuration of the multiplexed function, and the output enable signal needs to be added for the output signal);

d) Test name, to indicate which test was successful or failed.

In this embodiment, in S3, the verification tool is VC Formal or Japer Gold. Both of these verification tools are known verification tools in the art and are known to those skilled in the art.

In this embodiment, in S3, open the formal verification tool, configure related functions, import the chip source code file, compile and synthesize a netlist, and then import the IO multiplexing description file to obtain each table item to be tested, Set the initialization state, clock, reset and other signals.

In this embodiment, in S4, the verification is started, and the connectivity test is performed through the input, output and enabling conditions of each entry in the IO description file, the correctness of the IO multiplexing is judged, the result is output, and the result is analyzed. .

In S5, the IO multiplexing method does not match the design document, and an error message is printed to analyze the result; when the printed information indicates that a certain pin has an error, it means that under the conditions set by the current script, the repetition of the pin in the chip file The usage situation is inconsistent with the script setting; when the above inconsistency occurs, there may be two situations, one is that the chip file is wrong, that is, the design is BUG, and the other is that the script is written incorrectly, even if the condition setting is not accurate.

When there is a problem with the verification result, it is determined whether it is a design bug of chip IO multiplexing or the setting of the enabling conditions of the table entry is inaccurate; if it is the latter, modify the table entry of iteration S2, restart S3 and S4, and proceed to the next step. rounds of testing until all design bugs are found.

The verification method in this embodiment is a verification method and idea of IO multiplexing by using formal verification. The traditional UVM verification method needs to build a verification environment, build a test scenario, enable test incentives to obtain test results and compare them, and target all IOs. Each function multiplexing item of the pin is repeatedly tested, and the workload is huge. Since IO multiplexing is a system-level function, the entire chip needs to be simulated and run. The system operation of the entire chip takes a long time and the verification efficiency is low. The patented technology is based on formal verification, the steps are simple, and the chip system-level operation is not required. It only needs to compile and pass, and extract and organize the relevant table items that can describe the IO multiplexing according to the chip spec.

Specific examples:

As shown in Figure 2, the IO multiplexing register that controls P0[6] is P0_6_IOCON. When this register is equal to 0, 1, 2, 3, and 4, it corresponds to the four digital functions respectively. In the IO description file, the enable condition is set as, P0_6_IOCON=3, then the signal t2_mat inside the chip should be connected to the P0[6] port. In the chip description file, the signal t2_mat is used as the source terminal, and P0[6] is used as the target terminal.

After importing the IO description file and the chip file at the same time, the tool will automatically compare whether the connection method of the chip is consistent with the description file under the enabled condition in the chip file. If it is inconsistent, an error will be printed.

After the error is found, the engineer will check whether the IO description file is written incorrectly or the bug in the chip design itself, and deal with it separately to eliminate it.

Repeat the above debugging process until all IO descriptions correspond to the chip files.

The above embodiments are only to illustrate the technical idea of the present invention, and cannot limit the protection scope of the present invention. Any modification made on the basis of the technical solution according to the technical idea proposed by the present invention falls within the protection scope of the present invention. Inside.

Claims (9)

1. A chip IO multiplexing verification method based on formal verification is characterized in that: the method comprises the following steps:

s1, refining the chip IO multiplexing relation file according to the chip specified definition;

s2, automatically forming an IO description file according to the chip IO multiplexing relation file;

s3, performing open form verification, and importing a chip file and an IO description file to a verification tool;

s4, starting formal verification and outputting a verification result;

and S5, analyzing the result and judging whether the design BUG is adopted.

2. The chip IO multiplexing verification method based on formal verification according to claim 1, wherein: in S1, writing a chip IO multiplexing relation file according to the chip design document, wherein the chip IO multiplexing relation file comprises a type and a signal name, and the type is input, output or both input and output; the signal name includes a signal name of the function multiplexing item and a signal name after each item multiplexing.

3. The chip IO multiplexing verification method based on formal verification according to claim 1 or 2, wherein: in S2, the IO description file is a corresponding script configuration file written according to the information in the chip IO multiplexing relation file; and expanding the multiplexing function point of each input type and each output type into one table entry and expanding the multiplexing function point of each input type into two table entries for each pin in the IO description file.

4. The chip IO multiplexing verification method based on formal verification according to claim 3, wherein: each table entry comprises a hierarchical path of a pin in a chip code, a signal which drives the multiplexing function point or is driven by the multiplexing function point inside the chip, an enabling condition and a test name.

5. The chip IO multiplexing verification method based on formal verification according to claim 1, wherein: in S3, the verification tool is VC Formal.

6. The chip IO multiplexing verification method based on formal verification according to claim 1 or 5, wherein: in S3, the formal verification tool is turned on, the relevant function configuration is performed, the chip source code file is imported, the compiling is performed to synthesize a netlist, the IO multiplexing description file is imported, each table entry to be tested is obtained, and the initialization state, the clock and the reset signal are set.

7. The chip IO multiplexing verification method based on formal verification according to claim 6, wherein: in S4, verification is started, a connectivity test is performed through the input, output, and enable conditions of each entry of the IO description file, the correctness of IO multiplexing is determined, and the result is output and analyzed.

8. The chip IO multiplexing verification method based on formal verification of claim 7, wherein: in S5, the IO multiplexing mode is not matched with the design document, and error information is printed out for result analysis; when the printed information shows that a certain pin is in error, the multiplexing condition of the pin in the chip file is inconsistent with the script setting under the condition of the current script setting; when the inconsistency occurs, there may be two situations, one is that a chip file has an error, i.e., a BUG is designed, and the other is that a script is written with an error, even if the condition setting is inaccurate.

9. The chip IO multiplexing verification method based on formal verification of claim 8, wherein: when the verification result has a problem, judging whether the design BUG of the chip IO multiplexing or the enabling condition setting of the table entry is inaccurate; if the latter, the entries of iteration S2 are modified, S3 and S4 are restarted, and the next round of testing is performed until all design bugs are found.

Images