A Symbolic Transition System for a Subset of VHDL'87 Descriptions and its Application to Symbolic Model Checking

E. Encrenaz

IBP-Masi 1995/09: Rapport de Recherche Masi / Masi research reports
17 pages - Avril/April 1995 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: A Symbolic Transition System for a Subset of VHDL'87 Descriptions and its Application to Symbolic Model Checking

Résumé : Nous présentons une approche pour extraire un système de transitions symbolique d'une description écrite en un sous-ensemble de VHDL'87 (les instrustions faisant référence au temps sont exclues, et les objets manipulés sont de type booléen, bit ou bit-vector). Ce système de transitions symbolique peut être utilisé pour la vérification formelle de propriétés de descriptions VHDL (Vérification Symbolique de Modèle, appelée couramment Symbolic Model Checking, ou Équivalence d'Automates). Il consiste en un système d'équations booléennes indicant l'état futur du système en fonction de son état courant. Il est automatiquement construit à partir d'une représentation formelle de la description VHDL en réseaux de Petri. Le déterminisme intrinsèque de VHDL'87 et l'exclusion des descriptions VHDL, permet d'abstraire le comportement du système, réduisant la taille du système de transitions et par là même, le coût de la vérification formelle qui s'ensuit. La construction du système d'équations à partir du réseau de Petri intermédiaire est d'abord présentée, puis un exemple de vérification de propriété logico-temporelle illustre l'utilisation d'un tel système pour la Vérification Symbolique de Modèle. Les résultats expérimentaux présentés démontrent la faisabilité de l'approche.

Abstract : This paper presents the main principles for building a symbolic transition system from a description written in a subset of VHDL'87 (temporal information is excluded and objects are restricted to bit, bit_vector and Boolean types). This transition system is used for formal verification of the VHDL description. It consist of a system of Boolean equations indicating the next state of the system in terms of its current state. It is automatically generated from an intermediate representation of the VHDL description by means of a Petri Net. The deterministic nature of VHDL 87 and the exclusion of temporal elements in the description permit us to abstract the behavior of the system : only one state per delta cycle is represented instead of all intermediate states encountered in simulation. This abstraction reduces the size of the transition system which reduces the cost of subsequent analysis. The construction of the system of Boolean equations from the Petri Net is presented first, and then an example of verification of a temporal logic property illustrates its use for Symbolic Model Checking. Experimental results are given which demonstrate the feasibility of this approach.

Publications internes Masi 1995 / Masi research reports 1995