Automated Verification of Asynchronous Circuits Using Circuit Petri Nets

  1. Lookup NU author(s)
  2. Ivan Poliakov
  3. Dr Andrey Mokhov
  4. Ashur Rafiev
  5. Dr Danil Sokolov
  6. Professor Alex Yakovlev
Author(s)Poliakov I, Mokhov A, Rafiev A, Sokolov D, Yakovlev A
Editor(s)
Publication type Conference Proceedings (inc. Abstract)
Conference Name14th IEEE International Symposium on Asynchronous Circuits and Systems
Conference LocationNewcastle upon Tyne
Year of Conference2008
Date7-11 April 2008
Volume
Pages161-170
ISBN9780769531076
Full text is available for this publication:
To detect problematic circuit behaviour, such as potential hazards and deadlocks, in a reasonable amount of time a technique is required which would avoid exhaustive exploration of the state space of the system. Many of the existing methods rely on symbolic traversal of the state space, with the use of binary decision diagrams (BDDs) and associated software packages. This paper presents an alternative approach of using a special type of Petri nets to represent circuits. An algorithm for automatic conversion of a circuit netlist into a behaviourally equivalent Petri net is proposed. Once the circuit Petri net is constructed and composed with the provided environment specification, the presence and reachability of troublesome states is verified by using methods based on finite prefixes of Petri net unfoldings. The shortest trace leading to a deadlock or a hazard in the circuit Petri net is mapped back onto the gate-level representation of the circuit, thus assisting a designer in solving the problem. The method has been automated and compared against previously existing circuit verification tools.
PublisherIEEE Computer Society Press
URLhttp://dx.doi.org/10.1109/ASYNC.2008.18
DOI10.1109/ASYNC.2008.18
ActionsLink to this publication
Library holdingsSearch Newcastle University Library for this item