Formal verifying method for development in data processor involves executing verification algorithm using one limit of signal envelope, and limiting state-space search by using verification algorithm

摘要

A tracing program is determined by using a verification algorithm. The result of the determination of the tracing program is indicated on a graphical user interface. One limit of a signal envelope is then changed. The execution of the verification algorithm is then performed by using one limit of the signal envelope, and a state-space search is limited by the use of the verification algorithm. Independent claims are also included for the following: (a) a device for formal verification of development in data processor; (b) and a computer program for formal verification of development in data processor.