Verify over Interfaces
To prove correctness of the concrete implementation of a NoC, we view hardware 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’.
We have implemented techniques to analyse networks at the interface level 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.
Voi has a restrictive licence for academic use only. If this license is too restrictive for you, please contact the author, Sebastiaan J. C. Joosten, or use one of the following tools instead, which are Apache 2.0 licensed: