Circuit Generation for Verification of ESTEREL Programs

Alain Girault (1) , Gérard Berry

1 BIP - Biped Robot

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.

Mots clés: CODE GENERATION; ESTEREL; FORMAL VERIFICATION; MODEL CHECKING; PARALLEL LANGUAGES; REACTIVE SYSTEMS; SEQUENTIAL CIRCUITS; SYNCHRONOUS PROGRAMMING

Domaines: Autre [cs.OH]

Alain Girault, Gérard Berry. Circuit Generation for Verification of ESTEREL Programs. RR-3582, INRIA. 1998. ⟨inria-00073099⟩