Amazon Technologies, Inc.

Todd Swanson

Ron Diamant

Thomas A Volpe

Nishith Desai

Formal verification methods are used to solve a valid model of a design-under-test (DUT) to enumerate valid coverage points based on an architectural specification of the DUT. A formal solver can be queried to solve for valid solutions by crossing one or more fields of a variable. After each valid solve, values of the variable fields can be recorded and a count for number of valid solutions can be incremented. A new rule can be added to the solving process after each valid solve to invalidate the recorded values of the variable fields for subsequent solves. The count for the number of valid solutions can provide a running total of the valid solutions found for the query. Results of the query can be processed to convert the recorded values to provide the enumerated coverage points. The enumerated coverage points can be converted to test cases for running simulations on the DUT.

Enumerating coverage based on an architectural specification

Systems and methods for power analysis of a hardware device design. In various examples, a target circuit can be defined within the hardware device design. The target circuit can include a plurality of digital circuit elements linking a plurality of input nodes with a plurality of output nodes. A solver can be used to search for a transition pattern that, when applied to the input nodes, causes a number of output nodes equal to a counter to transition from a first binary value to a second binary value. If a transition pattern cannot be found, the counter is decremented and a new transition pattern is searched for. Once a transition pattern is found, it is determined whether the transition pattern satisfies a constraint.

Growing community of inventors

Pflugerville, TX, United States of America

Todd Swanson