VERification-Driven Asynchronous Design (VERDAD)
Lead Research Organisation:
University of Manchester
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Publications
Balasubramanian P
(2012)
Redundant Logic Insertion and Latency Reduction in Self-Timed Adders
in VLSI Design
BALASUBRAMANIAN P
(2013)
SELF-TIMED SECTION-CARRY BASED CARRY LOOKAHEAD ADDERS AND THE CONCEPT OF ALIAS LOGIC
in Journal of Circuits, Systems and Computers
P Balasubramanian (Author)
(2010)
Self-Timed Realization of Combinational Logic
Ren H
(2011)
Structure-Based Deadlock Checking of Asynchronous Circuits
in Journal of Computer Science and Technology
Toms W
(2011)
Indicating combinational logic decomposition
in IET Computers & Digital Techniques
| Description | The following research contributions have been made during this project: Techniques to synthesise petri-net models have been added to the Teak synthesis system to allow petri-net models of Teak descriptions to be synthesised and verified using unfolding tools PUNF and MPSAT. The petri-net models were used to identify errors in the existing Teak latch insertion scheme that causes deadlock under certain conditions and a new deadlock free scheme was implemented and validated using the models A structural based deadlock detection scheme was created which can identifies malformed structures in Teak circuits which may cause deadlocks. Structural techniques have an order of magnitude performance increase over reachability-based techniques. New performance based latch insertion schemes have been developed that analyse the delay of cycles within Teak circuits to optimise the performance of synthesised circuits showing 40% improvement over existing techniques A new formalism for constructing quasi-delay insensitive combinational logic circuits was developed, the formalism determines the conditions necessary for technology-independent implementation of any QDI CL circuit. Exact and heuristic algorithms were created to efficiently synthesise any m-of-n encoded QDI combinational logic circuit. A formal definition for block-level relaxation was defined for arbitrarily encoded QDI CL circuits and algorithms were developed to synthesise relaxed QDI CL circuits A multi-level synthesis system was defined for QDI CL circuits that allows minimised implementations of arbitrary encoded QDI circuits to be created. Formal proofs were defined to ensure that all of the optimisations applied during the synthesis process uphold the QDI property. |
| Exploitation Route | All the tools developed during the project have direct applications in the area of microelectronics and there should be few barriers to their adoption in a commercial context The software developed during the project will be made publicly available under a GPL license. The Teak synthesis system is being actively used by several sites globally leading to publications from institutions in Brazil and China. The developments undertaken in this project are being exploited in the GAELS EPSRC project (EP/I038306/1). |
| Sectors | Electronics |
| Description | A R M Ltd |
| Organisation | Arm Limited |
| Country | United Kingdom |
| Sector | Private |
| Start Year | 2006 |
| Description | Elastix |
| Organisation | Elastix |
| Country | Ecuador |
| Sector | Private |
| PI Contribution | N |
| Collaborator Contribution | N |
| Impact | N |
| Start Year | 2009 |