Name
Abstract | ||
|---|---|---|
Modern computer systems rely more and more on on-chip communication protocols to exchange data. To meet performance requirements these protocols have become highly complex, which usually makes their formal verification infeasible with reasonable time and effort. We present a new refinement approach to on-chip communication protocols that combines design and verification together, interleaving them hand-in-hand. Our modeling framework consists of design steps and design transformations formalized as finite state machines. Given a verified design step, transformations are used to extend the system with advanced features. A design transformation ensures that the extended design is correct if the previous system is correct. This approach is illustrated by an arbiter-based master-slave communication system inspired by the AMBA High-performance Bus architecture. Starting with a sequential protocol design, it is extended with pipelining and burst transfers. Transformations are generated from design constraints providing a basis for correctness-by-design of the derived system. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/FMCAD.2008.ECP.22 | FMCAD |
Keywords | Field | DocType |
design constraint,modern computer system,sequential protocol design,extended design,communication protocol,design step,design transformation,on-chip communication protocol,previous system,refinement approach,arbiter-based master-slave communication system,registers,finite state machines,communication system,chip,data exchange,automata,finite state machine,system on a chip,protocols,formal verification,system on chip,integrated circuit design,communication systems,master slave | Functional verification,Arbiter,System on a chip,Computer science,Communications system,Finite-state machine,Real-time computing,Integrated circuit design,Formal verification,Communications protocol | Conference |
Citations | PageRank | References |
6 | 0.54 | 12 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Peter Böhm | 1 | 20 | 2.99 |
| Thomas F. Melham | 2 | 384 | 35.63 |