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
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;
Conference_Titel :
Microprocessor Test and Verification (MTV), 2011 12th International Workshop on
Conference_Location :
Austin, TX
Print_ISBN :
978-1-4577-2101-4
DOI :
10.1109/MTV.2011.17
