CN115906730A - Method, device and storage medium for verifying logic system design - Google Patents

Abstract

The present disclosure provides a method, device and storage medium for verifying logic system design. The method includes: receiving a description of the logic system design and an assertion statement for validating the logic system design, the assertion statement being associated with a plurality of signals of the logic system design; Values on multiple operating cycles, respectively determine a plurality of assertion states of the assertion statement on the plurality of operating cycles, the assertion status includes assertion success or assertion failure; according to the plurality of signals in multiple operating cycles Determine the transition relationship of the plurality of assertion states; and generate a graphical assertion state diagram according to the plurality of assertion states and the transition relationship.

Description

Method, device and storage medium for verifying logic system design

technical field

The present disclosure relates to the technical field of chip verification, and in particular to a method for verifying logic system design, electronic equipment and a storage medium.

Background technique

In the field of verification of integrated circuits, formal verification (Formal Verification) refers to mathematically complete proof or verification of whether the implementation of the circuit actually implements the function described by the circuit design. A logical system design (eg, a circuit design) that is tested and verified may be referred to as a Design Under Test (DUT).

When performing formal verification, the user needs to input the verification target of the DUT (for example, an assertion statement (assertion statement)). The verification goal can set the goal that the DUT needs to achieve in each state, so as to judge whether the DUT meets the specified attributes. If the DUT proves through formal verification that it can achieve the goal required by the assertion, it means that the DUT meets the attributes of the design, otherwise it means that there is a problem in the design and needs to be modified. The way of proof can be to prove that DUT has this attribute, or there is a counterexample of this attribute.

Assertion statements are more complex to evaluate and form. For example, a concurrent assertion (concurrent assertion) used to describe properties possessed by a sequential logic circuit will perform an evaluation attempt (evaluation attempt) on each clock rising edge, but each evaluation has timing or evaluation path uncertainty. Only through the verification results given by the formal verification tool (for example, counterexample, which shows that the verification fails), it is difficult for the user to determine from which clock cycle the evaluation that caused the assertion statement to fail begins and on which evaluation path it occurs. That is to say, according to the usual evaluation of the assertion statement, the user can only obtain the evaluation result of the assertion statement, but cannot know the process of causing the result.

Contents of the invention

The first aspect of the present application provides a method for verifying a logic system design, including: receiving a description of the logic system design and an assertion statement for verifying the logic system design, the assertion statement being consistent with the logic system design A plurality of signal associations; based on the values of the plurality of signals over a plurality of operating cycles, respectively determine a plurality of assertion states of the assertion statement over the plurality of operating cycles, the assertion status includes assertion success or assertion failure ; determining the transition relationship of the plurality of assertion states according to the values of the plurality of signals in the plurality of operating cycles; and generating a graphical assertion state diagram according to the plurality of assertion states and the transition relationship.

A second aspect of the present application provides an electronic device. The electronic device includes a memory for storing a set of instructions; and at least one processor configured to execute the set of instructions so that the electronic device executes the method as described in the first aspect.

A third aspect of the present application provides a non-transitory computer-readable storage medium, the non-transitory computer-readable storage medium stores a set of instructions of a computer, and the set of instructions is used to cause the computer to perform the following steps when executed: The method described in the first aspect.

The present disclosure provides a method, device, and storage medium for verifying logic system design. By generating a graphical assertion state diagram, users can intuitively see the jump path of the assertion state in the evaluation process of the assertion statement, thereby determining the assertion statement The path of the evaluation process, while obtaining the assertion state, also intuitively obtains the state chain to reach the assertion state. Through the waveform diagram corresponding to the assertion state, the formal verification tool can visually display the signal and assertion state changes in the assertion associated with the logic system design in each cycle. The method provided in the present disclosure is helpful to help the user analyze the cause of the evaluation result of the assertion statement, and quickly modify the design problem.

Description of drawings

In order to more clearly illustrate the technical solutions in the present application or related technologies, the following will briefly introduce the accompanying drawings that need to be used in the description of the embodiments or related technologies. Obviously, the accompanying drawings in the following description are only for this application Embodiments, for those of ordinary skill in the art, other drawings can also be obtained based on these drawings without any creative effort.

