A Methodology for the Formal Analysis of Asynchronous Micropipelines

Antonio Cerone and George Milne

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


In this paper we present a process algebra approach for the integrated verification of correctness and performance in concurrent systems. The verification procedure is entirely performed within the Circal process algebra, without any recourse to other formalisms. Performance is characterised in terms of logical properties, which do not incorporate explicit time. Such properties are then interpreted in terms of degree of concurrency and allow the quantitative evaluation of the throughput of the system. The approach has been applied to two four-phase handshaking protocols, which are motivated by the implementation of the AMULET2 asynchronous RISC processor. Both correctness and performance properties are captured in the same verification framework and automatically proved using the Circal System.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Maintainer sjohnson@cs.indiana.edu.
Start Conference Manager
Conference Systems