DocumentCode
454504
Title
Proven correct monitors from PSL specifications
Author
Morin-Allory, Katell ; Borrione, Dominique
Author_Institution
Tima Lab., Grenoble
Volume
1
fYear
2006
fDate
6-10 March 2006
Firstpage
1
Lastpage
6
Abstract
We developed an original method to synthesize monitors from declarative specifications written in the PSL standard. Monitors observe sequences of values on their input signals, and check their conformance to a specified temporal expression. Our method implements both the weak and strong versions of PSL FL operators, and has been proven correct using the PVS theorem proven This paper discusses the salient aspects of the proof of our prototype implementation for on-line design verification
Keywords
hardware description languages; integrated circuit design; logic design; system-on-chip; theorem proving; PSL FL operators; PSL specifications; PSL standard; PVS theorem proven; declarative specification monitor; design verification; Automata; Circuit testing; Design engineering; Integrated circuit interconnections; LAN interconnection; Laboratories; Prototypes; Signal synthesis; Standards development; Very large scale integration;
fLanguage
English
Publisher
ieee
Conference_Titel
Design, Automation and Test in Europe, 2006. DATE '06. Proceedings
Conference_Location
Munich
Print_ISBN
3-9810801-1-4
Type
conf
DOI
10.1109/DATE.2006.244079
Filename
1657086
Link To Document