An Integrated
Framework for Formal Verification
and Distributed Simulation of Asynchronous Hardware

This project developed
a practical integrated framework for the analysis of asynchronous
hardware designs via formal verification and distributed
simulation. The project addressed weaknesses of the simulation for
asynchronous systems (particularly its failure to deal with
non-determinacy and deadlock detection) by exploiting the
particular suitability of asynchronous systems for formal
verification.
The system was implemented as an enhancement of the Balsa
synthesis toolkit, developed by the APT/AMULET
Group at Manchester. The core of the framework was
based on the process algebra CSP for maximum flexibility and
reusability of the methods. CSP has an underlying mathematical
theory and inherent parallelism, features that can be exploited to
perform both formal verification and distributed simulation. The
Framework implements Formal verification of properties such as
deadlock and equivalence checking through the translation of Balsa
into machine readable CSP, invoking the model checker FDR and
back-translating the diagnostics. Distributed simulation
ensures timing analysis of Balsa designs and performance
evaluation of benchmark programs. This project investigated the
applicability of semi-formal verification approaches, hybrid
combinations of formal verification and simulation, in the context
of asynchronous hardware. The framework will be evaluated on major
asynchronous hardware designs, such as the Amulet3i processor
aimed at embedded systems.
This was a
collaborative project with Stephen
Furber's APT/AMULET
Group at the University of Manchester and was funded by
EPRSC (Project No. GR/S11091/01 & GR/S11084/01).
People
- Professor Georgios Theodoropoulos (Principal Investigator, University of Birmingham)
- Dr Doug
Edwards (Principal Investigator, University of
Manchester)
- Professor Marta Kwiatkowska (Co-Investigator, University of Birmingham)
- Dr Xu
Wang (PostDoc, University of Birmingham)
- Dr Lilian
Janin
(PhD student, University of Manchester)
- Dr Ilias
Tsirogiannis (PhD Student, University of Birmingham)
- Dr Qianyi Zhang (PhD Student, University of Birmingham)
Distributed Simulation
The
project developed the PARBREEZE system, a Distributed discrete
event simulation engine for CSP/Balsa designs. This strand of the
work developed also new partitioning algorithms for
asynchronous CSP/Balsa circuits.
Formal Verification - Case Studies
- CSP delay-insensitivity verification of the False Variable circuit redesign using FDR (see script).
- CSP deadlock checking of the Instruction fetching phase of a simplified Balsa asynchronous processor using FDR (see script).
- CSP verification of SAMIPS distributed coloring algorithm using FDR (see script).
- CSP verification of a (balanced) tree arbiter using FDR (see script).
- CSP verification of a control circuit for counterflow pipeline (see script)
Publications
- E. Tsirogiannis, G. Theodoropoulos, "Profiling Multilevel Partitioning for Asynchronous VLSI Distributed Simulation", 13th International Conference on Systems Simulation, (AsiaSim2013), Concorde Hotel, Singapore, 6 – 8 November 2013, Communications in Computer and Information Science (CCIS) Series, Springer, pp. 310-324, doi: 10.1007/978-3-642-45037-2_29
- E. Tsirogiannis, G. Theodoropoulos, D. Chen, Q. Zhang, L. Janin, D. Edwards, “A Framework for Distributed Simulation of Asynchronous Handshake Circuits”, 39th IEEE Annual Simulation Symposium, Part of the 2006 Spring Simulation Multiconference Huntsville, Alabama, April 2-6, 2006. Pages: 214-222, ISBN ~ ISSN:1080-241X , 0-7695-2559-8. doi: 10.1109/ANSS.2006.5
- Wang, X., Kwiatkowska, M., Theodoropoulos, G., Zhang, Q., “Opportunities and Challenges in Process-Algebraic Verification of Asynchronous Circuit Designs”, Electronic Notes in Theoretical Computer Science, Volume 146, Issue 2, 26 January 2006, Pages 189-206. Based on a paper presented at the 2nd Workshop on Globally Asynchronous, Locally Synchronous Design (FMGALS05), July 15, 2005, Verona, Italy. doi: 10.1016/j.entcs.2005.05.042
- Wang, X., Kwiatkowska, M., Theodoropoulos, G., Zhang, Q., “Towards a Unifying CSP Framework for Hierarchical Verification of Asynchronous Hardware”, Electronic Notes in Theoretical Computer Science, Volume 128, Issue 6, 23 May 2005. Elsevier. Pages 231-246. Based on a paper presented at the 4th International Workshop on Automated Verification of Critical Systems (AVoCS 2004), 4 September 2004 London. doi: 10.1016/j.entcs.2005.04.014