Please use this identifier to cite or link to this item: doi:10.22028/D291-26469
Title: Designing correct recursive circuits using semantics-preserving transformations of nets
Author(s): Gamkrelidze, Alexander
Hotz, Günter
Zhu, Bin
Language: English
Year of Publication: 1998
DDC notations: 004 Computer science, internet
Publikation type: Report
Abstract: This paper will present a method of formal synthesis to design correct recursive circuits by using semantics-preserving transformations of nets (SPTNs). Its theoretical base is an algebraic calculus of nets. The calculus of nets is a hardware-specific calculus, and the transformations are circuit transformations themselves. Thus, it is much better adapted to the synthesis domain. The start point of the method is a conceptually simple specification for the required function. This specification can be easily proved to be correct, thereby the perplexed problem of the specification validation can be avoided. The specification is described compactly and graphically by a small kernel of recursive equations, and the synthesis task is simplified to transform these recursive equations in in the kernel. Because only semantics-preserving transformations are allowed in synthesis procedures, the synthesis result is not only a hardware implementation, but also a proof of correctness. We will illustrate two ways to transform a basic sorter into a odd-even-merging sorter, one being based on local incremantal transformations and the other being based on global partitions. The results show that there are circuits of practical interest, which can derived formally by using this method.
Link to this record: urn:nbn:de:bsz:291-scidok-51737
Series name: Technischer Bericht / A / Fachbereich Informatik, Universität des Saarlandes
Series volume: 1998/02
Date of registration: 4-Apr-2013
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
fb14_1998_02.pdf5,42 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.