A methodology for system-level design for verifiability

  • Paolo Camurati
  • Fulvio Corno
  • Paolo Prinetto
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)


Working at system level is attracting increasing interest. New issues must be taken into account, such as validation and verification at all steps. This paper presents a system-level design methodology that supports verification. Starting from a description in a proper subset of VHDL, a Petri Net description is obtained and used for validation purposes and for building the corresponding automaton. An efficient BDD-based tool for Process Algebra manipulation supports formal equivalence proofs. Experimental results show that the approach is feasible also for real-size industrial cases.


Label Transition System Hardware Description Language Symbolic Model Check Elementary Building Block VHDL Description 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Burch, J.R., Clarke, E.M., Long, D.E.: Representing Circuits More Efficiently in Symbolic Model Checking. DAC'91: 28th ACM/IEEE Design Automation Conference, San Francisco, CA (USA), June 1991, pp. 403–407Google Scholar
  2. 2.
    Browne, M., Clarke, E.M., Dill, D., Mishra, B.: Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, Vol.C-35, No.12, December 1986, pp. 1035–1044.Google Scholar
  3. 3.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 States and Beyond. LICS'90: 5th Annual IEEE Symposium on Logic in Computer Science, June 1990, pp. 428–439Google Scholar
  4. 4.
    Camurati, P., Prinetto, P.: Design For Verifiability and Design For Testability: limiting designers' freedom to achieve what? Workshop On Correct Hardware Design Methodologies, Turin (Italy), June 1991, P. Prinetto, P. Camurati editors, North Holland, Amsterdam (The Netherlands), pp. 295–309Google Scholar
  5. 5.
    Camurati, P., Corno, F., Prinetto, P.: Exploiting symbolic traversal techniques for efficient Process Algebra manipulation. CHDL'93: IFIP Conference on Hardware Description Languages and their Applications, Ottawa (Canada), April 1993Google Scholar
  6. 6.
    Camurati, P., Corno, F., Prinetto, P.: System-level fault modeling and test pattern generation with Process Algebras. ETC'93: IEEE European Test Conference, Rotterdam (The Netherlands), April 1993Google Scholar
  7. 7.
    De Nicola, R., Hennessy, M.: Testing Equivalence for Processes. Theoretical Computer Science, 34, 1984, pp. 83–133Google Scholar
  8. 8.
    Verilog: EVAL Predicate Transition Analyzer, Reference manual. Verilog SA, Toulouse (France), 1991Google Scholar
  9. 9.
    Genrich, H.J.: Predicate/Transition Nets. W. Brauer, W. Reisig, G. Rozemberg editors “Petri Nets: central models and their properties,” Advances in Petri Nets, part I, Lecture Notes in Computer Science 254, Springer, Berlin (Germany), 1987, pp. 207–247Google Scholar
  10. 10.
    Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Stuhl-Trauring, A.: STATEMATE: a working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering, vol. 16, n. 4, 1990, pp. 403–414Google Scholar
  11. 11.
    IEEE: IEEE standard VHDL language reference manual. IEEE, March 1988Google Scholar
  12. 12.
    Kohavi, Z.: Switching and Finite Automata Theory. second edition, Computer Science Series, Mc Graw Hill, New York, NYGoogle Scholar
  13. 13.
    Koomen, C.J.: The design of communicating systems: a system engineering approach. Kluwer Academic Publishers, Boston, MA (USA), 1991Google Scholar
  14. 14.
    Milne, G.J.: Circal and the representation of communication, concurrency, and time. ACM Trans. on Programming Languages and Systems, Vol. 7, No. 2, 1985Google Scholar
  15. 15.
    Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs, NJ (USA), 1989Google Scholar
  16. 16.
    Milne, G.J.: Design for verifiability. Workshop on “Hardware Specification, Verification and Synthesis: Mathematical Aspects”, Cornell University, Ithaca, NY (USA), July 1989Google Scholar
  17. 17.
    Narayan, S., Vahid, F., Gajski, D.D.: Translating system specifications to VHDL. EDAC'91: IEEE European Design Automation Conference, Amsterdam (The Netherlands), February 1991, pp. 390–394Google Scholar
  18. 18.
    Williams, T.W., Parker, K.P.: Design for Testability — a survey. IEEE Transactions on Computers, Vol. C-31, n. 1, January 1982, pp. 2–15Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Paolo Camurati
    • 1
  • Fulvio Corno
    • 1
  • Paolo Prinetto
    • 1
  1. 1.Dipartimento di Automatica e InformaticaPolitecnico di TorinoTurinItaly

Personalised recommendations