Fig. 1 shows a schematic structural diagram of an exemplary host according to an embodiment of the present disclosure.

FIG. 2 shows a schematic diagram of an exemplary formal verification tool according to an embodiment of the disclosure.

FIG. 3A shows a schematic diagram of an exemplary assertion state diagram according to an embodiment of the disclosure.

FIG. 3B shows a schematic diagram of an exemplary waveform diagram corresponding to a state chain according to an embodiment of the disclosure.

FIG. 4 shows a flowchart of an exemplary method of verifying a logic system design according to an embodiment of the disclosure.

Detailed ways

In order to make the purpose, technical solutions and advantages of the present application clearer, the present application will be further described in detail below in conjunction with specific embodiments and with reference to the accompanying drawings.

It should be noted that, unless otherwise defined, the technical terms or scientific terms used in the application shall have the usual meanings understood by those skilled in the art to which the application belongs. "First", "second" and similar words used in this application do not indicate any order, quantity or importance, but are only used to distinguish different components. "Comprising" and similar words mean that the elements or items appearing before the word include the elements or items listed after the word and their equivalents, and do not exclude other elements or items. "Connected" and similar words are not limited to physical or mechanical connection, but may include electrical connection, whether direct or indirect.

FIG. 1 shows a schematic structural diagram of a host 100 according to an embodiment of the present application. The host 100 may be an electronic device running an emulation system. As shown in FIG. 1 , the host 100 may include: a processor 102 , a memory 104 , a network interface 106 , a peripheral interface 108 and a bus 110 . Wherein, the processor 102 , the memory 104 , the network interface 106 and the peripheral interface 108 are connected to each other within the host through the bus 110 .

The processor 102 can be a central processing unit (Central Processing Unit, CPU), an image processor, a neural network processor (NPU), a microcontroller (MCU), a programmable logic device, a digital signal processor (DSP), an application-specific Integrated Circuit (Application Specific Integrated Circuit, ASIC), or one or more integrated circuits. Processor 102 may be configured to perform functions related to the techniques described herein. In some embodiments, processor 102 may also include multiple processors integrated into a single logical component. As shown in FIG. 1, the processor 102 may include a plurality of processors 102a, 102b, and 102c.

Memory 104 may be configured to store data (eg, sets of instructions, computer code, intermediate data, etc.). In some embodiments, the simulation testing system used to simulate the test design may be a computer program stored in the memory 104 . As shown in Figure 1, the data stored in the memory may include program instructions (for example, program instructions for implementing the method for verifying logic system design of the present application) and data to be processed (for example, the memory may store temporary code). Processor 102 can also access memory stored program instructions and data, and execute the program instructions to operate on the data to be processed. Memory 104 may include volatile storage or non-volatile storage. In some embodiments, memory 104 may include random access memory (RAM), read only memory (ROM), optical disks, magnetic disks, hard disks, solid state disks (SSD), flash memory, memory sticks, and the like.

The network interface 106 may be configured to provide the host computer 100 with communication with other external devices via a network. The network can be any wired or wireless network capable of transmitting and receiving data. For example, the network may be a wired network, a local wireless network (eg, Bluetooth, WiFi, Near Field Communication (NFC), etc.), a cellular network, the Internet, or a combination thereof. It can be understood that the type of the network is not limited to the above specific examples. In some embodiments, network interface 106 may include any combination of any number of network interface controllers (NICs), radio frequency modules, transceivers, modems, routers, gateways, adapters, cellular network chips, and the like.

The peripheral interface 108 can be configured to connect the host 100 with one or more peripheral devices for information input and output. For example, peripheral devices may include input devices such as keyboards, mice, touchpads, touch screens, microphones, and various sensors, and output devices such as displays, speakers, vibrators, and indicator lights.

Bus 110 may be configured to transfer information between various components of host 100 (e.g., processor 102, memory 104, network interface 106, and peripheral interface 108), such as an internal bus (e.g., a processor-memory bus), an external bus ( USB port, PCI-E bus), etc.

