On the Specification for VLSI Systolic Arrays
Summary :
Formal verification has become an increasing prominent technique towards establishing the correctness of hardware designs. We present a framework to specifying and verifying the design of systolic architectures. Our approach allows users to represent systolic arrays in Z specification language and to justify the design semi-automatically using the verifier. Z is a notation based on typed set theory and enriched by a schema calculus. We describe how a systolic array for matrix-vector multiplication can be specified and justified with respect to its algorithm.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E76-A No.4 pp.496-506
- Publication Date
- 1993/04/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on Discrete Mathematics and Its Applications)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Fuyau LIN, "On the Specification for VLSI Systolic Arrays" in IEICE TRANSACTIONS on Fundamentals,
vol. E76-A, no. 4, pp. 496-506, April 1993, doi: .
Abstract: Formal verification has become an increasing prominent technique towards establishing the correctness of hardware designs. We present a framework to specifying and verifying the design of systolic architectures. Our approach allows users to represent systolic arrays in Z specification language and to justify the design semi-automatically using the verifier. Z is a notation based on typed set theory and enriched by a schema calculus. We describe how a systolic array for matrix-vector multiplication can be specified and justified with respect to its algorithm.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e76-a_4_496/_p
Copy
@ARTICLE{e76-a_4_496,
author={Fuyau LIN, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={On the Specification for VLSI Systolic Arrays},
year={1993},
volume={E76-A},
number={4},
pages={496-506},
abstract={Formal verification has become an increasing prominent technique towards establishing the correctness of hardware designs. We present a framework to specifying and verifying the design of systolic architectures. Our approach allows users to represent systolic arrays in Z specification language and to justify the design semi-automatically using the verifier. Z is a notation based on typed set theory and enriched by a schema calculus. We describe how a systolic array for matrix-vector multiplication can be specified and justified with respect to its algorithm.},
keywords={},
doi={},
ISSN={},
month={April},}
Copy
TY - JOUR
TI - On the Specification for VLSI Systolic Arrays
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 496
EP - 506
AU - Fuyau LIN
PY - 1993
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E76-A
IS - 4
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - April 1993
AB - Formal verification has become an increasing prominent technique towards establishing the correctness of hardware designs. We present a framework to specifying and verifying the design of systolic architectures. Our approach allows users to represent systolic arrays in Z specification language and to justify the design semi-automatically using the verifier. Z is a notation based on typed set theory and enriched by a schema calculus. We describe how a systolic array for matrix-vector multiplication can be specified and justified with respect to its algorithm.
ER -
English
