High Level Verification and Its Use at Pos-Silicon Debugging and Patching

In this paper, we first discuss about high level formal verification and analysis techniques targeting C-based designs. They are based on dependence traversal and analyze design descriptions locally. An equivalence checking technique based on dependence traversal of the difference between the two design descriptions is shown. Then we introduce special mechanisms called patchable accelerators, for post-silicon verification and debugging which can automatically be high level synthesized from C-based design descriptions. By using the patch logic in the synthesized accelerators, values of internal signals can be observed and controlled. With those information, a post-silicon debugging technique based on symbolic traverse of the dependency in C-based design description is developed.