Logic Programming and the Specification of Circuits

The work

AuthorsW. F. Clocksin
Editors
Typetechreport
Year1985
Citekeyclocksin1985logic

Where it appeared

PublisherUniversity of Cambridge Computer Laboratory
Number in seriesUCAM-CL-TR-72
SchoolUniversity of Cambridge Computer Laboratory

Identifiers

DOI10.48456/tr-72
report_numberUCAM-CL-TR-72
ISSN1476-2986

Related

Distinct frombasin1989verification
Distinct fromcamilleri1986hardware
Distinct fromcamilleri1988simulation
Distinct fromgordon1983lcflsm
Distinct fromgordon1985why
Distinct fromhunt1994fm8501
Distinct fromleeser1988reasoning
Distinct frommelham1987abstraction
Distinct fromwinskel1987relating

From bibtex.

Abstract

Logic programming (see Kowalski, 1979) can be used for specification and automatic reasoning about electrical circuits. Although Propositional Logic has long been used for describing the truth functions of combinational circuits, the more powerful Predicate Calculus on which logic programming is based has seen relatively little use in design automation. Previous researchers have introduced a number of techniques similar to logic programming, but many of the useful consequences of the logic programming methodology have not been exploited. This paper first reviews and compares three methods for representing circuits, which will be called here the functional method, the extensional method, and the definitional method. The latter method, which conveniently admits arbitrary sequential circuits, is then treated in detail. Some useful consequences of using this method for writing directly executable specifications of circuits are described. These include the use of quantified variables, verification of hypothetical states, and sequential simulation.

A copy is held

pdf, 620.3 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-09-15 23:53 UTC
Approved bya person 2026-09-23 14:10 UTC

Cite it as

@techreport{clocksin1985logic,
  title        = {Logic Programming and the Specification of Circuits},
  author       = {W. F. Clocksin},
  year         = {1985},
  publisher    = {University of Cambridge Computer Laboratory},
  school       = {University of Cambridge Computer Laboratory},
  issn         = {1476-2986},
  doi          = {10.48456/tr-72},
}

This record lives at https://refs.drheap.org/clocksin1985logic/ and will keep doing so.