Abstract
The merit of higher order functions for hardware description and transformation is widely acknowledged by hardware designers. However, the use of higher order types makes their correctness proof very difficult. Herein, a new proof approach based on the principle of partial application is proposed which transforms higher order functions into partially applied first-order ones. Therefore, parameterised architectures modelled by higher order functions could be easily redefined only over first-order types. The proof could be performed by induction within the same specification framework that avoids translating the higher order properties between different semantics, which remains extremely difficult. Using the notion of parameterisation where verified components are used as parameters to build more complex ones, the approach fits elegantly in the incremental bottom-up design where both the design and its proof could be developed in a systematic way. The potential features of the proposed methodological proof approach are demonstrated over a detailed example of a circuit design and verification within a functional framework.
Original language | English |
---|---|
Pages (from-to) | 335-348 |
Number of pages | 14 |
Journal | IET Computers and Digital Techniques |
Volume | 15 |
Issue number | 5 |
DOIs | |
Publication status | Published - Sept 2021 |
Keywords
- electronic engineering computing
- formal specification
- functional programming
- hardware description languages
- hardware-software codesign
- network synthesis
ASJC Scopus subject areas
- Software
- Hardware and Architecture
- Electrical and Electronic Engineering