Verification of Interconnects
Authors:
- Joosten, Sebastiaan J. C.
https://research.tue.nl/en/publications/verification-of-interconnects
Abstract:
A communication fabric, or a Network on Chip (NoC), is a way to combine hardware components. For the final hardware to function correctly, it is critical that at least this NoC functions correctly. Some methods to prove the correctness of NoCs exist. An important property of correct NoCs, which turns out to be particularly difficult to prove, is that local deadlocks should not arise. We call NoCs live if they do not have such local deadlocks. Liveness proofs for networks that are large enough to be interesting in practice, used to exist only on an abstract level, or rely heavily on information from the abstract level.
To prove correctness of the concrete implementation of a NoC, we view the network as a set of queues an other state-holding elements, together with some combinational logic. This view lies very close to the actual hardware implementation. Queues and other state-holding elements are annotated through their interface. For this reason, we call this view on hardware the `interface level’.
The gate level implementation of a NoC design can be translated to combinational logic. At the gate level implementations, hardware designers make use of open wires and multi-directional gates. Where usual translations of gate level implementations are restricted to acyclic circuits with only binary gates, we show how to translate a richer class of gates to Boolean formulas. These Boolean formulas represent the gate level implementation of a NoC design.
In a proof about the correctness of a NoC, it can be important to know whether some queues can hold packets in a specific way. Linear one-step inductive invariants turn out to be a powerful tool to answer this question. Finding the right linear one-step inductive invariant used to require a high level description of the NoC. The essential property that is used describes when a packet of a certain type enters or leaves a queue: when a transfer occurs. By translating this property to a linear term, we can identify the linear invariants about the NoC. This property turns out to be available at the interface level. We describe how to translate this property to a linear term. As a consequence, we can automatically derive linear inductive invariants at the interface level.
To determine whether or not a NoC is live turns out to be very challenging. At the abstract level, there is a method that answer this question only partially: given a NoC, it can either prove that it is live, or it will present a situation which might be a reachable local deadlock. The latter case leaves the option open that the situation is not a reachable deadlock, in which case we still do not know whether or not the NoC is live. However, this methods has a good performance, and can determine liveness of NoCs of realistic sizes. We show that there is a similar algorithm at the interface level. Given a gate-level hardware description of a NoC, together with an interface specification of the queues, we formulate a Satisfiability Modulo Theory (SMT) problem that has an answer if the NoC has a reachable local deadlock. For many NoCs, the SMT problem turns out not to have an answer, which can be verified with standard SMT solvers. This proves that these NoCs are live, using only information that is available at the interface level.
We also reproduce an abstract-level description from the interface level. To do so, we give a procedure that constructs a tree of synchronising and arbitrating elements from the interface descriptions. Next, we orient the elements, deriving a graph in which all components are similar to the components in the xMAS language, a language for describing NoCs at an abstract level, proposed around 2010. For NoCs that were generated from xMAS, the resulting reproduced NoC is not necessarily equal to the original xMAS. Instead, we define a property called `transfer equivalence’, and show that the resulting NoCs are transfer equivalent.
In addition to describing these novel techniques to analyse NoCs at the interface level, we have implemented the techniques as a proof of concept. Most of those implementations are now also available as part of a tool called Voi, which stands for `Verify on interfaces’. The tool Voi is implemented in Haskell, and we give some insight into its implementation. With this tool, we believe to have made a significant step towards the automated verification of gate-level descriptions of NoCs.
BibTeX entry:
@phdthesis{joosten2016verification,
abstract = {A communication fabric, or a Network on Chip (NoC), is a way to combine hardware components. For the final hardware to function correctly, it is critical that at least this NoC functions correctly. Some methods to prove the correctness of NoCs exist. An important property of correct NoCs, which turns out to be particularly difficult to prove, is that local deadlocks should not arise. We call NoCs live if they do not have such local deadlocks. Liveness proofs for networks that are large enough to be interesting in practice, used to exist only on an abstract level, or rely heavily on information from the abstract level.
To prove correctness of the concrete implementation of a NoC, we view the network as a set of queues an other state-holding elements, together with some combinational logic. This view lies very close to the actual hardware implementation. Queues and other state-holding elements are annotated through their interface. For this reason, we call this view on hardware the `interface level'.
The gate level implementation of a NoC design can be translated to combinational logic. At the gate level implementations, hardware designers make use of open wires and multi-directional gates. Where usual translations of gate level implementations are restricted to acyclic circuits with only binary gates, we show how to translate a richer class of gates to Boolean formulas. These Boolean formulas represent the gate level implementation of a NoC design.
In a proof about the correctness of a NoC, it can be important to know whether some queues can hold packets in a specific way. Linear one-step inductive invariants turn out to be a powerful tool to answer this question. Finding the right linear one-step inductive invariant used to require a high level description of the NoC. The essential property that is used describes when a packet of a certain type enters or leaves a queue: when a transfer occurs. By translating this property to a linear term, we can identify the linear invariants about the NoC. This property turns out to be available at the interface level. We describe how to translate this property to a linear term. As a consequence, we can automatically derive linear inductive invariants at the interface level.
To determine whether or not a NoC is live turns out to be very challenging. At the abstract level, there is a method that answer this question only partially: given a NoC, it can either prove that it is live, or it will present a situation which might be a reachable local deadlock. The latter case leaves the option open that the situation is not a reachable deadlock, in which case we still do not know whether or not the NoC is live. However, this methods has a good performance, and can determine liveness of NoCs of realistic sizes. We show that there is a similar algorithm at the interface level. Given a gate-level hardware description of a NoC, together with an interface specification of the queues, we formulate a Satisfiability Modulo Theory (SMT) problem that has an answer if the NoC has a reachable local deadlock. For many NoCs, the SMT problem turns out not to have an answer, which can be verified with standard SMT solvers. This proves that these NoCs are live, using only information that is available at the interface level.
We also reproduce an abstract-level description from the interface level. To do so, we give a procedure that constructs a tree of synchronising and arbitrating elements from the interface descriptions. Next, we orient the elements, deriving a graph in which all components are similar to the components in the xMAS language, a language for describing NoCs at an abstract level, proposed around 2010. For NoCs that were generated from xMAS, the resulting reproduced NoC is not necessarily equal to the original xMAS. Instead, we define a property called `transfer equivalence', and show that the resulting NoCs are transfer equivalent.
In addition to describing these novel techniques to analyse NoCs at the interface level, we have implemented the techniques as a proof of concept. Most of those implementations are now also available as part of a tool called Voi, which stands for `Verify on interfaces'. The tool Voi is implemented in Haskell, and we give some insight into its implementation. With this tool, we believe to have made a significant step towards the automated verification of gate-level descriptions of NoCs.},
author = {Joosten, Sebastiaan Jozef Christiaan},
bdsk-url-1 = {https://www.win.tue.nl/ipa/?event=verification-of-interconnects},
date-modified = {2021-09-18 15:51:30 -0400},
day = {24},
month = {Feb},
school = {Technische Universiteit Eindhoven},
title = {Verification of Interconnects},
url = {https://research.tue.nl/en/publications/verification-of-interconnects},
year = {2016}
}