String-Functional Semantics for Formal Verification of Synchronous Circuits

Abstract

A new functional semantics is proposed for synchronous circuits, as a basis for reasoning formally about that class of hardware systems. Technically, we define an extensional semantics with monotonic length-preserving functions on finite strings, and an intensional semantics based on functionals on those functions. As support for the semantics we prove the equivalence of the extensional semantics with a simple operational semantics, as well as a characterization of circuits which obey the every loop is clocked design rule. Also, we develop the foundations in complete detail both to increase confidence in the theory, and as a prerequisite to its future mechanization.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1988
Accession Number
ADA197008

Entities

People

  • Alexandre Bronstein
  • Carolyn Talcott

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Algebra
  • Automata Theory
  • Calculus
  • Classification
  • Computational Science
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Language
  • Mathematics
  • Numbers
  • Operating Systems
  • Semantics
  • Simulations

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Integrated Circuit Design and Technology.
  • Software Engineering