A Petri Net Model for Verifying Properties of VHDL Programs

E. Encrenaz, R.K. Bawa

IBP-Masi 1995/07: Rapport de Recherche Masi / Masi research reports
21 pages - Février/February 1995 - Document en anglais.

PostScript : Ko /Kb

Titre / Title: A Petri Net Model for Verifying Properties of VHDL Programs

Résumé : Cet article présente un modèle formel de description VHDL basé sur les réseaux de Petri. Des propriétés logiques et logico-temporelles peuvent être automatiquement vérifiées sur des modèles symboliques dérivés de ce réseau de Petri (l'ensemble symbolique des états accessibles et le système de transitions symbolique). Les principes de traduction d'un programme VHDL dans le formalisme des réseaux de Petri sont donnés. Le comportement du réseau de Petri est décrit, et l'analyse du graphe d'accessibilité du réseau de Petri permet d'établir l'équivalence de comportement du réseau de Petri avec des simulations VHDL. Une représentation symbolique des ensembles d'états du réseau de Petri permet de construire des modèles symboliques sur lesquels se basent les analyses automatiques de propriétés. La prise en compte de particularités du comportement de VHDL'87 (déterminisme, notions de stabilisation) permet de réduire significativement le réseau de Petri etde simplifier l'analyse qui en découle.

Abstract : This paper proposes a Petri Net model as a formal model of a VHDL description. logical properties (resp. temporal logic properties) can be checked on symbolic reachability set of states (resp. symbolic transition system) derived from this Petri Net. The translation principles of a VHDL program into Petri Net are given. The behavior of the net is explained and its equivalence with VHDL descriptions is established by analyzing the structure of its reachability graph. Symbolic representation of states of the Petri Net allows the construction of symbolic transition system or symbolic set of reachable states. The reachability graph can be reduced when particularities of VHDL behaviors are taken into account : the deterministic nature of VHDL'87 allows us to reduce the Petri Net and to constraint the general firing rules, and stabilization points can be identified, simplifying the further analysis.

Publications internes Masi 1995 / Masi research reports 1995