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 (fanin), 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: 
[Garavel89bCD]
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/Garavel89b.html Available online from: http://cadp.inria.fr/publications/Garavel89bCD.html or from the CADP Web 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 online at: http://cadp.inria.fr/ftp/demos/demo_04 This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/casestudies 