A Temporal Logic for Multi-Level Reasoning About Hardware
The work
| Authors | Ben Moszkowski |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1982 |
| Citekey | moszkowski1982temporal |
Where it appeared
| Publisher | Stanford University, Department of Computer Science |
|---|---|
| Number in series | STAN-CS-82-952 |
| School | Stanford University, Department of Computer Science |
Identifiers
| DOI | 10.21236/ada324174 |
|---|---|
| OpenAlex | W1992552504 |
| report_number | STAN-CS-82-952 |
Access
| Landing page | http://doi.org/10.21236/ada324174 |
|---|
Empty on purpose
| container |
Related
| Distinct from | bryant1987boolean |
|---|---|
| Distinct from | camilleri1986hardware |
| Distinct from | dhingra1987formal |
| Distinct from | gordon1983lcflsm |
| Distinct from | gordon1985hol |
| Distinct from | halpern1983hardware |
| Distinct from | leeser1988reasoning |
| Distinct from | moszkowski2006hierarchical |
| Distinct from | pnueli1977temporal |
| Superseded by | moszkowski1983reasoning |
| Superseded by | moszkowski1985temporal |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
Abstract : The paper describes a logical notation for reasoning about digital circuits. The formalism provides a rigorous and natural basis for device specification as well as for proving properties such as correctness of implementation. Conceptual levels of circuit operation ranging from detailed quantitative timing and signal propagation up to functional behavior are integrated in a unified way. A temporal predicate calculus serves as the formal core of the notation, resulting in a versatile tool that has more descriptive power than any conventional hardware specification language. The logic has been applied to specifying and proving numerous properties of circuits ranging from delay elements up to the AM2901 ALU bit slice. Presentations of a delay model and a multiplication circuit illustrate various features of the notation.
A copy is held
pdf, 5.0 MB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-09-16 01:23 UTC |
| Approved by | a person 2026-10-05 21:32 UTC |
Filed under
Cite it as
@techreport{moszkowski1982temporal,
title = {A Temporal Logic for Multi-Level Reasoning About Hardware},
author = {Ben Moszkowski},
year = {1982},
publisher = {Stanford University, Department of Computer Science},
school = {Stanford University, Department of Computer Science},
doi = {10.21236/ada324174},
}
This record lives at https://refs.drheap.org/moszkowski1982temporal/ and will keep doing so.