Formalizing abstraction mechanisms for hardware verification in higher order logic

摘要: ion is the process by which important properties of a complex object are isolated for further consideration or use and remaining ones ignored as being irrelevant to task at hand. An example procedural abstraction in programming. Once procedure has been defined, it treated an atomic operation with only one attribute: what does. The exact sequence computation steps achieve this operation—how does it—is [36]. Programming language constructs that support Another approach make specifications executable, so designer can run them gain confidence their accuracy (see [10,65,80]). This special case more general strategy evaluating deriving consequences them.