Conformance and mirroring for timed asychronous circuits

ABSTRACT

Conformance has been used as a correctness criterion for asynchronous circuits. In the case of untimed systems, conformance of an implementation to a specification is equivalent to the failure-freeness between the implementation and the mirror of the specification. For bounded-delay systems, in general this property does not hold. In this paper, we define various notions of failures and examine whether the above property holds or not. We then discuss an alternative and effective algorithm for conformance checking of bounded-delay asynchronous circuits.

REFERENCES

• 1: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
• 2: Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 3: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 4: Tomas Rokicki , Chris J. Myers, Automatic Verification of Timed Circuits, Proceedings of the 6th International Conference on Computer Aided Verification, p.468-480, June 21-23, 1994
• 5: J. Ebergen and R. Berks, "VERDECT: A verifier for Asynchronous Circuits," IEEE TCCA Newsletter, 1995.
• 6: Kenneth L. McMillan, Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings, Proceedings of the 7th International Conference on Computer Aided Verification, p.180-195, July 03-05, 1995
• 7: Oriol Roig , Jordi Cortadella , Enric Pastor, Verification of Asynchronous Circuits by BDD-based Model Checking of Petri Nets, Proceedings of the 16th International Conference on Application and Theory of Petri Nets, p.374-391, June 26-30, 1995
• 8: Tomohiro Yoneda , Takashi Yoshikawa, Using Partial Orders For Trace Theoretic Verification Of Asynchronous Circuits, Proceedings of the 2nd International Symposium on Advanced Research in Asynchronous Circuits and Systems, p.152, March 18-21, 1996
• 9: Bernd--Holger Schlingloff , Tomohiro Yoneda, Efficient Verification of Parallel Real–Time Systems, Formal Methods in System Design, v.11 n.2, p.187-215, Aug. 1997 [doi>10.1023/A:1008682131325]
• 10: H. Schlingloff, O. Meyer and T. H. ulsing, "Correctness Analysis of an Embedded Controller," Proc. Int. Conf. on Data Systems in Aerospace (Dasia '99), Lissabon, 1999.
• 11: Wendy Belluomini , Chris J. Myers, Verification of Timed Systems Using POSETs, Proceedings of the 10th International Conference on Computer Aided Verification, p.403-415, June 28-July 02, 1998
• 12: Tomohiro Yoneda , Bin Zhou , Bernd-Holger Schlingloff, Verification of Bounded Delay Asynchronous Circuits with Timed Traces, Proceedings of the 7th International Conference on Algebraic Methodology and Software Technology, p.59-73, January 04-08, 1999
• 13: B. Zhou and T. Yoneda, "Verification of asynchronous circuits with bounded delay model,"(in Japanese) IEICE journal, Vol. J82-D-I, No. 7, pp. 819-833, 1999.
• 14: Tomohiro Yoneda , Hiroshi Ryu, Timed Trace Theoretic Verification Using Partial Order Reduction, Proceedings of the 5th International Symposium on Advanced Research in Asynchronous Circuits and Systems, p.108, April 19-21, 1999
• 15: B. Zhou, T. Yoneda and B. Schlingloff, "Conformance and Mirroring for Timed Asynchronous Circuits," TIT technical report, 2000.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.4 INPUT/OUTPUT AND DATA COMMUNICATIONS
      B.4.3 Interconnections (subsystems)
          Subjects: Asynchronous/synchronous operation

Additional Classification:
  B. Hardware
  B.7 INTEGRATED CIRCUITS
  B.8 Performance and Reliability

  J. Computer Applications
  J.2 PHYSICAL SCIENCES AND ENGINEERING
      Subjects: Electronics

General Terms:
Algorithms, Design, Performance, Theory