Modelling and verification of parameterized architectures: A functional approach

Salah Merniz, Saad Harous

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Pages (from-to)335-348
Number of pages14
JournalIET Computers and Digital Techniques
Volume15
Issue number5
DOIs
Publication statusPublished - Sep 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

Fingerprint

Dive into the research topics of 'Modelling and verification of parameterized architectures: A functional approach'. Together they form a unique fingerprint.

Cite this