ISSN:
1572-8102
Keywords:
hardware verification and synthesis
;
theorem proving
;
higher-order logic
;
higher-order unification
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract Formal Synthesis is a methodology developed at the university of 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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1023/A:1008758500273
Permalink