Constrained random simulation coverage closure guided by a cover property

A circuit verification system which biases input stimuli for a circuit to satisfy one or more temporal coverage properties to be verified for the circuit, comprising:

• a conversion mechanism configured to convert a respective temporal coverage property into a corresponding finite state automaton (FSA) and into a corresponding collection of soft constraints, wherein the corresponding collection of soft constraints defines allowable transitions across the FSA;
• and
• a testbench environment configured to perform a simulation in which random input stimuli are applied to the circuit, wherein the testbench environment performs the simulation by:
• using an FSA instance for a temporal coverage property to observe inputs and outputs of the circuit, wherein the FSA instance includes a sequence of states which satisfy the temporal coverage property, and wherein using the FSA instance involves concurrently using multiple FSA instances associated with one or more temporal coverage properties to observe the inputs and outputs of the circuit;
• and
• using soft constraints associated with the FSA instance to bias input stimuli for the circuit so that the simulation is likely to progress through the sequence of states.

A non-transitory computer-readable storage medium storing instructions that when executed by a computer cause the computer to perform a method for verifying a circuit which biases input stimuli for the circuit to satisfy one or more temporal coverage properties to be verified for the circuit, comprising:

• performing a simulation in which random input stimuli are applied to the circuit;
• wherein performing the simulation involves,
• using a finite state automaton (FSA) instance for a temporal coverage property to observe inputs and outputs of the circuit, wherein the FSA instance includes a sequence of states which satisfy the temporal coverage property, and wherein using the FSA instance involves concurrently using multiple FSA instances associated with one or more temporal coverage properties to observe the inputs and outputs of the circuit, and
• using soft constraints associated with the FSA instance to bias input stimuli for the circuit so that the simulation is likely to progress through the sequence of states.