Database of Case Studies Achieved Using CADP

Systolic Networks for Convolution Product

Organisation: LGI/IMAG (Grenoble, France)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Hardware Design

Period: 1989

Size: 380 lines of LOTOS
up to 101,000 states and 150,000 transitions

Description: 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 of inputs.

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.

Conclusions: 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.

Publications: [Garavel-89-b-CD] Hubert Garavel. "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 our FTP site in PDF or PostScript

Contact:
Hubert Garavel
LGI - IMAG Campus
BP 53X
38041 GRENOBLE cedex
FRANCE



Further remarks: The LOTOS descriptions as well as explanations on the verification with CADP are available on-line at:
ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_04

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page