Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic

  • Katell Morin-Allory
  • David Cachera
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


The polyhedral model mixes recurrence equations over polyhedral domains and affine dependency functions. This model provides a unified framework for reasoning about regular systems composed of both hardware and software parts. Systems are described in a generic manner through the use of symbolic parameters, and structuring mechanisms allow for hierarchical specifications. The ALPHA language [3] and the MMALPHA environment [4] provide a syntax and a programming environment to define and manipulate polyhedral equation systems. High-level system specifications are refined through a user-guided series of automatic transformations, down to an implementable description, from which may be derived C code or a VHDL architecture. For hardware components and interfaces, control signals are generated to validate computations or data transfers. The use of systematic and semi-automatic rewritings together with the clean semantic basis provided by the polyhedral model should ensure the correctness of the final implementation. However, interface and control signal generators are not certified, and hand-made optimisations are still performed to tune the final result. As a consequence, the correctness of control signals has to be checked at the lower level of description, in the presence of symbolic parameters. A formal verification tool that benefits from the intrinsic regularity of the model has been developed to (partially) certify low-level system descriptions [2], based on polyhedra manipulation. The present work develops new strategies to prove a wider class of formulae. The basic idea is to detect particular patterns in the definition of signals, that characterise the propagation of known values along spatial or temporal dependencies, and to define a widening operator that allows for the automatic determination of how this propagation can be useful in the proof process.


Recurrence Equation Regular System Proof Tree Proof Rule Polyhedral Domain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Cachera, D., Morin-Allory, K.: Proving parameterized systems: the use of a widening operator and pseudo-pipelines in polyhedral logic. Technical report, TIMA (April 2005)Google Scholar
  2. 2.
    Cachera, D., Morin-Allory, K.: Verification of safety properties for parameterized regular systems. Trans. on Embedded Computing Sys. 4(2), 228–266 (2005)CrossRefGoogle Scholar
  3. 3.
    Mauras, C.: Alpha: un langage équationnel pour la conception et la programmation d’architectures systoliques. PhD thesis, Univ. Rennes I, France (December 1989)Google Scholar
  4. 4.
    Wilde, D.K.: A library for doing polyhedral operations. Technical Report 785, IRISA, Rennes, France (January 1993)Google Scholar
  5. 5.
    Wilde, D.K.: The Alpha language. Technical Report 999, IRISA, Rennes, France (January 1994)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Katell Morin-Allory
    • 1
  • David Cachera
    • 2
  1. 1.TIMAGrenobleFrance
  2. 2.IRISA – ENS Cachan (Bretagne)RennesFrance

Personalised recommendations