Master Internship: Assertion-Based Verification of hardware systems: generation of proper test sequences
 Duration: 6 months (beginning of 2012)


Description

The design of leading-edge hardware/software devices (PDAs, smartphones, digital cameras,...) is a complex process that increasingly involves the use and interconnection of large components. Guaranteeing their correctness is a challenging issue. In this context, Assertion-Based Verification can be of great help to verify the correctness of the systems under development: it involves formal or semi-formal methods to check whether the system complies with its requirements or expected behaviour, formalized as logic and temporal assertions (written in languages such as the IEEE standards PSL or SVA).
Various solutions exist for the construction of property checkers (monitors) from temporal assertions. Such property checkers are connected to the design under verification and inform about the satisfaction of the properties during simulation or FPGA emulation. In this process, guaranteeing that the property is not verified vacuously is crucial. Test sequences cannot be generated purely randomly: they must be designed to ensure a good coverage of the monitor's activation conditions. Consider as a trivial example a property of the form always(A implies B), which means that it is always true that, if A holds, then B also holds. If the testbench is such that A never holds, then the property is always verified, but verified vacuously i.e., without having actually been checked. In general, the form of the property can be more complex, and the Boolean sub-expressions involved in the temporal assertion (such as A and B in the example) can be expressions over the device primary inputs but also over its internal state and primary outputs. Thus, determining test sequences for the primary inputs that can ensure non vacuity does not have a straightforward solution.
The goal of the internship will be to take part in the research work of the VDS team of the TIMA Laboratory in this area. The team works towards the development of a specific method for the automatic test sequences generation directed by the necessity to avoid vacuous assertion satisfaction. The intern will have to: learn some notions related to hardware verification and more precisely to assertion-based verification, make a state of the art of research in coverage analysis, generation of test sequences related to temporal properties, etc..., and contribute to the development, implementation and test of algorithms for solving the problem described above.


Required skills:

Contact:
Prof. Laurence PIERRE
TIMA Laboratory
Laurence.Pierre@imag.fr
Tel. +33 (0)4 76 57 49 92