Hazard Checking of Timed Asynchronous Circuits Revisited

• Autorzy: Béal F. , Yoneda T. , Myers C.J.
• Języki publikacji: EN

Abstrakty

EN

This paper proposes a new approach for the hazard checking of timed asynchronous circuits. Previous papers proposed either exact algorithms, which suffer from state-space explosion, or efficient algorithms which use (conservative) approximations to avoid state-space explosion, but have the drawback of a rather conservative definition of failure states, which results in the rejection of designs which are valid. Algorithms based on [1], extending it to the timed case [7], while being very efficient, are unable to handle circuits with internal loops, which prevents their use in some cases. We propose a new approach to the problem in order to overcome the mentioned limitations, without sacrificing efficiency. To do so, we first introduce a general framework targeted at the conservative checking of safety failures. This framework is not restricted to the checking of timed asynchronous circuits. Then, we propose a new (conservative) semantics to timed circuits, in order to use the proposed framework for hazard checking of such circuits. Using this framework with the proposed semantics yields an efficient algorithm that solves the limitations of the previous approaches.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 88, nr 4
• Strony: 411--435
• Opis fizyczny: bibliogr. 15 poz., tab., wykr.

Twórcy

autor

Béal F.

autor

Yoneda T.

autor

Myers C.J.

• Tokyo Institute of Technology, Tokyo, Japan,

Bibliografia

• [1] Beerel, P. A., Meng, T. H.-Y., Burch, J.: Efficient Verification of Determinate Speed-Independent Circuits, Proc. International Conf. Computer-Aided Design (ICCAD), IEEE Computer Society Press, November 1993.
• [2] Clarisó, R., Cortadella, J.: Verification of Concurrent Systems with Parametric Delays Using Octahedra, Proc. 5th International Conference on Application of Concurrency to System Design (ACSD'05), IEEE Computer Society Press, June 2005.
• [3] Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints., POPL, 1977.
• [4] Dill, D. L.: Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits, MIT press, 1988.
• [5] Jeong, C., Nowick, S. M.: Fast hazard detection in combinational circuits, DAC (S. Malik, L. Fix, A. B. Kahng, Eds.), ACM, 2004, ISBN 1-58113-828-8.
• [6] Myers, C. J., Belluomini, W., Killpack, K., Mercer, E., Peskin, E., Zheng, H.: Timed Circuits: A New Paradigm for High-Speed Design, Proc. of Asia and South Pacific Design Automation Conference, February 2001.
• [7] Nelson, C., Myers, C., Yoneda, T.: Efficient verification of hazard-freedomin gate-level timed asynchronous circuits, IEEE Transactions on CAD, 2007, 26(3).
• [8] Peña, M. A., Cortadella, J., Kondratyev, A., Pastor, E.: Formal verification of safety properties in timed circuits, Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, IEEE Computer Society Press, April 2000.
• [9] Roig, O., Cortadella, J., Pastor, E.: Verification of asynchronous circuits by BDD-based model checking of Petri nets, 16th International Conference on the Application and Theory of Petri Nets, 815, June 1995.
• [10] Rokicki, T., Myers, C.: Automatic verification of timed circuits, LNCS 818 Computer Aided Verification, 1994, 468-480.
• [11] Stevens, K. S., Rotem, S., Ginosar, R., Beerel, P., Myers, C. J., Yun, K. Y., Koi, R., Dike, C., Roncken, M.: An asynchronous instruction length decoder, IEEE Journal of Solid-State Circuits, 36(2), February 2001, 217-228.
• [12] Sutherland, I., Fairbanks, S.: GasP: A Minimal FIFO Control, Proc. of ASYNC'01, 2001, 46-53.
• [13] Thompson, S., Mycroft, A.: Abstract Interpretation of Combinational Asynchronous Circuits., SAS (R. Giacobazzi, Ed.), 3148, Springer, 2004, ISBN 3-540-22791-1.
• [14] Yoneda, T., Ryu, H.: Timed Trace Theoretic Verification Using Partial Order Reduction, Proc. International Symposium on Advanced Research in Asynchronous Circuits and Systems, April 1999.
• [15] Zheng, H., Mercer, E., Myers, C. J.: Modular Verification of Timed Circuits Using Automatic Abstraction, IEEE Transactions on Computer-Aided Design, 22(9), September 2003.