• DocumentCode
    724746
  • Title

    Correctness checking of HDL-model behavior based on runtime trace matching

  • Author

    Ivannikov, V.P. ; Kamkin, A.S. ; Chupilko, M.M.

  • Author_Institution
    Inst. for Syst. Program., Moscow, Russia
  • fYear
    2013
  • fDate
    10-12 Oct. 2013
  • Firstpage
    25
  • Lastpage
    30
  • Abstract
    Correctness checking of HDL-model behavior is an integral part of runtime verification of hardware. As a rule, it is based on comparing of HDL-model behavior and reference model behavior, developed in high-level programming languages. Being verified, both models are stimulated with the same input sequence; their output traces are caught and matched. Due to the abstractness of the reference model, the matching is not a trivial task as event sequences can be different and some events of one trace may miss in the other one. A methodology of runtime trace matching for hardware models of different abstraction levels is suggested in this paper. The methodology has been successfully applied to a number of industrial projects of unit-level microprocessor verification.
  • Keywords
    formal verification; hardware description languages; high level languages; HDL model behavior; correctness checking; high-level programming languages; industrial projects; reference model behavior; runtime trace matching; runtime verification; unit-level microprocessor verification; Concrete; Data models; Hardware; Microprocessors; Monitoring; Runtime; Time-domain analysis; HDL; partially ordered multisetsr; partially ordered multisetsuntime verification; trace matching; unit-level verification; untime verification;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Tools & Methods of Program Analysis (TMPA), 2013
  • Conference_Location
    Kostroma
  • Print_ISBN
    978-0-9860773-1-9
  • Type

    conf

  • DOI
    10.1109/TMPA.2013.7163717
  • Filename
    7163717