DocumentCode :
3265325
Title :
Using integer equations to check PSL properties in RT level design
Author :
Alizadeh, Bijan ; Navabi, Zainalabedin
Author_Institution :
Dept. of Electr. & Comput. Eng., Tehran Univ., Iran
fYear :
2004
fDate :
19-21 July 2004
Firstpage :
83
Lastpage :
86
Abstract :
This article describes a high level model of digital circuits for application of formal verification properties at this level. In our method, a behavioral state machine is represented by a multiplexer based structure of linear integer equations, and a subset of PSL property language is directly applied. It reduces the need for large BDD data structures and uses far less memory. Furthermore, there is no need to separate the data and control sections in circuits. We used a canonical form of linear TED (Ciesielski et al., 2002). This paper compares our results with those of the VIS verification tool which is a BDD based program.
Keywords :
data flow graphs; data structures; digital circuits; formal verification; multiplexing equipment; BDD data structure; PSL property language; RT level design; behavioral state machine; digital circuits; formal verification; high level model; linear integer equations; multiplexer-based structure; Application software; Arithmetic; Automatic control; Binary decision diagrams; Data structures; Digital circuits; Equations; Formal verification; Hardware; Multiplexing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
System-on-Chip for Real-Time Applications, 2004.Proceedings. 4th IEEE International Workshop on
Print_ISBN :
0-7695-2182-7
Type :
conf
DOI :
10.1109/IWSOC.2004.1319855
Filename :
1319855
Link To Document :
بازگشت