Database of Case Studies Achieved Using CADP

Verification of Circuits for Systolic Array Parallel Computation

Organisation: Shinshu University, Nagano (JAPAN)

Method: LOTOS

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

Domain: Hardware Design.

Period: 2023

Size: 32279 states and 94326 transitions

Description: In hardware design, verification is an important factor in reducing development costs by detecting problems at an early stage. Systolic arrays consist of multiple Processor Elements (PE), each of which performs calculations individually at the appropriate timing. Systolic array architectures are designed to perform operations without writing temporary data generated during the computation process to memory. Systolic arrays can perform a variety of calculations (matrix product and convolution, digital filters, finding the longest common sequence, etc.) depending on the design and PE configuration.

This study focuses on designing a W1 systolic array by formally modeling it in LOTOS and verifying the behavior of the underlying LTS using the CADP toobox. The model is constructed using a synchronous circuit equipped with a global clock. The synchronous configuration reduces the abstraction level of the systolic array and makes the behavior of each element (e.g., adders, multipliers, registers) observable, enabling to check both local message asynchrony and global synchrony.

Conclusions: The formal modeling and verification provided by CADP enabled to determine that the synchronous implementation of the W1 systolic array architecture captures the intended functioning of the circuit, and also to detect the presence of undesirable behaviors caused by the delays in the adder and multiplier PEs of the circuit.

Publications: [Chiba-Wasaki-23] Yuya Chiba and Katsumi Wasaki. "Description and Verification of Systolic Array Parallel Computation Model in Synchronous Circuit Using LOTOS". Proc. of the 20th International Conference on Information Technology-New Generations (ITNG'2023), Advances in Intelligent Systems and Computing vol. 1445, pp. 379-386. Springer Verlag, 2023.
Available on-line at:

Katsumi Wasaki
Faculty of Engineering
Shinshu University

Further remarks: This case-study, amongst others, is described on the CADP Web site:

Last modified: Wed Feb 21 11:43:32 2024.

Back to the CADP case studies page