An Integrated Framework for Formal Verification

and Distributed Simulation

of Asynchronous Hardware

Partners

• University of Manchester
  • Dr Doug Edwards,
  • Dr Lilian Janin
• University of Birmingham
• Dr Georgios  Theodoropoulos
• Prof Marta Kwiatkowska,
• Dr Xu Wang
• Mr Ilias Tsirogiannis , PhD Student
• Ms Qianyi Zhang , PhD Student, (funded by the School of Computer Science, University of Birmingham)

Project Summary

The system will be implemented as an enhancement of an existing Balsa synthesis toolkit, developed by the AMULET group at Manchester, that already supports limited analysis of the designs via simulation. The core of the framework will be 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.

Previous approaches have been hampered by the fact that verification has been, by necessity, post-hoc. The CAD systems used for the specification and implementation of circuits have been divorced from the verification tools and have totally non-orthogonal underpinnings. In this proposal, Balsa is derived from CSP. Thus, there is the same theoretical basis in the synthesis tool and the verification tool.

Formal verification of properties such as deadlock and equivalence checking will thus be implemented through the translation of Balsa into machine readable CSP, invoking the model checker FDR and back-translating the diagnostics. Distributed simulation will ensure timing analysis of Balsa designs and performance evaluation of benchmark programs. The project will also investigate 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.

Aims and Objectives

• Exploit compositionality of designs to enable automatic support for refinement checking, equivalence checking and deadlock detection.
• Investigate applicability of data independence as a means to automate datapath abstraction and verification of parameterised component descriptions.
• Investigate applicability of semi-formal techniques in the context of asynchronous hardware.
• Develop algorithms and techniques for partitioning, load balancing, synchronisation approach  and monitoring to support the distributed simulation.
• Develop a prototype integrated environment for the specification, distributed simulation and formal verification of asynchronous VLSI systems.
• Develop test cases and conduct experiments to test and evaluate our approach.

Links

Publications

Case studies

Some conferences