A SYSTEM AND METHOD FOR VERIFYING LOGICAL, ARITHMETIC AND TIMING DEPENDENCIES OF SYSTEM BEHAVIORS USING CONSTRAINT CALCULUS ANALYSIS

摘要

An apparatus and method for verifying system behavior using behavior-constraint-calculus analysis is disclosed. The apparatus accepts a first "known" constraint graph and a second "conjectured" constraint graph. The apparatus transforms the second graph in such a way that the resultant "verified" graph "accepts" only those paths that are implied by the first graph and appear in the second graph.