The use of fixed point induction in verifying systolic array designs : An applicative approach

機構典藏 > College of Engineering > Graduate Institute & Department of Computer Science and Information Engineering > Journal Article > Item 987654321/71608

Please use this identifier to cite or link to this item: https://tkuir.lib.tku.edu.tw/dspace/handle/987654321/71608

Title:	The use of fixed point induction in verifying systolic array designs : An applicative approach
Authors:	施國琛
Contributors:	淡江大學資訊工程學系
Keywords:	Systolic arrays;Equations;Design engineering;Logic programming;Humans;Topology
Date:	2002-08-06
Issue Date:	2011-10-24 01:24:54 (UTC+8)
Abstract:	The paper presents our applicative approach of using fixed point induction principle to verify the correctness of systolic array designs. Fixed point induction exploits the repeatable, regular, and local attributes of systolic arrays in realizing recursive functions. The applicative language in denotational semantics improves proof efficiency by skipping the redundant search time and space that occurred in other techniques. Our approach, as well as an example of applying it to prove a systolic array for matrix inversion, are provided in the paper.
Relation:	Midwest symposium on circuits and systems 36(2)
DOI:	10.1109/MWSCAS.1993.343224
Appears in Collections:	[Graduate Institute & Department of Computer Science and Information Engineering] Journal Article

Files in This Item:

File	Size	Format
index.html	0Kb	HTML	33	View/Open