Distributed Formal Verification
Today, verification of industrial size designs like multi-million gate ASICs (Application Specific Integrated Circuit) and SoC (System-on-a-Chip) processors consumes up to 75% of the design effort. The trend to augment functional verification with formal verification tries to alleviate this problem. Efficient property checking algorithms based on binary decision diagrams (BDDs) and satisfiability (SAT) solvers allow automatic verification of medium-sized designs. However, the steadily increasing design sizes still leave verification the major bottleneck, because formal methodologies do not yet scale to very large designs.
One feasible way is to parallelize the model checker to handle the crux of the verification
problem for very large designs that is state explosion. The main idea of the approach is to
split/partition the state set into partitions and delegate traversal of these subsets to
nodes on a cluster computer. Detecting a target/error state on one node can immediately
abort computation on all other. Parallel computation can show approximate linear speedups
in execution time and enables faster verification of properties. This is not only true
because of the reduced memory requirements, but also because the parallel algorithm is
not sensitive to the scheduling of partition traversal. The following figure illustrates
the basic parallelization process.
Verification of Embedded Software
The verification of complex systems, like embedded systems as well as SoCs, can not be considered only on hardware module level anymore. The amount of software has increased significantly over the last years and therefore, the verification of embedded software has become a fundamental importance. However, the complexity of embedded software is much higher than for the hardware. In software, complex structures are used to store the information, for instance, pointers, integer, floating-point, trees, chain lists, unions and structures. Nevertheless, the verification of embedded software is much of interest, which has timing and constraints description compared to the ordinary personal computer software. Therefore, our ESW is constrained to the MISRA (Motor Industry Software Reliability Association) standard, which is a standard for C programs in the automotive industry. This standard restricts the recursion and arithmetic operation on pointers. The verification of a temporal property in the realm of ESW is still a concern. So, our research at Tübingen focuses on developing methodologies to tackle the verification problems for ESW. The following figure explicates the basic flow that we use for ESW verification.