It should be noted that although the host architecture above only shows the processor 102, memory 104, network interface 106, peripheral interface 108, and bus 110, in the specific implementation process, the host architecture may also include other components. In addition, those skilled in the art can understand that the above host architecture may only include components necessary to implement the solution of the embodiment of the present application, and does not necessarily include all the components shown in the figure.

FIG. 2 shows a schematic diagram of an exemplary formal verification tool 200 according to an embodiment of the disclosure. In the field of chip design, the formal verification tool 200 may be the GalaxFV formal verification tool produced by Xinhuazhang Technology Co., Ltd. Formal verification tool 200 may be a computer program running on electronic device 100 . In some embodiments, formal verification tool 200 may include components such as simulators.

Based on the system design to be verified and the assertion statement (AssertionStatement) used for formal verification of the system design, the formal verification tool 200 can perform formal verification of the system design. Inputs to verification tool 200 may include system design 202 and assertion statement 204 . Assertion statements can include assert, assume, or cover. Assert is used to indicate that a given assertion statement must be satisfied under any conditions. Assume is used to express the constraints of various formal verifications. Cover represents the situation that must be covered in the process of formal verification.

System design 202 may be a hardware or software design. The system design 202 may be a design described by software languages such as C, C++, and Java, hardware description languages such as VHDL, Verilog, and SystemVerilog, or register-transfer level (RTL) codes. For example, system design 202 may be a chip design and a verification environment used to verify the chip design.

In some embodiments, system design 202 may be an RTL design. In integrated circuit design, RTL is an abstraction level used to describe the operation of synchronous digital circuits. At the RTL level, the chip is composed of a set of registers and logical operations between registers. The reason for this is that most circuits can be regarded as storing binary data by registers, and completing data processing by logical operations between registers. The flow of data processing is controlled by a sequential state machine. These processing and control It can be described in a hardware description language.

Assertion statement 204 may, for example, be a SystemVerilog Assertion (SVA) described by SystemVerilog. Assertion statements 204 may be used to describe the desired behavior of system design 202 . By proving or falsifying assertion statement 204 may be used to verify that system design 202 is correct. Thus, assertion statement 204 is a description of behavior associated with the correctness of system design 202 .

As shown in FIG. 2 , after the system design 202 and the assertion statement 204 are processed by the verification tool 200 , a verification result 206 is finally output. The verification result 206 may be an assertion success or an assertion failure. In some embodiments, the verification result 206 may also be inconclusive.

As mentioned above, the assertion statement 204 may include a cover property for describing the design under test (DUT). For example, assert statement 204 could be:

