US 11,055,460 B1
Input-directed constrained random simulation
Ali Abdi, Haifa (IL); and Guy Eliezer Wolfovitz, Haifa (IL)
Assigned to CADENCE DESIGN SYSTEMS, INC., San Jose, CA (US)
Filed by Cadence Design Systems, Inc., San Jose, CA (US)
Filed on May 21, 2020, as Appl. No. 16/880,311.
Int. Cl. G06F 30/30 (2020.01); G06F 30/3323 (2020.01); G06F 30/3308 (2020.01); G06F 30/33 (2020.01); G06F 111/04 (2020.01); G06F 111/08 (2020.01); G06F 119/16 (2020.01)
CPC G06F 30/3323 (2020.01) [G06F 30/33 (2020.01); G06F 30/3308 (2020.01); G06F 2111/04 (2020.01); G06F 2111/08 (2020.01); G06F 2119/16 (2020.01)] 20 Claims
OG exemplary drawing
 
1. A method for input-directed constrained random simulation, the method comprising:
obtaining an initial state for a finite state machine (FSM) that models an electronic circuit design under test (DUT), the initial state assigning values to registers of the DUT, by providing, to a satisfiability problem (SAT) solver, an initial state function I(s) relating to the FSM, to obtain register values that satisfy the initial state function;
constructing a random Boolean circuit R(i);
querying the SAT solver or a different SAT solver for a satisfying assignment for a conjoined expression providing a conjunction of at least a valid-transition Boolean circuit T(s, i, s′) and the random Boolean circuit R(i), the valid-transition Boolean circuit describing valid transitions of the FSM as a function of current state s, inputs i, and next state s′; and
adding the satisfying assignment to the end of a constructed trace.