A simulation-based approach to architectural verification of multiprocessor systems
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper presents a simulation-based method for verifying coherency in weakly ordered shared memory multiprocessor systems. This methodology requires minimal assumptions regarding the implementation details, such as the coherence protocol and cache line replacement rules. Independence from implementation details for architectural verification is achieved via a technique called data-coloring. The non-determinism arising from weak ordering is resolved by introducing the notion of valid sets for checking the correctness of memory operations. We contrast our approach with other methods that have been prevalent in the industry and provide implementation details and an example implementation of our methodology.<>Keywords
This publication has 10 references indexed in Scilit:
- Weak ordering-a new definitionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- MPTG: a portable test generator for cache-coherent multiprocessorsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Multiprocessor system verification through behavioral modeling and simulationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Directions in multiprocessor verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal verification of sequential hardware: a tutorialIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1993
- Verification of the IBM RISC System/6000 by a dynamic biased pseudo-random test program generatorIBM Systems Journal, 1991
- Correct memory operation of cache-based multiprocessorsPublished by Association for Computing Machinery (ACM) ,1987
- Memory access buffering in multiprocessorsACM SIGARCH Computer Architecture News, 1986
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess ProgramsIEEE Transactions on Computers, 1979
- A New Solution to Coherence Problems in Multicache SystemsIEEE Transactions on Computers, 1978