Automatically adjusting system level designs after RTL/gate-level ECO

摘要

In this paper we discuss techniques by which system level designs in C can be automatically modified or refined to be equivalent to given implementation designs in RTLetlists, assuming that the numbers of statements in C to be changed are small, e,g., one to several statements. This can correspond to the cases when RTL/gate-level ECO (Engineering Change Order) happens, as under ECO usually small portions of designs or small functionalities are changed. In the proposed method, templates are generated from the original C descriptions by replacing a set of statements with parameterized and programmable statements having symbolic variables that represent program variables, constants, operators and others. Then the problem to refine templates so that the resulting C descriptions become equivalent to the implementation designs is formulated as a QBF (Quantified Boolean Formula) problem. The QBF problem is solved by repeatedly applying SAT solvers in incremental ways without any formal analysis on the implementation designs. Implementation designs are just simulated by a number of times. This process also generates a set of test patterns by which the equivalence between the C descriptions with refined templates and the implementations can be 100% guaranteed as long as the templates can capture the behaviors of the implementation designs. We show preliminary experimental results which show usefulness of the proposed approach.