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 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 on-line 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/case-studies

Back to the CADP case studies page