Ion, which eliminates details that are of no importancewhen checking whether a design satisfies a particularproperty.ffl Decomposition, which consists of breaking the design ata given level of the hierarchy into components that can bedesigned and verified almost independently.These mechanisms can be applied to different classes ofdesigns: from embedded controllers to computers, from microprocessorsto digital-to-analog converters. They are not onlyuseful in the verification process but ...