Motorola Corporation

Matthew J Kaufmann

Andrew Kenneth Martin

Carl P Pixley

A method is presented for performing model checking of an integrated circuit design that avoids the need for construction of an environment model by the use of constraints (44). The method supports an assume/guarantee style of reasoning to ensure that the constraints (44) are a true abstraction of the actual environment in which the integrated circuit is designed to operate. The constraints (44) may be used to provide primary inputs for a design under analysis (DUA) (16). Also, the constraints (44) may refer to internal states and to outputs of the DUA (16). In addition, monitors (42) may be used to monitor the inputs to the DUA (16). The constraints (44) can then be used with the monitors (42) to specify complex sequential environment properties.

Growing community of inventors

Austin, TX, United States of America

Matthew J Kaufmann