HAVEN

SystemVerilog Assertions (SVA) is a standardised language for specification of lineartime temporal properties of systems. Being a core part of SystemVerilog makes SVA easy to use for assertion-based verification of hardware systems. During the verification of a system, it is often useful to provide SVA formulae describing correct behaviour of interfaces of system’s subcomponents, so that any violation of an interface protocol during a verification run is captured and reported. Moreover, for standard interfaces, such as PCI or HyperTransport, there are packages with their description (either in SVA or in another assertion language) already available.

Due to its linear-time nature, any SVA formula can be effectively transformed into a Buchi automaton, which is in turn easily synthesisable into a finite-state machine in an FPGA. HAVEN allows the user to connect different Assertion Checkers to the verified system. An Assertion Checker represents one or more assertions and whenever a violation of any of the assertions is detected, a special packet with information about the nature of the violation is sent to the software environment for further analysis of the error.

A small demonstration video that shows the debugging process in HAVEN is available through this link. At first, you can see the run of the non-accelerated version of HAVEN (FRAMEWORK parameter set to 0), which ends with an assertion error after the 22. transaction is processed, so while processing the 23. transaction. The reason is that the input protocol of DUT has been violated. The second run demonstrates that we are able to detect the same violation also in the accelerated version of HAVEN (FRAMEWORK parameter set to 1). The run ended also while processing the 23. transaction.