Circuit generation and verification of Esterel

Abstract

We propose in this paper a method that takes external Boolean variables into account for the verification of Esterel programs. The intermediate code that we use is a circuit that drives an action table. The circuit represents the control of the program, and the action table manipulates its external variables. The method transforms the actions into Boolean gates and registers acting on nets instead of variables. This involves encoding the input variables into the circuit and decoding output variables. This expansion method has been implemented within the scdata processor and can be used in conjunction with the Esterel compiler.

BibTeX entry

@InProceedings{GB99,
  author = 	 {A. Girault and G. Berry},
  title = 	 {Circuit Generation and Verification of Esterel},
  booktitle = 	 {IEEE International Symposium on Signals, Circuits,
                  and Systems, SCS'99},
  year =	 {1999},
  publisher =	 {``Gh. Asachi'' Publishing},
  address =	 {Iasi, Romania},
  month =	 {July},
  pages =	 {85--89},
  note =	 {Research report INRIA 3582}
}