Formal Verification of Hardware Designs

Team

Emmanuelle Encrenaz: Associate Professor

Jean-Lou Desbarbieux : Assistant Professor

Cécile Braunstein : Assistant Professor

Abdelrezzak Bara  : Research Engineer

Sana Younes  : Post-Doc

Former members (since 2000)

Soheib Baarir : Post-doc (oct. 2008 - aug. 2009)

Sami Taktak  : PhD Student (defended in jan. 2009)

Cécile Braunstein : Ms Student (2003) and PhD Student (defended in may 2007)

Vincent Beaudenon : PhD Student (defended in dec. 2006)

Cédric Roux : PhD Student (2001-)

Hassen Doghmen : Ms Student (2009)

Joel Ossima-Kheba : Ms Student (2002 and 2003)

Research topics

Our purpose is to promote the use of model-checking techniques in the hardware design process.

Our aim is to enhance classical techniques for model-checking hardware designs. We investigate four axis :

• Apply a property-dependant reduction to each parallel component of a distributed system in order to traverse a smaller state space during the model-checking verification.
• Use an extended decision-diagram structure to model-check finite-domain descriptions without having to re-encode them into BDD. The HADDOCK model-checker performs symbolic reachability analysis of static PROMELA programs. Its internal data structure is based on Set Decision Diagrams.
• Formalize an incremental design approach and the transformations of properties along the design process in order to automate some non-regression verifications.
• Automate the verification of absence of Deadlock in NoCs. The tool ODI is based on an original algorithm to guarantee the absence of deadlock, and can deal with inter-messages dependencies.

We also apply classical model-checking techniques to designs developed in the lab (in order to quantify the potential benefits of our ideas) :

• ZCSP (secure distant memory access without intermediary copy). Verification of liveness properties with SPIN.
• ANI (a low cost bus architecture). Verification of liveness properties with SPIN.
• RSPIN routers. Deadlock detection and correction with HADDOCK, a DDD-based model-checker.
• VCI-PI wrappers (protocol converters from VCI to PI bus and conversely). Verification of safety and liveness properties with VIS.

Projects and Collaborations

FME3 (2008-2010). Enhancing the detection of transient faults in circuits with formal methods. ANR Project, in collaboration with TIMA lab (L. Pierre and R. Leveugle).

SIMOP (2007-2009). Synergie between simulation and model-checking for ditributed control architectures. FARMAN Project, in collaboration with LSV (T. Chatain and L. Fribourg) and LURPA (B. Denis, O. deSmet, S. Ruel) labs.

VALMEM (2007-2009). Validation of timing characteristics in memory circuits described at transistor-level. ANR Project, in collaboration with LIP6 (P. Bazargan, P. Renault) , LSV (L. Fribourg) and STMicroelectronics (R. Chevallier).

BLUEBERRIES (2004-2007). Validation of response time of memory circuits. MEDEA+ Project, in collaboration with LSV (L. Fribourg) and STMicroelectronics (R. Chevallier) (during my position at LSV).

DESIGN AND VERIFICATION OF PROTOCOL CONVERTERS (WRAPPERS) (2001-2005). Thematic area of the joint laboratory CERME, between LIP5 and STMicroelectronics.

CLOVIS (1999-2001). Data decision diagrams for the verification of VHDL programs . DGA Research project in collaboration with LABRI (J.M. Couvreur) , LIP6 (D. Poitrenaud, E. Paviot-Adet).

Member of the CNRS-AS SoC thematic area "  Formal Verification " (2001-2002).

Member of the EUROSOC network proposal (2003).