Counting Solutions in the Field of Verification

In the last years the formal verification technique "property checking" was used to prove the correctness of microchip designs. This technique checks all possible input pattern which satisfy the design if these also valid for the given property. Such a property is given in a formal language, such as Verilog or VHDL, and describes certain aspects of a chip design. The "property checking" method brought a huge improvement compared to the simulation technique. This technique, however, just verifies a chip design point-wise, such that the global correctness of a design still is unproven. In case a property is faulty, it is of interest the know the number input patterns which lead to in incorrect output.

The goal of this project is to analyze these problems from the mathematical point view to check whether the number faulty input pattern is computable in a reasonable time. Therefore, the focus is on the techniques developed in the Valse-XT project. In particular in which way these are extendable, to solve the counting problems efficiently.