Patent ID: 6985840

Claim:
An apparatus for verifying that a circuit specification describes a circuit exhibiting a property defined as a consequent behavior occurring during clock cycles 1 through N of a clock signal following an antecedent event, wherein N is an integer greater than 0, wherein the circuit responds to input signals by producing output signals, wherein the antecedent event is a first state change pattern in at least one of the input and output signals, and wherein the consequent behavior is production of a second state change pattern in at least one of the output signals, the apparatus comprising: a circuit simulator for implementing a simulated circuit, wherein the simulated circuit simulates the circuit described by the circuit specification, wherein the circuit simulator produces output waveform data representing time-varying behavior of the input and output signals and representing a current state of the simulated circuit; detector means for detecting in the output waveform data an occurrence of a data pattern representing the antecedent event; and means for generating a temporally expanded model of the simulated circuit based on the circuit specification and on a state of the circuit upon the occurrence of data pattern as indicated by the output waveform data, the temporally expanded model representing the circuit as a set of N circuit functions CKT 1 –CKT N , each corresponding to a separate one of the N clock cycles and each representing behavior of the circuit during its corresponding clock cycle.