Methods for automatically generating assertions
OwnerYuan Lu, Yunshan Zhuinventors
Life of this patent
Estimating the term…
Abstract
One embodiment of the present invention provides a method that automatically generates assertions of a hardware design. The method includes accessing a trace and a set of predicates of the hardware design. Then, the trace is projected over the set of predicates to generate a second trace. Then, a new set of states of the second trace is computed and the result is represented as a logical formula. The formula is reduced by logic optimization techniques. And finally, a set of logical consequences of the logic formula is produced and each logical consequence is enumerated as an assertion.
Claims30
A method for generating assertions of a hardware design to aid verification in an electronic design automation (EDA) system, the method comprising:
- accessing trace data of a hardware design, wherein the trace data is a sequence of recorded netlist node values of the hardware design, obtained while the hardware design executed one or more tests;
- accessing a predetermined set of predicates of the hardware design by a computer, wherein each predicate represents a Boolean relation among netlist nodes in the hardware design;
- projecting the trace data over the set of predicates by a computer to generate a second trace;
- computing a set of states based on the second trace by the computer, wherein each state is a complete assignment of the set of predicates at one moment in time;
- producing a set of logical consequences from the set of states by the computer;
- and
- enumerating each logical consequence as an assertion by the computer.
A computer readable storage medium having embodied thereon a program, the program being executable by a processor to perform a method for generating assertions of a hardware design, the method comprising:
- accessing trace data of a hardware design, wherein the trace data is a sequence of recorded netlist node values of the hardware design, obtained while the hardware esign executed one or more tests;
- accessing a predetermined set of predicates of the hardware design by a computer, wherein each predicate represents a Boolean relation among netlist nodes in the hardware design;
- projecting the trace data over the set of predicates by a computer to generate a second trace;
- computing a set of states based on the second trace by the computer, wherein each state is a complete assignment of the set of predicates at one moment in time;
- producing a set of logical consequences from the set of states by the computer;
- and
- enumerating each logical consequence as ar assertion by the computer.
An apparatus for generating assertions of a hardware design, the apparatus comprising:
- a processor;
- memory;
- a first set of instructions stored in memory and executed by the processor to project trace data of a hardware design over a predetermined set of predicates of the hardware design, the trace data is a sequence of recorded netlist node values of the hardware design, obtained while the hardware design executed one or more tests, each predicate representing a Boolean relation among netlist nodes in the hardware design;
- a second set of instructions stored in memory and executed by the processor to compute a set of states based on the second trace, wherein each state is a complete assignment of the set of predicates at one moment in time;
- a third set of instructions stored in memory and executed by the processor to produce a set of logical consequences from the set of states by the computer;
- and
- a fourth set of instructions stored in memory and executed by the processor to enumerate each logical consequence as an assertion by the computer.
Dependencies are inferred from the claim text.