Correct compilation of specifications to deterministic asynchronous circuits
| Autor: | Amy E. Zwarico, Scott F. Smith |
|---|---|
| Rok vydání: | 1995 |
| Předmět: |
Correctness
Asynchronous system Programming language Computer science Concurrency Parallel computing computer.software_genre Theoretical Computer Science Hardware and Architecture Asynchronous communication Compiler Equivalence (formal languages) computer Equivalence (measure theory) Software Hardware_LOGICDESIGN Electronic circuit |
| Zdroj: | Formal Methods in System Design. 7:155-226 |
| ISSN: | 1572-8102 0925-9856 |
| DOI: | 10.1007/bf01384076 |
| Popis: | Powerful methods have been developed by A. martin and others wherby asynchronous circuits may be automatically constructed by starting from high-level specifications and incrementally transforming them into asynchronous circuits. In this paper we make the informal arguments for the correctness of this compilatin process mathematically rigorous. With rigorsouly justified transformations, specifications may be translated into circuits that provably meet their specification. A full proof of the correctness of the circuit compiler is given. Other results of independent interest include: the process model takes fairness of gates into account, hazard-freeness is formally defined, and all hazard-free circuits constructed solely of and, or, not gates and C elements are proven to behave deterministically to any outside observer. A novel notion of equivalence is used to justify the correctness of the compiler. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink