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 hdl:20.500.11880/26525 http://dx.doi.org/10.22028/D291-26469 |
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 | Size | Format | |
---|---|---|---|---|
fb14_1998_02.pdf | 5,42 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.