Formal methods of algorithm analysis for decreasing RTL-verification complexity

Author

Lyalin, Alexander

Author_Institution

Dept. of Comput. Sci., Moscow Inst. of Phisics & Technol., Moscow

fYear

2007

fDate

19-24 Feb. 2007

Firstpage

101

Lastpage

103

Abstract

The basis for RTL-development and verification system is functional device specification. More often bugs are "produced" when informal transitions from this specification to RTL and "verification environment"- code are taken by design and validation engineers. In contrast to this traditional approach the formal transition method to RTL-code and verification environment development is introduced, based on device C- model Control-DataFlow Graph (CDFG) analysis. As an example, in this article the introduced formal approach is applied for JPEG2000 model for getting RTL SystemC-code.

Keywords

circuit CAD; data flow graphs; formal verification; JPEG2000 model; RTL-verification complexity; algorithm analysis; control-dataflow graph analysis; formal transition method; verification environment development; Algorithm design and analysis; Computer bugs; Design engineering; Design methodology; Discrete transforms; Flow graphs; Hardware; Sparks; Standards development; Time to market; CDFG; JPEG2000; SPARK; SystemC; algorithm analysis; formal transition; functional verification;

fLanguage

English

Publisher

ieee

Conference_Titel

CAD Systems in Microelectronics, 2007. CADSM '07. 9th International Conference - The Experience of Designing and Applications of

Conference_Location

Lviv-Polyana

Print_ISBN

966-533-587-0

Type

conf

DOI

10.1109/CADSM.2007.4297489

Filename

4297489