Efficient Verification of Hazard-Freedom in Gate-Level Timed Asynchronous Circuits

ABSTRACT

This paper presents an efficient method for verifying hazard freedomin timed asynchronous circuits. Timed circuits are a classof asynchronous circuits that utilize explicit timing informationfor optimization throughout the entire design process. In asynchronouscircuits, correct operation requires that there are no hazardsin the circuit implementation. Therefore, when designing anasynchronous circuit, each internal node and output of the circuitmust be verified for hazard-freedom to ensure correct operation.Current verification algorithms for timed asynchronous circuits requirean explicit state exploration often resulting in state explosionfor even modest sized examples. The goal of this work isto abstract the behavior of internal nodes and utilize this informationto make a conservative determination of hazard-freedom foreach node in the circuit. Experimental results indicate that thisapproach is substantially more efficient than existing timing verificationtools. These results also indicate that this method scaleswell for large examples. It is capable of analyzing circuits in lessthan a second that could not be previously analyzed. While thismethod is conservative in that some false hazards may be reported,our results indicate that the number of false hazards is small.

REFERENCES

• 1: Peter A. Beerel , Jerry R. Burch , Teresa H. Meng, Checking combinational equivalence of speed-independent circuits, Formal Methods in System Design, v.13 n.1, p.35-85, May 1, 1998
• 2: Peter A. Beerel , Jerry Burch , Teresa H.-Y. Meng, Efficient verification of determinate speed-independent circuits, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.261-267, November 07-11, 1993, Santa Clara, California, United States
• 3: [3] W. Belluomini and C. J. Myers. Timed state space exploration using posets. IEEE Transactions on Computer-Aided Design, 19(5):501-520, May 2000.
• 4: David L. Dill, Timing Assumptions and Verification of Finite-State Concurrent Systems, Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, p.197-212, June 12-14, 1989
• 5: David L. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits, MIT Press, Cambridge, MA, 1989
• 6: [6] J. Ebergen and S. Gingras. A verifier for network decompositions of command-based specifications. In Proc. Hawaii International Conf. System Sciences, volume I. IEEE Computer Society Press, Jan. 1993.
• 7: [7] G. Gopalakrishnan, E. Brunvand, N. Michell, and S. Nowick. A correctness criterion for asynchronous circuit validation and optimization. IEEE Transactions on Computer-Aided Design, 13(11):1309-1318, Nov. 1994.
• 8: M. Kishinevsky , A. Kondratyev , A. Taubin , V. Varshavsky, Analysis and identification of speed-independent circuits on an event model, Formal Methods in System Design, v.4 n.1, p.33-75, Jan. 1994 [doi>10.1007/BF01383956]
• 9: [9] O. M. M. Bozga, H. Jianmin and S. Yovine. Verification of asynchronous circuits using timed automata. In O. M. Eugene Asarin and S. Yovine, editors, Electronic Notes in Theoretical Computer Science, volume 65. Elsevier Science Publishers, 2002.
• 10: [10] E. Mercer, C. Myers, and T. Yoneda. Improved poset timing analysis in timed petri nets. In The Tenth Workshop on Synthesis and System Integration of Mixed Technologies (SASIMI 2001), October 2001.
• 11: [11] P. Merlin and D. J. Faber. Recoverability of communication protocols. IEEE Trans. on Communication, COM- 24(9):1036-1043, 1976.
• 12: Chris J. Myers , Wendy Belluomini , Kip Kallpack , Eric Peskin , Hao Zheng, Timed circuits: a new paradigm for high-speed design, Proceedings of the 2001 conference on Asia South Pacific design automation, p.335-340, January 2001, Yokohama, Japan [doi>10.1145/370155.370379]
• 13: [13] C. J. Myers, T. G. Rokicki, and T. H.-Y. Meng. POSET timing and its application to the synthesis and verification of gate-level timed circuits. IEEE Transactions on Computer-Aided Design, 18(6):769-786, June 1999.
• 14: Marco A. Pena , Jordi Cortadella , Enric Pastor , Alex Kondratyev, Formal Verification of Safety Properties in Timed Circuits, Proceedings of the 6th International Symposium on Advanced Research in Asynchronous Circuits and Systems, p.2, April 02-06, 2000
• 15: O. Roig , J. Cortadella , E. Pastor, Hierarchical gate-level verification of speed-independent circuits, Proceedings of the 2nd Working Conference on Asynchronous Design Methodologies, p.128, May 30-31, 1995
• 16: 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
• 17: [17] K. S. Stevens, S. Rotem, R. Ginosar, P. Beerel, C. J. Myers, K. Y. Yun, R. Koi, C. Dike, and M. Roncken. An asynchronous instruction length decoder. IEEE Journal of Solid-State Circuits, 36(2):217-228, Feb. 2001.
• 18: 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
• 19: [19] H. Zheng, E. Mercer, and C. Myers. Modular verification of timed circuits using automatic abstraction. IEEE Transactions on Computer-Aided Design, 22(9), Sept. 2003.
• 20: Hao Zheng , Chris J. Myers , David Walter , Scott Little , Tomohiro Yoneda, Verification of Timed Circuits with Failure Directed Abstractions, Proceedings of the 21st International Conference on Computer Design, p.28, October 13-15, 2003

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.4 INPUT/OUTPUT AND DATA COMMUNICATIONS
      B.4.3 Interconnections (subsystems)
          Subjects: Topology (e.g., bus, point-to-point)
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Verification

General Terms:
Algorithms, Design, Verification