A Quantitative Type Approach to Formal Component-Based System Design

Functional programming languages are recognised for their high abstraction level, high expressiveness, formal semantics, and correspondence to formal logic. However, the utilisation of functional languages in system design is limited because the existence of stateful, black-box components, e.g., simulation models and legacy components, breaks the functional languages’ ground. Existing solutions to this situation, e.g. monads, are sub-optimal due to their ad-hoc and overconstrained nature. To address this challenge, we employ the quantitative type theory (QTT), which combines the dependent and linear (resource) type systems, for component specification. QTT enables stateful components to be used as pure functions with minimised restrictions. To this end, a functional language with QTT can be used for glue specification in a component-based design framework with all its advantages leveraged. The proposed approach is demonstrated by a case study in which a QTT-based RV32I instruction set architecture (ISA) specification in Idris2, a Haskell-like language, is simulated, verified, transformed and implemented in Verilog HDL by utilising properties of pure functions, which confirms the advantages of the proposed approach.