LGI/IMAG (Grenoble, France)
CADP (Construction and Analysis of Distributed Processes)
380 lines of LOTOS
up to 101,000 states and 150,000 transitions
This case study deals with systolic networks computing convolution product.
Such networks consist of arrays of identical (or almost identical) cells
assembled together to perform a flow of computation. Each cell takes one or
two inputs, and delivers one or two outputs, which are a linear combination
Four different systolic network architectures were considered: B1 (broadcast), F (fan-in), W1 and W2 (pure systolic - weights stay). Each network is parameterized by its number N of cells and the length M of value sequences that are given as input to the network. These input values are not concrete values (i.e., numbers) but symbolic ones (i.e., variables), so that the outputs produced by the circuits are also symbolic (i.e., algebraic terms expressing linear combinations of input values).
The verification was carried out by generating (using CAESAR) the labelled transition system corresponding to each network for given values of N and M, by minimizing (using ALDEBARAN) this labelled transition system modulo observational equivalence, and by visually checking that convolution product is properly computed as expected.
This case study was truly the second one performed by jointly using the CAESAR
and ALDEBARAN tools, the combination of which gave birth to the CADP toolbox.
It was also the first time that LOTOS was used to formally model and verify
hardware circuits, keeping in mind that LOTOS had been originally designed
for specifying telecommunication protocols.
This case study demonstrated that systolic circuits, so far described using synchronous languages, could also be specified using an asynchronous process calculus such as LOTOS, and that their behaviour could be automatically verified using model checking. Finally, this case study proposed an early form of symbolic model checking in which inputs and outputs are symbolic (rather than concrete) data.
"Utilisation de CAESAR et ALDEBARAN".
Technical report, 24 pages, in French.
Based on Appendix D of Hubert Garavel's PhD thesis "Compilation et vérification de programmes LOTOS", Thèse de Doctorat, Université Joseph Fourier (Grenoble), November 1989. http://cadp.inria.fr/publications/Garavel-89-b.html
Available on-line from: http://cadp.inria.fr/publications/Garavel-89-b-CD.html
or from the CADP Web site in PDF or PostScript
LGI - IMAG Campus
38041 GRENOBLE cedex
The LOTOS descriptions as well as explanations on the verification with
CADP are available on-line at: |
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies