Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Zeitschriftenartikel

Modeling a Hardware Synthesis Methodology in Isabelle

MPG-Autoren
/persons/resource/persons44075

Basin,  David A.
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44446

Friedrich,  Stefan
Programming Logics, MPI for Informatics, Max Planck Society;

Externe Ressourcen
Es sind keine externen Ressourcen hinterlegt
Volltexte (beschränkter Zugriff)
Für Ihren IP-Bereich sind aktuell keine Volltexte freigegeben.
Volltexte (frei zugänglich)
Es sind keine frei zugänglichen Volltexte in PuRe verfügbar
Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
Zitation

Basin, D. A., & Friedrich, S. (1999). Modeling a Hardware Synthesis Methodology in Isabelle. Formal Methods in Systems Design, 15(2), 99-122.


Zitierlink: https://hdl.handle.net/11858/00-001M-0000-000F-3664-2
Zusammenfassung
Formal Synthesis is a methodology developed at Kent for combining circuit design and verification, where a circuit is constructed from a proof that it meets a given formal specification. We have reinterpreted this methodology in Isabelle's theory of higher-order logic so that circuits are incrementally built during proofs using higher-order resolution. Our interpretation simplifies and extends Formal Synthesis both conceptually and in implementation. It also supports integration of this development style with other proof-based synthesis methodologies and leads to techniques for developing new classes of circuits, e.g., recursive descriptions of parametric designs.