Expressing and Verifying Properties of VHDL Programs

Rajesh K. Bawa, E. Encrenaz

IBP-Masi 1995/02: Rapport de Recherche Masi / Masi research reports
13 pages - Janvier/January 1995 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: Expressing and Verifying Properties of VHDL Programs

Résumé : Nous proposons une méthode de vérification de systèmes décrits en VHDL. Cette approche repose sur la vérification symbolique de propriétés logico-temporelles. Un système de transitions symbolique représenté sous forme de BDD est extrait d'une description VHDL. Les propriétés à vérifier sont exprimées dans un environnement associant la syntaxe de VHDL et de CTL.

Abstract : In this paper we propose a method for design verification based on Symbolic Model Checking. A symbolic transition system, based on BDD representation, is derived from a VHDL description and properties expressed in a mixed environment of VHDL and CTL are used for formal verification of VHDL systems.

Publications internes Masi 1995 / Masi research reports 1995