Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Functional Type Expressions of Sequential Circuits with the Notion of Referring Forms

Shunji Nishimura

TL;DR

The paper addresses a functional, time-aware analysis of sequential circuits by modeling them as causal stream functions $f: I^{\mathbb{N}_1} \to O^{\mathbb{N}_1}$ and introducing referring forms, derived from dependent-type–encoded domain restrictions, to characterize how circuits reference past inputs. It formalizes the relationship between Mealy machines and causal stream functions, and defines domain restriction maps $\phi$ and referring forms $\rho$ that capture memory usage across time. A key contribution is proving a universal time-preservation property for multiple clock-domain circuits, demonstrating that referring-forms sets preserve an implicit temporal order, and illustrating with D-FF, synchronous, and multi-clock scenarios, including a non-time-preserving counterexample. The framework offers a behavioral, type-theoretic lens for analyzing sequential circuits, with potential implications for circuit analysis, verification, and design.

Abstract

This paper introduces the notion of referring forms as a new metric for analyzing sequential circuits from a functional perspective. Sequential circuits are modeled as causal stream functions, the outputs of which depend solely on the past and current inputs. Referring forms are defined based on the type expressions of functions and represent how a circuit refers to past inputs. The key contribution of this study is identifying a universal property in multiple clock domain circuits using referring forms. This theoretical framework is expected to enhance the comprehension and analysis of sequential circuits.

Functional Type Expressions of Sequential Circuits with the Notion of Referring Forms

TL;DR

The paper addresses a functional, time-aware analysis of sequential circuits by modeling them as causal stream functions and introducing referring forms, derived from dependent-type–encoded domain restrictions, to characterize how circuits reference past inputs. It formalizes the relationship between Mealy machines and causal stream functions, and defines domain restriction maps and referring forms that capture memory usage across time. A key contribution is proving a universal time-preservation property for multiple clock-domain circuits, demonstrating that referring-forms sets preserve an implicit temporal order, and illustrating with D-FF, synchronous, and multi-clock scenarios, including a non-time-preserving counterexample. The framework offers a behavioral, type-theoretic lens for analyzing sequential circuits, with potential implications for circuit analysis, verification, and design.

Abstract

This paper introduces the notion of referring forms as a new metric for analyzing sequential circuits from a functional perspective. Sequential circuits are modeled as causal stream functions, the outputs of which depend solely on the past and current inputs. Referring forms are defined based on the type expressions of functions and represent how a circuit refers to past inputs. The key contribution of this study is identifying a universal property in multiple clock domain circuits using referring forms. This theoretical framework is expected to enhance the comprehension and analysis of sequential circuits.
Paper Structure (9 sections, 2 theorems, 9 equations, 6 figures)

This paper contains 9 sections, 2 theorems, 9 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Types of Causal Stream Functions
  4. Dependent Types
  5. Referring Forms
  6. Definition
  7. Examples
  8. Time Preservation
  9. Conclusion

Key Result

Lemma 1

Let $\rho$ be a referring form of multiple clock domain circuits. If $\rho_{m_1}$ contains $I$ at $l_1$, for an arbitrary $m_2 \ge m_1$, there exists $l_2 \ge l_1$ and $\rho_{m_2}$ contains $I$ at $l_2$.

Figures (6)

  • Figure 1: Referring form of D-FF.
  • Figure 2: Synchronous circuits.
  • Figure 3: Multiple clock domain circuits.
  • Figure 4: Two-clock domain circuit.
  • Figure 5: Pseudo-graph for referring forms of multiple clock domain circuits (Fig. \ref{['fig:DiagMCD']}).
  • ...and 1 more figures

Theorems & Definitions (7)

  • Definition 1
  • Definition 2
  • Definition 3
  • Lemma
  • proof
  • Theorem
  • proof