Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:




Library Locked Library locked




Author, Editor(s)
Author(s):
Basin, David A.
Brown, G. M.
Leeser, M. E.		dblp
dblp
dblp

BibTeX cite key*:

Basin91c

Title

Title*:

Formally Verified Synthesis of Combinational CMOS Circuits

Journal

Journal Title*:

Integration: The Intern. Journal of VLSI Design
Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:


Publisher's URL:


Publisher's
Address:


ISSN:


Vol, No, pp, Date

Volume*:

11
Number:


Publishing Date:

1991

Pages*:

235-250
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

We present a system for simultaneously synthesizing and proving correct CMOS implementations of combinational circuits. Our system, developed within the Nuprl proof development system, is based on a set of transformation rules that generate CMOS implementations from their logical specifications. Our research differs from previous work in three important ways: our rules are rigorously proven with respect to a formal transistor model, our transformation rules admit the synthesis of both pass transistor and series/parallel networks, and our implementation produces a human readable proof along with each circuit it synthesizes.} } %erg,

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:


Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:


BibTeX Entry:
@ARTICLE{Basin91c,
AUTHOR = {Basin, David A. and Brown, G. M. and Leeser, M. E.},
 TITLE = {Formally Verified Synthesis of Combinational {CMOS} Circuits},
 JOURNAL = {Integration: The Intern. Journal of VLSI Design},
 YEAR = {1991},
 VOLUME = {11},
 PAGES = {235--250},
}

Entry last modified by Uwe Brahm/MPII/DE, 08/06/2014
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]		Created
01/14/1995 06:50:39 PM
Revisions
3.
2.
1.
0.
Editor(s)
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Edit Dates
21/01/95 20:45:04
17/01/95 21:40:56
15/01/95 17:51:39
14/01/95 19:00:53