Seminar Room, ground floor (Building IMAG)
28 octobre 2016 - 15h00
Assertion and Measurements for Mixed-Signal Simulation (Phd Defense)
par Thomas FERRERE de Verimag
Abstract: This thesis is concerned with the monitoring of mixed-signal circuit simulations. In the field of hardware verification, the use of declarative property languages in combination with simulation is now standard practice. However the lack of features to specify asynchronous behaviors, or the insufficient integration of verification results, makes existing assertion and measurement languages unable to enforce mixed-signal requirements. We propose several theoretical and practical tools for the description and automatic monitoring of such behaviors, that feature both discrete and continuous aspects. For this we build on previous work on real-time extensions of temporal logic and regular expressions. We describe new algorithms to compute the distance from some simulation trace to temporal logic specifications, whose complexity is not higher than traditional monitoring. A novel diagnostic procedure is provided in order to efficiently debug such traces. The monitoring of continuous behaviors is then extended to other forms of assertions based on regular expressions. These expressions form the basis of our measurement language, that describes conjointly a measure and the patterns over which that measure should be taken. We show how other measurements implemented in analog circuits simulators can be ported to digital descriptions, this way extending structured verification approaches used for digital designs toward mixed-signal.
Jury:
- Oded MALER - Directeur de these
- Ernst CHRISTEN - Co-encadrant de these
- Javier ESPARZA - Rapporteur
- Ahmed BOUAJJANI - Rapporteur
- Jyotirmoy DESHMUKH - Rapporteur
- Alberto SANGIOVANNI-VINCENTELLI - Examinateur
- Thomas HENZINGER - Examinateur
- Dejan NICKOVIC - Examinateur
