M. Azizi, X. Song, and E.-M. Aboulhamid
Formal verification, model checking, VIS, cache coherence, BDD, multiprocessor systems, Verilog, CTL, properties, implementation, specification, FSM
This article presents a case study on verifying formally a multi- processor system with shared memory using the model-checking technique. The system consists of a set of processors where each processor has its own cache, the shared main memory and the bus. The RTL (Register Transfer Level) design of the system is described in a Verilog-HDL code, and the behaviour is specified by a set of CTL (Computation Tree Logic) properties. We establish the effect of data width upon the reachability analysis. We successfully verify a set of critical safety and liveness properties for the system design. The experiments demonstrate the effectiveness of our methods. The verification results manifest the relationship between the state space, BDD (Binary Decision Diagram) size, and the verification time when the data width and the number of processors increase.
Important Links:
Go Back
