|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: https://doi.org/10.1007/978-3-031-28332-1_43 |
| Contact: | Katsumi Wasaki Faculty of Engineering Shinshu University Nagano JAPAN Email: [email protected] |
| Further remarks: | 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