Method and system for formal bug hunting
AssigneeCadence Design Systems, Inc.
InventorsYaron Schiller, Guy Wolfovitz, Habeeb Farah
Life of this patent
Estimating the term…
Abstract
A method for formal deep bug hunting in a device under test (DUT) may include obtaining a selection of a start state for the DUT; obtaining a selection of one or a plurality of variables that are declared as random variables; for each of said one or a plurality of random variables, generating a sequence of random values in a generation order using a random number generator (RNG); and performing formal verification exploration of the DUT starting at the start state and consecutively assigning each of said one or a plurality of random variables a value from the sequence of values in the generation order.
Claims14
A computer implemented method for formal deep bug hunting in a device under test (DUT) comprising:
- using a processor, obtaining a start state for the DUT;
- using the processor, obtaining a subset of one or a plurality of variables from a plurality of variables of the DUT;
- setting the subset of the one or a plurality of variables to one or a plurality of random variables;
- for each of said one or a plurality of random variables, generating a sequence of random values in a generation order using a random number generator (RNG) using a dedicated seed for the RNG for each random variable of said one or a plurality of random variables;
- performing formal verification exploration of the DUT starting at the start state and consecutively assigning each of said one or a plurality of random variables a value from the sequence of values in the generation order, wherein the consecutively assigning comprises assigning that value at a clocking event of an assumption set relating to that random variable;
- and
- finding one or more bugs if present in the DUT.
A system for formal bug hunting, the system comprising:
- memory;
- and
- a processor configured to:
- obtain a subset of one or a plurality of variables from a plurality of variables of the DUT;
- set the subset of one or a plurality of variables to one or a plurality of random variables;
- for each of said one or a plurality of random variables, generate a sequence of random values in a generation order using a random number generator (RNG) using a dedicated seed for the RNG for each random variable of said one or a plurality of random variables;
- perform formal verification exploration of the device under test (DUT) starting at a start state and consecutively assigning each of said one or a plurality of random variables a value from the sequence of values in the generation order, wherein the consecutively assigning comprises assigning that value at a clocking event of an assumption set relating to that random variable;
- and
- find one or more bugs if present in the DUT.
A non-transitory computer readable storage medium for formal bug hunting, having stored thereon instructions that when executed by a processor will cause the processor to:
- set a subset of one or a plurality of variables of a device under test (DUT) to one or a plurality of random variables;
- for each of one or a plurality of random variables of the DUT, generate a sequence of random values in a generation order using a random number generator (RNG) using a dedicated seed for the RNG for each random variable of said one or a plurality of random variables;
- perform formal verification exploration of the DUT starting at a selected start state and consecutively assigning each of said one or a plurality of random variables a value from the sequence of values in the generation order, wherein the consecutively assigning comprises assigning that value at a clocking event of an assumption set relating to that random variable;
- and
- find one or more bugs if present in the DUT.
Dependencies are inferred from the claim text.