Approach for a Formal Verification of a Bit-serial Pipelined Architecture

  • Henning Zabel
  • Achim Rettberg
  • Alexander Krupp
Part of the IFIP – The International Federation for Information Processing book series (IFIPAICT, volume 231)


Model Check Linear Temporal Logic Computation Tree Logic Symbolic Model Check VHDL Code 
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]
    M. Bartley, D. Galpin, and T. Blackmore. A comparison of three verification techniques: Directed testing, pseudo-random testing and property checking. In Proceedings of DAC 2002, New Orleans, June 2002. ACM.Google Scholar
  2. [2]
    J. Bergeron, E. Cerny, A. Hunter, and A. Nightingale. Verification Methodology Manual for SystemVerilog. Springer, 2006.Google Scholar
  3. [3]
    E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.Google Scholar
  4. [4]
    Florian Dittmann, Achim Rettberg, Thomas Lehmann, and Mauro C. Zanella. Invariants for distributed local control elements of a new synchronous bit-serial architecture. In Second IEEE International Workshop on Electronic Desing, Test and Applications (DELTA 2004), pages 245-250, Perth, Western Australia, 28 - 30 January 2004.CrossRefGoogle Scholar
  5. [5]
    IEEE. IEEE Std.1800-2005 - Standard for SystemVerilog Unified Hardware Design, Specification and Verification Language, November 2005.Google Scholar
  6. [6]
    IEEE. IEEE Std.1850-2005 - IEEE Standard for Property Specification Language (PSL), September 2005.Google Scholar
  7. [7]
    Achim Rettberg, Florian Dittmann, Mauro C. Zanella, and Thomas Lehmann. Towards a high-level synthesis of reconfigurable bit-serial architectures. In Proceedings of the 16th Symposium on Integrated Circuits and System Design (SBCCI), Sao Paulo, Brazil, 8- 11 September 2003.Google Scholar
  8. [8]
    Achim Rettberg, Thomas Lehmann, Mauro C. Zanella, and Christophe Bobda. Selbststeuernde rekonfigurierbare bit-serielle pipelinearchitektur. Deutsches Patent- und Markenamt, December 2004. Patent-No. 10308510.Google Scholar
  9. [9]
    Achim Rettberg, Mauro C. Zanella, Christophe Bobda, and Thomas Lehmann. A fully self-timed bit-serial pipeline architecture for embedded systems. In Proceedings of the Design Automation and Test Conference (DATE), Messe Munich, Munich, Germany, 3-7 March 2003.Google Scholar
  10. [10]
    J. Ruf. “RAVEN: Real-Time Analyzing and Verification Environment”. Journal on Universal Computer Science (J.UCS), Springer, Heidelberg, February 2001.Google Scholar
  11. [11]
    J. Ruf and T. Kropf. “Modeling and Checking Networks of Communicating Real-Time Processes”. In Int. Conf. on Correct Hardware Design and Verification Methods, Bad Herrenalb, Germany, 1999. Springer-Verlag.Google Scholar
  12. [12]
    Jurgen Ruf and Thomas Kropf. “Symbolic Model Checking for a Discrete Clocked Temporal Logic with Intervals”. In Conference on Correct Hardware Design and Verification Methods (CHARME), Montreal, Canada, October 1997.Google Scholar

Copyright information

© International Federation for Information Processin 2007

Authors and Affiliations

  • Henning Zabel
    • 1
  • Achim Rettberg
    • 2
  • Alexander Krupp
    • 3
  1. 1.University of Paderborn/C-LABGermany
  2. 2.University of Paderborn/C-LABGermany
  3. 3.University of Paderborn/C-LABGermany

Personalised recommendations