on the design of a formal debugger for system architecture
Bruno Monsuez, Franck Védrine, Nicolas Vallée · International Conference on Circuits · 2008
System level design helps alleviate much of the burden of usual RTL level design except verification. Functional verification of system architecture may first seem easier at the higher level of abstraction. In fact, insight on fundamental aspects of semantics of system level design and impact on lower levels of abstraction makes it much harder. Formal verification has received till now little attention for functional verification of system architecture. However, formal verification may provide great benefits to the system level designers. In this paper, starting from the experiments we have conducted with analyzing and verifying SystemC models using formal verification techniques, we describe what a potentially very useful approach to build a formal debugger to verify system architectures designed using a modern system model language like SystemC or SystemVerilog. Key–Words: Formal debugger, SystemC, Hypergraphs, Abstract interpretation