c1:cover property(@(posedge clk)(req[0]##1gnt[0])or(req[1]##1gnt[1])

The above-mentioned assertion statement 204 involves the req signal and the gnt signal described by the logic system. Assertion statement 204 describes that system design 202 should cover the following cases: when req[0] is true, gnt[0] is true one cycle later; or when req[1] is true, gnt[1] is also true one cycle later When true, the assertion succeeds, otherwise the assertion fails.

Like the assertion statement described in c1 above, the assertion statement 204 may include multiple states and transitions between multiple states. In the current formal verification tools, the states involved in an assertion statement 204 and the transition between states only rely on the user to understand through the code. Meanwhile, the assertion statement 204 can only feed back transitions related to failed states. For example, for the above c1, the current formal verification tools usually only give the values of the req signal and the gnt signal for 2 cycles. That is, a formal verification tool may give req[0](1)=0 and req[1](1)=0 or req[0](1)=1 and gnt[0](2)=0, where req[0](1) and req[1](1) represent the values of req[0] and req[1] in the first period respectively, and gnt[0](2) represent the values of gnt[0] in the second period value. However, in the actual verification work, the signal that causes the failure state may come from an earlier signal, that is, caused by an earlier signal transition (for example, making req[0](0)=1 transition to req[0] (1)=0 causes).

All in all, the existing technology cannot visualize the connotation of the assertion statement 204, nor can it present the process information of how the system design 202 runs to the failure state to the user.

The formal verification tool 200 of the embodiment of the present disclosure can determine the state of the assertion statement 204 in each operation cycle and the transition relationship of these states based on the values of multiple signals in the assertion statement 204 in multiple operation cycles, and generate a graphical Assertion state diagram, so that the user can see the transition process of the assertion state during the evaluation process.

FIG. 3A shows a schematic diagram of an exemplary assertion state diagram 300 according to an embodiment of the disclosure.

As shown in FIG. 3A , the state in which assert statement 204 begins is initial state 301 . Signals req[0] and req[1] can have 4 states (00,11,10,01). When req[0]=0 and req[1]=0, the evaluation condition of the assertion statement 204 is not satisfied, so the assertion statement 204 will not be evaluated, and jump directly to the result state 305 of failure. When req[0]=1, req[1]=1, the assertion statement 204 begins to evaluate the attempt on the rising edge of the clock, at this time, the assertion statement 204 is in the state 302; only in the next cycle gnt[0]=0&&gnt[1 ]=0, the assertion statement 204 will jump from state 302 to result state 305 of failure, and will jump from state 302 to result state 306 of success in other cases. When req[0]=1, req[1]=0, the assertion statement 204 tries to evaluate on the rising edge of the clock, at this time, the assertion statement 204 is in the state 303; when the next cycle gnt[0]=1, the assertion is satisfied Condition, the assertion statement 204 jumps from the state 303 to the result state 306 of success, when the next cycle gnt[0]=0, the assertion condition is not met, the assertion statement 204 jumps from the state 303 to the result state 305 of failure. When req[0]=0, req[1]=1, the assertion statement 204 makes an evaluation attempt on the rising edge of the clock, at this time, the assertion statement 204 is in the state 304; when the next cycle gnt[1]=1, the assertion is satisfied Condition, the assertion statement 204 jumps from the state 304 to the result state 306 of success, when the next cycle gnt[1]=0, the assertion condition is not satisfied, the assertion statement 204 jumps from the state 304 to the result state 305 of failure.

Thus, the assertion state diagram 300 shows the assertion states of the assertion statement 204 and the transition relationship between these assertion states.

In some embodiments, the formal verification tool 200 may receive an instruction from a user to select a failed assertion state in the assertion state diagram 300 . Based on this instruction, formal verification tool 200 may highlight the state chain of failed assertion states in assertion state diagram 300 . As the state chain shown in bold in FIG. 3A , the assertion statement 204 jumps from the initial state 301 to the state 303 , and then jumps to the result state 305 . It can be understood that FIG. 3A only exemplarily highlights a state chain of a failed assertion state, and the formal verification tool 200 can display more state chains of assertion states according to user instructions, including a state chain of a failed assertion state or a successful assertion state . The bold display shown in FIG. 3A is only one form of highlighting, and the formal verification tool 200 can also use other methods (for example, making the jump connecting lines to be displayed in other colors) to perform highlighting, which is not covered in this disclosure. limit.

In some embodiments, a state chain shown in assert state diagram 300 may be an evaluation attempt of assert statement 204 .

In some embodiments, the formal verification tool 200 may receive an instruction from the user to select a target state, and highlight the state chain from the initial state 301 to the target state.

In some embodiments, the highlighted state chain may include multiple states, but the highlighted state chain in the state diagram 300 only includes some of the states, and the remaining states that are not displayed are displayed with omitted icons. For example, an ellipsis can be used as an ellipsis icon to represent a remaining state that is not displayed. The formal verification tool 200 may receive an instruction from the user to further click on the omission icon in the state diagram 300 to expand and display the remaining states that are not displayed. In some embodiments, clicking on the omission icon may allow the user to further define which parts of the remaining state that are not displayed should be expanded.

Formal verification tool 200 can also generate and display waveform diagrams for users to view changes in signals associated with assertions.

FIG. 3B shows a schematic diagram of an exemplary waveform diagram 310 corresponding to a state chain, according to an embodiment of the disclosure.

For the state chain of the highlighted failed assertion state shown in FIG. 3A , the formal verification tool 200 can generate and display a waveform diagram 310 corresponding to this state chain. As can be seen from waveform diagram 310 , formal verification tool 200 generated an evaluation attempt covering properties: req[1:0]:00,01,01,gnt[1:0]:00,11,10, assert statement 204 The evaluation of starts from the second cycle, and the assertion statement 204 goes through the evaluation path of initial state 301—>state 303—>result state 305. It should be noted that although FIG. 3B only shows waveforms of three operating cycles, in an actual operating process, the waveforms may be waveforms of the entire verification process including more operating cycles. For example, after the result status 305 of failure is obtained in this evaluation attempt, the formal verification tool 200 can proceed to the next evaluation attempt, and then the waveform diagram can continue to display the next fourth cycle, fifth cycle or even more Waveforms of the signals req and gnt of a cycle.

It can be understood that the formal verification tool 200 can also display a waveform diagram of any assertion state in the assertion state diagram 300 . The waveform diagram that specifically displays the assertion state is determined by actual requirements. In some embodiments, the actual demand for displaying the waveform diagram of the assertion state may be an instruction issued by the user to select a target assertion state, and the formal verification tool 200 displays the waveform diagram corresponding to the assertion state according to the instruction.

In this way, by generating a graphical assertion state diagram, the formal verification tool 200 can not only display the conversion process of the assertion statement to the user, but also visually display the state chain to an assertion state. Through the waveform diagram corresponding to the assertion state, the formal verification tool 200 can visually display the signal in the assertion associated with the logic system design and the change of the assertion state in each cycle. Adopting the method provided by the present disclosure can help users analyze the cause of the assertion result and quickly modify the design problem.

The embodiment of the present application provides a method for verifying logic system design.

FIG. 4 shows a flowchart of an exemplary method 400 for verifying a logic system design according to an embodiment of the present application. The method 400 can be executed by the host 100 in FIG. 1 , more specifically, by the formal verification tool 200 running on the host 100 . Method 400 may include the following steps.

In step 402, the formal verification tool 200 may receive a description of the logical system design (eg, the system design 202 of FIG. 2 ) and an assertion statement (eg, the assertion statement 204 of FIG. 2 ) for verifying the logical system design, The assertion statements are associated with a plurality of signals of the logic system design (eg, signals req and gnt). The assertion statement may include assert, assume or cover.

In step 404, the formal verification tool 200 can respectively determine a plurality of assertion states (for example, initial state, intermediate state, status, and result status), the assertion status includes assertion success or assertion failure.

In step 406, the formal verification tool 200 may determine the transition relationship of the plurality of assertion states according to the values (for example, 0 or 1) of the plurality of signals over the plurality of operating cycles.

In step 408, the formal verification tool 200 can generate a graphical assertion state diagram (for example, the assertion state diagram 300 in FIG. 3A ) according to the plurality of assertion states and the conversion relationship. In some embodiments, an assertion state diagram may show that the assertion goes from an initial state (e.g., initial state 301 of FIG. 3A ) to an intermediate state (e.g., states 302, 303, 304 of FIG. , the transition relationship of the resulting states 305, 306) in FIG. 3A. The assertion state diagram may also display the values (eg, 0 or 1) of the plurality of signals (eg, signals req and gnt) over a plurality of execution cycles. Formal verification tool 200 can also generate and display waveform diagrams.

In some embodiments, the assertion state diagram may include an initial assertion state (eg, initial state 301 of FIG. 3A ) and a failed assertion state for an assertion failure (eg, failed result state 305 of FIG. 3A ). Formal verification tool 200 may receive an instruction to select the failed assertion state on the assertion state diagram; highlight the state chain from the initial assertion state to the failed assertion state (e.g., the bolded state of FIG. 3A chain).

In some embodiments, formal verification tool 200 may display a waveform diagram (eg, waveform diagram 310 of FIG. 3B ) corresponding to the state chain. For example, waveform diagram 310 may show the values of signals req and gnt over three execution cycles in an assertion statement (e.g., assertion statement 204) whose assertion evaluation begins at the second cycle and whose evaluation The path may be initial state 301 —> state 303 —> result state 305 .

In some embodiments, the formal verification tool 200 may receive an instruction to select a target assertion state (e.g., a failed assertion state) among a plurality of assertion states on the assertion state diagram (e.g., the assertion state diagram 300 of FIG. 3A ). ;Display the waveform diagram corresponding to the asserted state of the target.

In this way, through the graphical assertion state chain and waveform diagram, the formal verification tool 200 can not only give the evaluation result of the assertion statement, but also visually display the evaluation process of the assertion statement (that is, the transition relationship of the assertion state) and the association in the assertion changes in the signal.

The embodiment of the present application also provides an electronic device. The electronic device may be the host 100 in FIG. 1 . The electronic device may include a memory for storing a set of instructions; and at least one processor configured to execute the set of instructions to cause the electronic device to perform the method 400 .

The embodiment of the present application also provides a non-transitory computer-readable storage medium. The non-transitory computer-readable storage medium stores a set of instructions for a computer, which when executed causes the computer to perform the method 400 .

The foregoing describes some embodiments of the present application. Other implementations are within the scope of the following claims. In some cases, the actions or steps recited in the claims can be performed in an order different from that in the embodiments and still achieve desirable results. In addition, the processes depicted in the accompanying figures do not necessarily require the particular order shown, or sequential order, to achieve desirable results. Multitasking and parallel processing are also possible or may be advantageous in certain embodiments.

Those of ordinary skill in the art should understand that: the discussion of any of the above embodiments is exemplary only, and is not intended to imply that the scope of the application (including claims) is limited to these examples; under the thinking of the application, the above embodiments or Combinations between technical features in different embodiments are also possible, steps may be implemented in any order, and there are many other variations of the different aspects of the application as described above, which are not presented in detail for the sake of brevity.

Although the application has been described in conjunction with specific embodiments thereof, many alternatives, modifications and variations of those embodiments will be apparent to those of ordinary skill in the art from the foregoing description. For example, other memory architectures such as dynamic RAM (DRAM) may use the discussed embodiments.

This application is intended to embrace all such alterations, modifications and variations that fall within the broad scope of the appended claims. Therefore, any omissions, modifications, equivalent replacements, improvements, etc. made within the spirit and principles of the present application shall be included within the protection scope of the present application.

Claims (7)

1. A method of validating a logic system design, comprising:

receiving a description of the logic system design and assertion statements for verifying the logic system design, the assertion statements being associated with a plurality of signals of the logic system design;

determining a plurality of assertion states of the assertion statement over a plurality of operating cycles based on values of the plurality of signals over the plurality of operating cycles, respectively, the assertion states including assertion success or assertion failure;

determining a transition relationship of the plurality of assertion states according to values of the plurality of signals over a plurality of operating cycles; and

and generating a graphical assertion state diagram according to the assertion states and the conversion relation.

2. The method of claim 1, wherein the assertion state diagram includes an initial assertion state and a failed assertion state in which assertion fails, the method further comprising:

receiving an instruction to select the failed predicate state on the predicate state diagram;

highlighting a chain of states from the initial assertion state to the failed assertion state.

3. The method of claim 1, wherein the method further comprises:

receiving an instruction to select a target predicate state among a plurality of predicate states on the predicate state diagram;

displaying a waveform diagram corresponding to the target assertion state.

4. The method of claim 2, wherein the method further comprises:

and displaying a waveform diagram corresponding to the state chain.

5. A method as recited in claim 1, wherein the assertion declaration comprises assert, or cover.

6. An electronic device comprises

A memory for storing a set of instructions; and

at least one processor configured to execute the set of instructions to cause the electronic device to perform the method of any of claims 1-5.

7. A non-transitory computer readable storage medium storing a set of instructions of a computer for, when executed, causing the computer to perform the method of any of claims 1 to 5.

Images