A Symbolic Approach for Checking Functional and Timing Compatibility of Synthesized Designs

摘要

In a redesign situation, the compatibility of the replacement chips is critical. This can only be obtained by verifying both their functionality and timing. In this report, we will postulate that the general RTL verification problem is too difficult to be solved. Hence, it is necessary for a RTL verification system to trade off generality for usability. In fact, there is a real need for an automatic tool that can check the functional and timing compatibility of automatically synthesized chips quickly and effectively. We found that synthesized designs have several common properties that can be utilized to facilitate this task. By making use of the USC design data structure (DDS) graph models, we developed a hybrid symbolic approach that will not only verify functional compatibility but also take into account the timing and the interaction between the controller and the datapath. Experiments have been performed on two designs, an AR filter and a robot arm controller synthesized by the ADAM system. The results are very encouraging. In fact, these experiments helped to identify problems with the early version of the control signal generator (CSG) software.