+++
title = "Verifying Stability Conditions on HLS"
date = "2022-10-04"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3c7"]
forwardlinks = ["3c8a"]
zettelid = "3c8"
+++

Currently, the correctness proof for HLS only takes into account the
actual correctness of the final result that is computed. Instead, it
would be useful to also have a notion of stability of the output. This
means that changes in the input to a different, equivalent program
should not result in a large difference in the design of the output.
However, even there, there are two possibilities:

-   Stability of performance metrics, such as latency, throughput and
    area.
-   Stability of architecture, which implies the above but may be
    restrictive.

It might be easiest to start by proving stability of the architecture
and see how restrictive that metric is, and how many optimisations do
not actually have that property.