To search, Click below search items. |
| All Published Papers Search Service |
|
|
|
Title |
A Formal Verification Case Study for IEEE-P.896 Bus Arbiter by using A Model Checking Tool |
|
Author |
Katsumi Wasaki |
| Citation |
Vol. 7 No. 3 pp. 184-192 |
|
Abstract |
In this paper, we describe a case study of formal verification for a computer bus arbitration controller by using the temporal logic of model checking. The implementation of the verification uses the Berkeley-VIS model checking system. Futurebus is a multiprocessor system bus with an arbitration and control mechanism. We describe the verification of the arbitration controller of ""Futurebus'' (IEEE-P.896) in Verilog-HDL (Hardware Description Language). Using this method, we have verified all satisfied specifications by designing the general Futurebus under CTL (Computation Tree Logic) and using the VIS model checker. |
|
Keywords |
Formal Verification, Model Checking, Temporal Logic, Bus Arbiter, Hardware Description Languages |
|
URL |
