Recently a lot of multimedia applications have been emerging on portable appliances. They require both the flexibility of upgradeable devices (traditionally software based) and a powerful computing engine (typically hardware). In this context, programmable HW and dynamic reconfiguration allow novel approaches to the migration of algorithms from SW to HW. Thus, in the frame of the Symbad project, we propose an industrial design flow for reconfigurable SoC. The goal of Symbad consists of developing a system level design platform for hardware and software SoC systems including formal and semi formal verification techniques.

Research in applied formal verification has become a hot topic in circuit and system design due to rising circuit complexity. Design verification presents the biggest bottleneck in digital hardware design. Major hardware bugs found in ASIC design may cause expensive project delays when they are discovered during system test on the real silicon chip. The consequences are severe, from cost overruns to lost market opportunity. Simulation and emulation tools, which are traditionally used to find bugs in a design, often cannot find the corner cases or hard-to-find bugs that may occur only after hundreds of thousands of cycles, and are well beyond the reach of conventional simulation and emulation technologies. Formal methods have emerged as an alternative approach to ensure the quality and correctness of hardware designs, overcoming some of the limitations of traditional validation techniques such as simulation and testing.

Compares our linear programming technology for software verification (LPV) with other verification systems: explicit exploration using partial order reduction (Spin) and implicit exploration using BDDs (Xeve/Esterel). The case study is a safety property of an easily-scalable problem (a bus arbiter). The results show that exploration-based methods (Spin and Xeve/Esterel) have an overall exponential complexity, restricting their use on small instances. The LPV technique, which does not rely on exploration, is the only one fast enough (quadratic complexity) to handle systems that are 50 times larger than the other techniques presented in this paper can do. Moreover, in opposition to exploration-based methods, LPV produces real proven facts that mean this technique shares some common points with theorem proving. We believe that the scale-change robustness of LPV shows that linear programming can be applied successfully to the verification of industrial systems.