Gate-level modelling and verification of asynchronous circuits using CSP_M and FDR
- When?
- Thursday 1 February 2007, 14:00
- Open to:
- Staff, Students
Professor mark Josephs, London South Bank University
Abstract:
The switching behaviour of asynchronous circuits involves input/output elements (such as AND gates, Muller C elements and Mutual Exclusion elements) that compute and communicate 'signal transitions'.
It is desirable that such circuits should function correctly without making any timing assumptions about the speeds of their elements and transmission delays in the wires that connect them, though sometimes it is necessary to assume that certain forks are 'isochronic'. We shall see how to model asynchronous elements and circuits as processes in CSP_M and how to verify them using FDR: processes abstract away from the speed of the elements; a process parameterised by a Boolean function suffices to model any complex gate; another such process models mutual exclusion; multi-way synchronisation facilitates the modelling of isochronic forks; process transformations allow one to model transmission lines and handshaking ports. The approach is illustrated on several asynchronous circuits drawn from the literature.
Notes:
Mark Josephs received the B.Sc. (Hons) degree in Mathematics from University College, London, in 1983 and the M.Sc. and D.Phil. degrees in Computation from the University of Oxford in 1984 and 1986, respectively. He spent 1987 as a Visiting Scientist at IBM Yorktown Heights before returning to the Computing Laboratory, University of Oxford, as a postdoctoral researcher. Concurrent appointments during the next five years included a Lecturership in Computation at Trinity College, Oxford, and a Visiting Fellowship at Eindhoven University of Technology. He subsequently moved to South Bank University, London, where the title of Professor of Computing was conferred upon him in 1998. In 2001 he was elected a Senior Member of the Institute of Electrical and Electronics Engineers, and in 2004 he was elected a Member of the UK Computing Research Commitee and a Chartered Fellow of the British Computer Society. On sabbatical in 2005/6, he spent part of the year at the California Institute of Technology as a Visiting Associate. He is currently Director of the Institute for Computing Research at London South Bank University.
