Verification Techniques for System-Level Design

Chapter 9. Conclusion

We have presented formal analysis and verification techniques for high-level design descriptions. The static analysis methods can detect various kinds of design inappropriateness without fully traversing the design descriptions and can be applied to large designs. Moreover, static analysis can support much wider language constructs such as model checking than can state traversal–based methods. One of the drawbacks of static analysis methods, however, is that they may generate false warnings, which is a major issue for future research. The equivalence-checking methods for C-based design languages work well for high-level design descriptions and in cases where the two descriptions to be compared are similar. Along with the ...