Guided exploration of circuit design states

摘要

A model checking tool, which is used to test a circuit design, attempts to reach a target state from an initial state in the state-space of the circuit design using one or more intermediate states. Through an iterative process, the tool identifies intermediate states in the state-space of the circuit design that are used to generate starting states for subsequent iterations of the process. The intermediate states help to restrict the scope of the state-space search to reduce the time and memory requirements needed to reach the target state. The model checking tool also explores the state-space in parallel from a subset of computed restart states, which reduces the possibility of bypassing any essential intermediate or target states.

主权项

1. A method for testing a circuit design, the method comprising:
receiving a circuit design encoded in a hardware description language; receiving a target state definition and a plurality of intermediate state definitions, wherein the plurality of intermediate state definitions include user-specified intermediate state definitions; exploring, by a model checking tool, a state-space of the circuit design with bounded model checking by traversing the state-space of the circuit design to identify one or more intermediate states that satisfy one or more of the plurality of intermediate state definitions; exploring, by the model checking tool, the state-space of the circuit design with bounded model checking to identify a target state that satisfies the target state definition, the state-space explored in parallel from a plurality of starting states in the state-space of the circuit design, wherein at least one starting state is determined from the one or more intermediate states; and outputting a result of exploring the state-space of the circuit design to identify the target state, wherein the result includes an indication of whether or not the target state is reachable.