Title :
Towards verifying VHDL descriptions of processors
Author :
Arditi, Laurent ; Collavizza, Hélène
Author_Institution :
CNRS, Nice Univ., Sophia Antipolis, France
Abstract :
We present a system for the formal verification of processors which combines a computer algebra simplification tool with an object-oriented approach. It has been successfully used for verifying the DP32 processor described in the VHDL Cookbook. A general VHDL description style for proving processors is derived from this case study
Keywords :
formal verification; hardware description languages; microprocessor chips; object-oriented programming; DP32 processor; VHDL processor descriptions; computer algebra simplification tool; formal verification; object-oriented approach; Algebra; Assembly; Circuits; Concrete; Design automation; Displays; Formal verification; Object oriented modeling; Prototypes;
Conference_Titel :
Design Automation Conference, 1995, with EURO-VHDL, Proceedings EURO-DAC '95., European
Conference_Location :
Brighton
Print_ISBN :
0-8186-7156-4
DOI :
10.1109/EURDAC.1995.527438
