Formal Verification of a Programmable Hypersurface

TL;DR

This paper discusses the ongoing development and formal verification of a programmable hypersurface, aiming to improve design robustness and reduce manufacturing costs through rigorous evaluation procedures.

Contribution

It introduces a formal verification approach for the Hypersurface network, integrating iterative design and evaluation to enhance robustness and resource efficiency.

Findings

Formal verification guided design improvements

Reduced manufacturing costs through rigorous evaluation

Enhanced robustness of the Hypersurface network

Abstract

A metasurface is a surface that consists of artificial material, called metamaterial, with configurable electromagnetic properties. This paper presents work in progress on the design and formal verification of a programmable metasurface, the Hypersurface, as part of the requirements of the VISORSURF research program (HORIZON 2020 FET-OPEN). The Hypersurface design is concerned with the development of a network of switch controllers that are responsible for configuring the metamaterial. The design of the Hypersurface, however, has demanding requirements that need to be delivered within a context of limited resources. This paper shares the experience of a rigorous design procedure for the Hypersurface network, that involves iterations between designing a network and its protocols and the formal evaluation of each design. Formal evaluation has provided results that, so far, drive the development team in a more robust design and overall aid in reducing the cost of the Hypersurface manufacturing. This paper presents work in progress on the design and formal verification of a programmable Hypersurface as part of the requirements of the VISORSURF research programme (HORIZON 2020 FET-OPEN).