DocumentCode
1584409
Title
Temporal Refinement in Co-Design
Author
Aljer, Ammar ; Boulanger, Jean-Louis ; Devienne, Philippe
Author_Institution
HeuDiaSyC Lab., Technol. Univ. of Compiegne, Compiegne
fYear
2008
Firstpage
1
Lastpage
6
Abstract
This paper shows how it is possible to employ refinement concept of B formal method in hardware design. The structural, logical and temporal properties of a Hardware Description Language that is enriched with annotations of the Property Specification language are projected into B model. Then the generated B image is analyzed, using B method tools, in order to prove the initial properties. This technique produces a correct by design component.
Keywords
hardware description languages; logic CAD; B formal method; hardware description language; hardware design; property specification language; temporal refinement; Circuits; Design methodology; Embedded system; Formal specifications; Hardware design languages; Image generation; Laboratories; Logic; Paper technology; Specification languages; B method; PSL; Refinement; VHDL;
fLanguage
English
Publisher
ieee
Conference_Titel
Information and Communication Technologies: From Theory to Applications, 2008. ICTTA 2008. 3rd International Conference on
Conference_Location
Damascus
Print_ISBN
978-1-4244-1751-3
Electronic_ISBN
978-1-4244-1752-0
Type
conf
DOI
10.1109/ICTTA.2008.4530351
Filename
4530351
Link To Document