caa a22 4500 475797450 CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000101xx s 000 0 eng 10.1023/A:1008773308108 doi (NATIONALLICENCE)springer-10.1023/A:1008773308108 Eiríksson Ásgeir Silicon Graphics Inc., Mountain View, California, USA aut The Formal Design of 1M-gate ASICs [Elektronische Daten] [Ásgeir Eiríksson] Refinement of a directory based cache coherence protocol specification, to a pipelined hardware implementation is described. The hardware that is analyzed is the most complex part of a 1M-gate ASIC. The design consists of 30,000 lines of synthesizable register transfer-level verilog code, amounting to approximately 200,000 gates. The design contains a pipeline that is 5 levels deep and approximately 150 bits wide. It has a 16 entry, 150 bit wide, context addressable memory (CAM), and includes a 256 × 72 bit RAM. Refinement maps relate the behavior of the high-level protocol model to the hardware implementation. The Cadence Berkeley Labs SMV model checker was used to create the maps and to prove their correctness. There are approximately 1500 proof obligations. The formal model has been used for three tasks. First, to formally diagnose, and then fix broken features in a legacy version of the design. Second, to integrate the legacy sub-system design with a new system design. Finally, it has been used to formally design additional sub-system features required for the new system design. The same hardware designer enhanced the design, created the refinement maps, and formally proved the correctness of the refinements. Kluwer Academic Publishers, 2000 model checking nationallicence refinement nationallicence formal design nationallicence Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 7-22 0925-9856 16:1<7 2000 16 10703 https://doi.org/10.1023/A:1008773308108 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008773308108 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Eiríksson Ásgeir Silicon Graphics Inc., Mountain View, California, USA aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/1(2000-01-01), 7-22 0925-9856 16:1<7 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer