Title :
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
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;
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
DOI :
10.1109/CADSM.2007.4297489
