PU Cache

the system using test programs executed by the PU. These test programs are often generated by advanced code generators using pseudo-random techniques[1, 2, 3]. The use of this approach alone is no longer sufficient when the supporting chips become more and more complex. Formal approaches have been proposed for verifying the supporting chips. For example, they are used to prove the correctness of the cache updates and so on [4, 5]. However, the size of the circuits which can be handled by such approaches is still too limited. This paper is organized as follows: Section 2 reviews the problem of verifying the bus controller ASICs for our multi-processor system. Section 3, presents the incremental verifica-tion approach used to verify our ASICs. In Section 4, the CAD tools will be introduced as used for hierarchically speci-fying the timing diagrams followed by the execution of the timing diagrams, such that the design parts are verified by a “controlled ” random simulation. In Section 5, the results are presented. Finally, in Section 6 our conclusions are given. 2. Verification of our Multiprocessor Systems Figure 1 shows the basic structure of the processor module of the third generation IBM S/390 CMOS processors. These modules form the processor core of the “IBM S/390 Parallel Enterprise Server- Generation 3 ” and the “IBM S/390 Multi-prise 2000 ” systems. These systems are the successors to ou