• DocumentCode
    3195005
  • Title

    A Unified Formal Framework for Analyzing Functional and Speed-path Properties

  • Author

    Olivo, Oswaldo ; Ray, Sandip ; Bhadra, Jayanta ; Vedula, Vivekananda

  • Author_Institution
    Univ. of Texas at Austin, Austin, TX, USA
  • fYear
    2011
  • fDate
    5-7 Dec. 2011
  • Firstpage
    44
  • Lastpage
    45
  • Abstract
    We develop a formal tool for speed-path analysis and debug. We encode speed-path requirements in a formal hardware description language providing the semantics of both the functional behavior and timing constraints, and the disciplined use of an SMT solver to analyze speed-path requirements. We are applying our framework for speed-path analysis of several RTL designs from Opencores.
  • Keywords
    electronic engineering computing; formal languages; hardware description languages; logic design; programming language semantics; Opencores; RTL designs; SMT solver; formal hardware description language; functional property analysis; speed-path analysis; timing constraints; unified formal framework; Analytical models; Clocks; Hardware; Hardware design languages; Integrated circuit modeling; Logic gates; Timing; SMT; functional verification; hardware description language; static timing analysis;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Microprocessor Test and Verification (MTV), 2011 12th International Workshop on
  • Conference_Location
    Austin, TX
  • ISSN
    1550-4093
  • Print_ISBN
    978-1-4577-2101-4
  • Type

    conf

  • DOI
    10.1109/MTV.2011.17
  • Filename
    6142325