Towards verifying VHDL descriptions of processors

We present a system for the formal verication of processors which combines a computer algebra simplication 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.

• Type: Conference
• Year: 1995
• Where: EURODAC
• Authors: Laurent Arditi, Hélène Collavizza
• Keywords: Algebra Simpli Cation, EURODAC 1995, Formal Veri Cation, VHDL, VHDL Cookbook