Journée du 13 Novembre 2009

Lieu

LIP6/Jussieu (salle 211, tour 55-65): comment y aller

Programme

14h00-15h00: G. Fey (Univ. Bremen), Computing Bounds for Fault Tolerance using Formal Techniques

Abstract: Continuously shrinking feature sizes result in an increasing susceptibility of circuits to transient faults, e.g. due to environmental radiation. Approaches to implement fault tolerance are known. But assessing the fault tolerance of a given circuit is a tough problem.

In this talk the use of formal methods to assess the robustness of a digital circuit with respect to transient faults is proposed. Our formal model uses a fixed bound in time to cope with the complexity of the underlying sequential equivalence check. The result is a lower and an upper bound on the robustness. The underlying algorithm and techniques to improve the efficiency are presented. In experiments the method is evaluated on circuits with different fault detection mechanisms.

15h00-15h30 : U. Kühne (Univ. Bremen), Verification of a pipeline processor from the instruction set architecture (ISA)

Abstract: Verification is a critical and costly step in the design of processors. For high quality results, the verification should be based on formal techniques like model checking. But, this requires a significant manual effort for setting up a good property suite that covers all possible bugs. Furthermore, a high level of expertise is needed in contrast to traditional simulation based methods. In the past, several methods have been proposed to raise the degree of automation in the verification of processors. While some approaches focus on incremental design and verification, others concentrate on the automated checking of specific features of a processor such as out-of-order execution or the forwarding control logic of the pipeline.

In this talk, an approach will be presented for the complete verification of processors based on architectural models. There, the textual specification is transformed to a formal architecture description that captures the instruction set architecture (ISA). The user then needs to specify how the ISA is mapped to the register transfer level (RTL) implementation. This is done by implementing a number of predefined predicates and functions that describe the generic concepts of a correct pipelined processor. Using this information, a property suite is generated that is complete by construction, i.e. no bugs can be missed. The properties are checked on the design automatically using a commercial model checking tool. By using the proposed technique, the productivity of the verification can be increased significantly when compared to a manual approach.

The use of architectural models in the formal verification suggests further applications such as the automatic generation of instruction set simulators (ISSs) or the automatic synthesis of embedded software. A short overview on these supplementary techniques will also be given in the talk.

15h30-16h00: pause café

16h00-16h30: vie du groupe