VERification-Driven Asynchronous Design (VERDAD)

Lead Research Organisation: Newcastle University
Department Name: Computing Sciences

Abstract

This project redefines conventional asynchronous VLSI tool flows, by incorporating verification into the heart of the design process. Assertion-based verification is used to drive the synthesis procedure by analysing the behaviour of circuits to prove properties which may be exploited for optimisation. Using verification as part of the synthesis procedure represents a major paradigm shift from existing approaches where the validity of optimisations is determined statically and verification is performed after synthesis. Combining synthesis and verification will provide practical and theoretical advances in both areas extending beyond the focus of the project domain. Results of the project will be disseminated into the VLSI community in the form of tutorials and workshops with the aim of promoting asynchronous circuits as an effective solution to the problem of process variation.
 
Description The following research contributions have been made during this project:
• A verification method based on a novel condensed representation of the set of reachable states of the system, called Merged Processes, has been developed and implemented in software tools PUNF and MPSAT.
• A new formalism, called the algebra of Parameterized Graphs, has been developed, and its applicability to the microelectronics design has been demonstrated on several case studies, including the design of a simple processor instruction set.
• A new algorithm for decomposition of Signal Transition Graphs has been developed and implemented in the DESIJ tool; this algorithm is essential for synthesising large asynchronous controllers.
• A new method for computing the optimised parallel composition of labelled Petri nets (in particular, Signal Transition Graphs) has been developed and implemented in the tool PCOMP. Its main advantage is that it allows producing Petri nets with fewer redundant places, without incurring any significant overhead in terms of the runtime. Such Petri nets are advantageous for the decomposition algorithm (see above).
• An algorithm for logic decomposition of asynchronous circuits based on Petri net unfoldings has been developed and implemented in MPSAT.
• A method for asynchronous circuit re-synthesis has been implemented in the WORKCRAFT tool.
• An automated approach to synthesis of robust controllers for sub-threshold digital systems based on dual-rail implementation of control logic has been proposed and implemented in the MPSAT tool.
• A new way of constructing N-way arbiter circuits have been proposed. The main idea is to perform arbitrations between all pairs of requests, and then make decision on what grant to issue based on their outcomes. Crucially, all the mutual exclusion elements in such an arbiter work in parallel. This 'flat' arbitration is prone to new threats such as formation of cycles (leading to deadlocks), and thus special care has to be taken to cope with such situations.
• A polynomial translation of Finite Control Processes (an important decidable fragment of pi-calculus) to safe Petri nets have been developed and implemented in the FCP2PN tool. This allows for verification of systems with mobility using efficient techniques for Petri nets.
• Theoretical contributions to the theory of concurrency have been made, including the definition of semantics and the development of synthesis algorithms for several concurrency models.
• A method for efficient verification of the Diagnosability and Predictability properties using parallel LTL-X model checking based on Petri net unfoldings has been developed and implemented in the PUNF tool.
Exploitation Route The tools developed during this project have direct applications in the area of microelectronics design, and the links to the other existing tools make the industrial adoption quite straightforward.
Sectors Digital/Communication/Information Technologies (including Software),Education,Electronics
 
Description The software developed during this project has been used, and is now used, in industry and academia, including delivery of a course at Newcastle University.
First Year Of Impact 2011
Sector Education,Electronics
 
Title An Algorithm for Direct Construction of Complete Merged Processes 
Description Merged processes are a recently proposed condensed representation of a Petri net's behaviour similar to branching processes (unfoldings), which copes well not only with concurrency, but also with other sources of state space explosion like sequences of choices. They are by orders of magnitude more compact than traditional unfoldings, and yet can be used for efficient formal verification. However, constructing complete merged processes is difficult, and the only known algorithm was based on building a (potentially much larger) complete unfolding prefix of a Petri net, whose nodes are then merged. Obviously, this significantly reduces their appeal as a representation that can be used for practical verification. As a part of VERDAD project, we have developed an algorithm that avoids constructing the intermediate unfolding prefix, and builds a complete merged process directly from a Petri net. In particular, a challenging problem of truncating a merged process is solved. 
Type Of Material Computer model/algorithm 
Year Produced 2011 
Provided To Others? Yes  
Impact This algorithm was implemented in the MPSAT tool, which is a part of Workcraft framework. Please see the MPSAT and Workcraft impact in the software section. 
 
Title FCP2PN 
Description A tool implementing a polynomial translation of Finite Control Processes (an important subset of pi-calculus) to safe Petri nets. This allows for verification of systems with mobility using efficient techniques for Petri nets. 
Type Of Technology Software 
Year Produced 2012 
Impact FCP2PN tool was an implementation of the polynomial translation of Finite Control Processes (an important subset of pi-calculus) to safe Petri nets, that demonstrated its practicality. The possibility of a polynomial translation is of major theoretical importance. We are not aware of any "practical" impact. 
URL http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/fcp2pn/
 
Title MPSAT 
Description Verification tool based on merged processes. 
Type Of Technology Software 
Year Produced 2011 
Impact MPSAT is included as a back-end into Workcraft framework, which has a high impact - please see the Workcraft entry in this section. 
URL http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/UnfoldingTools/current/
 
Title PCOMP 
Description Tool for computing the optimised parallel composition of labelled Petri nets 
Type Of Technology Software 
Year Produced 2011 
Impact PCOMP is included as a back-end into Workcraft framework, which has a high impact - please see the Workcraft entry in this section. 
URL http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/UnfoldingTools/current/
 
Title PUNF 
Description Tool for building merged processes, which are used for formal verification. 
Type Of Technology Software 
Year Produced 2011 
Impact PUNF is included as a back-end into Workcraft framework, which has a high impact - please see the Workcraft entry in this section. 
URL http://homepages.cs.ncl.ac.uk/victor.khomenko/tools/UnfoldingTools/current/
 
Title Workcraft 
Description Workcraft is designed to provide a flexible common framework for development of Interpreted Graph Models, including visual editing, (co-)simulation and verification. The tool is platform-independent, highly customisable by means of plug-ins, and is freely available for academic use. 
Type Of Technology Software 
Year Produced 2011 
Impact * Workcraft framework is used by industry for designing electronic circuits * Workcraft framework is used in teaching the theory of concurrency course in the School of Computing Science, Newcastle University 
URL http://workcraft.org