Patent ID: 7260800
Filing Date: 2007-08-21
Classification: G06F

Abstract:
1. A method of initializing a first representation derived from a high-level model, for formal analysis, comprising: indicating a location, in the high-level model, where the high-level model is initialized; executing the high-level model; intercepting procedure calls related to memory allocation, resulting from execution of the high-level circuit model, with a first collection of procedures that produces a collection of memory allocation information; halting execution of the high-level model at the indicated location to obtain a partially executed high-level model; initializing the first representation, which involves determining a first initial value for the first representation by extracting a first value, from the partially executed high-level model, using the collection of memory allocation information wherein the determine a first initial value further comprises: identifying the first value as corresponding to a first location in the first representation; identifying a second value, of a second model, as corresponding to a second location in the first representation; determining the first initial value for the first location and a second initial value for the second location to be equal to a common value if the first value and the second value are equal applying a method of formal analysis to the first representation, wherein the partially executed high-level model produces the initial value for the first representation.