Inductive techniques for formal verification of systolic array designs in dsp applications

Nam Ling; Timothy Shih; Jonathan Huang

doi:10.1109/ICASSP.1992.226555

Inductive techniques for formal verification of systolic array designs in dsp applications

Nam Ling, Timothy Shih, Jonathan Huang

Department of Computer Science and Information Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

In this paper we show how several inductivc techniques can be utilized to provide fast and efficient proofs to the correctness of systolic designs in digital signal processing (DSP) applications. These techniques exploit the repeatability, regularity, and locality nature of systolic arrays and algorithms in DSP to produce fast proofs independent on the array size. We show how inductive techniques can be applied to different array topologies suitable for DSP and also illustrate the structure of the verifier we developed to automate induction using logic programming.

Original language	English
Title of host publication	ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	573-576
Number of pages	4
ISBN (Electronic)	0780305329
DOIs	https://doi.org/10.1109/ICASSP.1992.226555
State	Published - 1992
Event	1992 IEEE International Conference on Acoustics, Speech, and Signal Processing, ICASSP 1992 - San Francisco, United States Duration: 23 Mar 1992 → 26 Mar 1992

Publication series

Name	ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings
Volume	5
ISSN (Print)	1520-6149

Conference

Conference	1992 IEEE International Conference on Acoustics, Speech, and Signal Processing, ICASSP 1992
Country/Territory	United States
City	San Francisco
Period	23/03/92 → 26/03/92

Access to Document

10.1109/ICASSP.1992.226555

Cite this

Ling, N., Shih, T., & Huang, J. (1992). Inductive techniques for formal verification of systolic array designs in dsp applications. In ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing (pp. 573-576). Article 226555 (ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings; Vol. 5). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/ICASSP.1992.226555

Ling, Nam ; Shih, Timothy ; Huang, Jonathan. / Inductive techniques for formal verification of systolic array designs in dsp applications. ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing. Institute of Electrical and Electronics Engineers Inc., 1992. pp. 573-576 (ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings).

@inproceedings{14f15c1b3e4c46398dde170f91ebfb6e,

title = "Inductive techniques for formal verification of systolic array designs in dsp applications",

abstract = "In this paper we show how several inductivc techniques can be utilized to provide fast and efficient proofs to the correctness of systolic designs in digital signal processing (DSP) applications. These techniques exploit the repeatability, regularity, and locality nature of systolic arrays and algorithms in DSP to produce fast proofs independent on the array size. We show how inductive techniques can be applied to different array topologies suitable for DSP and also illustrate the structure of the verifier we developed to automate induction using logic programming.",

author = "Nam Ling and Timothy Shih and Jonathan Huang",

note = "Publisher Copyright: {\textcopyright} 1992 IEEE.; 1992 IEEE International Conference on Acoustics, Speech, and Signal Processing, ICASSP 1992 ; Conference date: 23-03-1992 Through 26-03-1992",

year = "1992",

doi = "10.1109/ICASSP.1992.226555",

language = "???core.languages.en_GB???",

series = "ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "573--576",

booktitle = "ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing",

}

Ling, N, Shih, T & Huang, J 1992, Inductive techniques for formal verification of systolic array designs in dsp applications. in ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing., 226555, ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings, vol. 5, Institute of Electrical and Electronics Engineers Inc., pp. 573-576, 1992 IEEE International Conference on Acoustics, Speech, and Signal Processing, ICASSP 1992, San Francisco, United States, 23/03/92. https://doi.org/10.1109/ICASSP.1992.226555

Inductive techniques for formal verification of systolic array designs in dsp applications. / Ling, Nam; Shih, Timothy; Huang, Jonathan.
ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing. Institute of Electrical and Electronics Engineers Inc., 1992. p. 573-576 226555 (ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings; Vol. 5).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Inductive techniques for formal verification of systolic array designs in dsp applications

AU - Ling, Nam

AU - Shih, Timothy

AU - Huang, Jonathan

PY - 1992

Y1 - 1992

N2 - In this paper we show how several inductivc techniques can be utilized to provide fast and efficient proofs to the correctness of systolic designs in digital signal processing (DSP) applications. These techniques exploit the repeatability, regularity, and locality nature of systolic arrays and algorithms in DSP to produce fast proofs independent on the array size. We show how inductive techniques can be applied to different array topologies suitable for DSP and also illustrate the structure of the verifier we developed to automate induction using logic programming.

AB - In this paper we show how several inductivc techniques can be utilized to provide fast and efficient proofs to the correctness of systolic designs in digital signal processing (DSP) applications. These techniques exploit the repeatability, regularity, and locality nature of systolic arrays and algorithms in DSP to produce fast proofs independent on the array size. We show how inductive techniques can be applied to different array topologies suitable for DSP and also illustrate the structure of the verifier we developed to automate induction using logic programming.

UR - http://www.scopus.com/inward/record.url?scp=85019595469&partnerID=8YFLogxK

U2 - 10.1109/ICASSP.1992.226555

DO - 10.1109/ICASSP.1992.226555

M3 - 會議論文篇章

AN - SCOPUS:85019595469

T3 - ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings

SP - 573

EP - 576

BT - ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 1992 IEEE International Conference on Acoustics, Speech, and Signal Processing, ICASSP 1992

Y2 - 23 March 1992 through 26 March 1992

ER -

Ling N, Shih T, Huang J. Inductive techniques for formal verification of systolic array designs in dsp applications. In ICASSP 1992 - 1992 International Conference on Acoustics, Speech, and Signal Processing. Institute of Electrical and Electronics Engineers Inc. 1992. p. 573-576. 226555. (ICASSP, IEEE International Conference on Acoustics, Speech and Signal Processing - Proceedings). doi: 10.1109/ICASSP.1992.226555

Inductive techniques for formal verification of systolic array designs in dsp applications

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this