Verification of electronic systems
Alberto Luigi Sangiovanni-Vincentelli, Patrick C. McGeer, A. Saldanha · 1996
ion, which eliminates details that are of no importance when checking whether a design satisfies a particular property. ffl Decomposition, which consists of breaking the design at a given level of the hierarchy into components that can be designed and verified almost independently. These mechanisms can be applied to different classes of designs: from embedded controllers to computers, from microprocessors to digital-to-analog converters. They are not only useful in the verification process but also in the design process per se making verification itself unnecessary in some cases. For example, formalization of the design specifications is required for formal verification but it also helps in design transfer between different organizations eliminating the risk of losing knowledge about the design and its specifications, thus making verification before and after the transfer unnecessary. We argue that almost all advances in verification stem from the application of these three basic con...