Date and Time: Thursday, 17 September 2009, 15:30 - 16:30

Location: HG 6.96

Speaker: Matthias Raffelsieper (OAS)

Title: Formal Analysis of Verilog Cell Library Simulation Models

Abstract:

In the ValiChip project, formal verification of hardware descriptions is being studied. Especially, functional descriptions of cell libraries, which are collections of standard logic cores, in the hardware definition language Verilog are analyzed. Earlier, we provided a formal semantics for the subset of Verilog that is usually used in cell library descriptions. Together with a standard procedure to extract a formal model from a transistor netlist, we were able to implement a fully automatic equivalence checker for cell libraries.

In this talk, we focus on the non-determinism that is still present for Verilog descriptions at this level and poses a challenge to validation. Simulators resolve this problem by using certain rules to make the specification deterministic. This however is not justified by the behavior of the hardware that is to be modeled. Hence, simulation might not be able to detect certain errors.

We developed a technique to prove whether non-determinism does not affect the behavior of the simulation model, or whether there exists a situation in which the simulation model might produce different results. To make our technique efficient, we show that the global property of equal behavior for all possible evaluations is equivalent to checking only a certain local property. We also make use of additional information given in cell libraries to further restrict the possible behaviors. This allows the designer of a cell library to specify valid operational conditions by means of timing constraints. Therefore, we extend our technique to only consider non-determinism whenever it can be exhibited in a valid simulation run.

Our currently ongoing work, that is briefly sketched, extends the analysis of timing specifications to module paths, which specify that a changing input can cause a change in an output after some delay. We are currently developing techniques to on the one hand check whether a given path is feasible with respect to the functional description, and on the other hand to derive from a given functional description all possible module paths.