Back to results
US 7,444,274 B1Granted
Method and system for verifying circuit designs through propagation of assertions
AssigneeCadence Design Systems, Inc.
InventorsManu Chopra, Xiaoqun Du, Alok Jain, Robert P. Kurshan, Franz Erich Marschner, Kavita Ravi
Life of this patent
Estimating the term…
Abstract
A method and system for verifying circuit designs through propagation of assertions within a circuit design. In an embodiment, a plurality of provided assertions a circuit design are propagated within the circuit design. The circuit design is then verified using at least one of the propagated assertions as an assumption.
Claims53
A computer implemented method for verifying a circuit design comprising:
- propagating a plurality of provided assertions as one or more groups of related assertions within a circuit design;
- classifying one assertion in each of the one or more groups of related assertions as a first requirement for verifying the circuit design, in which two assertions are related if the two assertions are propagated from a same provided assertion or one of the two assertions is propagated from the other of the two assertions;
- selecting a requirement from the first requirement of each of the one or more groups of related assertions to verify;
- isolating a portion of the circuit design containing the selected requirement;
- avoiding circular reasoning, in which an assumption is directly or indirectly used to prove itself;
- verifying the selected requirement in the isolated portion of the circuit design using one or more of the plurality of provided assertions not selected as the selected requirement in the isolated portion of the circuit design as one or more assumptions;
- and
- storing a result of the act of verifying the selected requirement in the isolated portion of the circuit design in a computer readable medium.
5 more elements
A system for verifying a circuit design comprising:
- means for propagating a plurality of provided assertions as one or more groups of related assertions within a circuit design;
- means for classifying one assertion in each of the one or more groups of related assertions as a first requirement for verifying the circuit design, in which two assertions are related if the two assertions are propagated from a same provided assertion or one of the two assertions is propagated from the other of the two assertions;
- means for selecting a requirement from the first requirement of each of the one or more groups of related assertions to verify;
- means for isolating a portion of the circuit design containing the selected requirement;
- means for avoiding circular reasoning, in which an assumption is directly or indirectly used to prove itself;
- means for verifying the selected requirement in the isolated portion of the circuit design using one or more of the plurality of provided assertions not selected as the selected requirement in the isolated portion of the circuit design as one or more assumptions;
- and
- means for storing a result of the act of verifying the selected requirement in the isolated portion of the circuit design in a computer readable medium.
5 more elements
A computer implemented method for verifying a circuit design comprising:
- propagating a plurality of provided assertions as one or more groups of related assertions within a circuit design;
- and
- verifying the circuit design using at least one of the propagated assertions as an assumption, wherein the act of verifying the circuit design comprises:
- classifying one assertion in each of the one or more groups of related assertions as a first requirement for verifying the circuit design, in which two assertions are related if the two assertions are propagated from a same provided assertion or one of the two assertions is propagated from the other of the two assertions;
- selecting a requirement from the first requirement of each of the one or more groups of related assertions to verify;
- isolating a portion of the circuit design containing the selected requirement;
- verifying the selected requirement in the isolated portion of the circuit design using one or more of the plurality of provided assertions not selected as the selected requirement in the isolated portion of the circuit design as one or more assumptions;
- and
- storing a result of the act of verifying the selected requirement in the isolated portion of the circuit design in a computer readable medium.
6 more elements
A system for verifying a circuit design, comprising:
- means for propagating a plurality of provided assertions as one or more groups of related assertions within a circuit design;
- and
- means for verifying the circuit design using at least one of the propagated assertions as an assumption, wherein the means for verifying the circuit design comprises:
- means for classifying one assertion in each of the one or more groups of related assertions as a first requirement for verifying the circuit design, in which two assertions are related if the two assertions are propagated from a same provided assertion or one of the two assertions is propagated from the other of the two assertions;
- means for selecting a requirement from the first requirement of each of the one or more groups of related assertions to verify;
- means for isolating a portion of the circuit design containing the selected requirement;
- means for verifying the selected requirement in the isolated portion of the circuit design using one or more of the plurality of provided assertions not selected as the selected requirement in the isolated portion of the circuit design as one or more assumptions;
- and
- means for storing a result of the act of verifying the selected requirement in the isolated portion of the circuit design in a computer readable medium.
6 more elements
A computer program product comprising a computer readable medium having executable code to execute a process for verifying a circuit design, the process comprising:
- propagating a plurality of provided assertions as one or more groups of related assertions within a circuit design;
- classifying one assertion in each of the one or more groups of related assertions as a first requirement for verifying the circuit design, in which two assertions are related if the two assertions are propagated from a same provided assertion or one of the two assertions is propagated from the other of the two assertions;
- selecting a requirement from the first requirement of each of the one or more groups of related assertions to verify;
- isolating a portion of the circuit design containing the selected requirement;
- avoiding circular reasoning, in which an assumption is directly or indirectly used to prove itself;
- verifying the selected requirement in the isolated portion of the circuit design using one or more of the plurality of provided assertions not selected as the selected requirement in the isolated portion of the circuit design as one or more assumptions;
- and
- storing a result of the act of verifying the selected requirement in the isolated portion of the circuit design in a computer readable medium.
5 more elements
A computer program product comprising a computer readable medium having executable code to execute a process for verifying a circuit design, the process comprising:
- propagating a plurality of provided assertions as one or more groups of related assertions within a circuit design;
- and
- verifying the circuit design using at least one of the propagated assertions as an assumption, wherein the act of verifying the circuit design comprises:
- classifying one assertion in each of the one or more groups of related assertions as a first requirement for verifying the circuit design, in which two assertions are related if the two assertions are propagated from a same provided assertion or one of the two assertions is propagated from the other of the two assertions;
- selecting a requirement from the first requirement of each of the one or more groups of related assertions to verify;
- isolating a portion of the circuit design containing the selected requirement;
- verifying the selected requirement in the isolated portion of the circuit design using one or more of the plurality of provided assertions not selected as the selected requirement in the isolated portion of the circuit design as one or more assumptions;
- and
- storing a result of the verifying act and the circuit design after the verifying the selected requirement in a computer readable medium for use in electronic circuit design or manufacturing.
6 more elements
Dependencies are inferred from the claim text.