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

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

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