Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SynQ: An Embedded DSL for Synchronous System Design with Quantitative Types

Rui Chen, Ingo Sander

TL;DR

The paper tackles the challenge of semantic gaps in embedded system design by proposing SynQ, an Idris2-embedded EDSL for synchronous systems that enforces semantic coherency across specification, modelling, verification, and implementation. It achieves this through Quantitative Type Theory and a tagless final embedding, enabling a unified, manipulable design flow with explicit resource and state accounting. The authors present a two-layer semantics (combinational and sequential) with glue and atomic components, and demonstrate three interpreters that map SynQ terms to Idris2 functions, typed netlists, and transformed forms for design transformations, plus a case study on ISA design that highlights end-to-end coherence from specification to HDL generation. The work showcases a practical, formal approach to system design automation, enabling coherent multi-stage synthesis and verification while supporting hardware and software targetization.

Abstract

System design automation aims to manage the design of embedded systems with ever-increasing complexity. To the success of system design automation, there is still a lack of systematic and formal design process because an entire design process, from a system's specification to its implementation, has to deal with inherent concerns about the systems' different aspects and, consequently, inherent semantic gaps. These gaps make it hard for a design process to be traceable or transparent. Particularly, guaranteeing the correctness of produced implementations becomes the main challenge for a system design process. SynQ (Synchronous system design with Quantitative types) is an embedded domain specification language (EDSL) targeting the design of systems obeying the perfect synchrony hypothesis. SynQ is based on a component-based design framework and, by design, facilitates semantic coherency by leveraging the quantitative type theory (QTT) and language embedding. SynQ enables a semantically coherent design process, including formal specification and verification, modelling, simulation and code generation. This paper presents SynQ and its underlying formalism and demonstrates its features and potential for semantically coherent system design through a case study.

SynQ: An Embedded DSL for Synchronous System Design with Quantitative Types

TL;DR

The paper tackles the challenge of semantic gaps in embedded system design by proposing SynQ, an Idris2-embedded EDSL for synchronous systems that enforces semantic coherency across specification, modelling, verification, and implementation. It achieves this through Quantitative Type Theory and a tagless final embedding, enabling a unified, manipulable design flow with explicit resource and state accounting. The authors present a two-layer semantics (combinational and sequential) with glue and atomic components, and demonstrate three interpreters that map SynQ terms to Idris2 functions, typed netlists, and transformed forms for design transformations, plus a case study on ISA design that highlights end-to-end coherence from specification to HDL generation. The work showcases a practical, formal approach to system design automation, enabling coherent multi-stage synthesis and verification while supporting hardware and software targetization.

Abstract

System design automation aims to manage the design of embedded systems with ever-increasing complexity. To the success of system design automation, there is still a lack of systematic and formal design process because an entire design process, from a system's specification to its implementation, has to deal with inherent concerns about the systems' different aspects and, consequently, inherent semantic gaps. These gaps make it hard for a design process to be traceable or transparent. Particularly, guaranteeing the correctness of produced implementations becomes the main challenge for a system design process. SynQ (Synchronous system design with Quantitative types) is an embedded domain specification language (EDSL) targeting the design of systems obeying the perfect synchrony hypothesis. SynQ is based on a component-based design framework and, by design, facilitates semantic coherency by leveraging the quantitative type theory (QTT) and language embedding. SynQ enables a semantically coherent design process, including formal specification and verification, modelling, simulation and code generation. This paper presents SynQ and its underlying formalism and demonstrates its features and potential for semantically coherent system design through a case study.
Paper Structure (8 sections, 3 equations, 3 figures)

This paper contains 8 sections, 3 equations, 3 figures.

Table of Contents

  1. Introduction
  2. The Need and Challenge of Semantic Coherency
  3. The SynQ Language
  4. Contributions and Contents
  5. Preliminary
  6. Quantitative Type Theory
  7. Dependent Types
  8. Linear and Quantitative Types

Figures (3)

  • Figure 1: The visualisation of a top-down design flow under the three-stage decomposition view in which each plane corresponds to a design space at a specific abstraction level and exemplified artefacts that can will be produced in a C-centric design flow.
  • Figure 2: The illustration of the sequential composition of Mealy machines characterised by functions of type |(x: a) -> (st: s) -> (b, s)| and |(i: b) -> (st: s) -> (c, s)|, respectively, which share a state space with four states $s_1 \dots s_4$. The result of composition is another function of type |(x: a) -> (st: s) -> (c, s)|.
  • Figure 3: C functions that take pointers of states as input (a) and the corresponding Idris2 declarations that introduce these functions by the foreign function interface (FFI) (b).