Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic
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  and the MMALPHA environment  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 , 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.
KeywordsRecurrence Equation Regular System Proof Tree Proof Rule Polyhedral Domain
- 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
- 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.Wilde, D.K.: A library for doing polyhedral operations. Technical Report 785, IRISA, Rennes, France (January 1993)Google Scholar
- 5.Wilde, D.K.: The Alpha language. Technical Report 999, IRISA, Rennes, France (January 1994)Google Scholar