| Summary: | In order to ensure the correct behaviors and that bugs have not entered the design, equivalence checking technology plays an important role in VLSI design. In this paper, we propose a new template-based, semi-formal equivalence checking method for C-based system design and Register Transfer Level (RTL)/netlist implementation design, whose internal structures can be very different. Staring with a C-based description as a specification, we first randomly generate a set of templates. Each template has one or a small number of missing sentences based on the original C description. Many sets of mutants can be represented by these templates, using symbolic constants, variables, and operators. The process of finding those missing portions can be formulated as a Quantified Boolean Formula (QBF) problem. Then, based on the counter-example guided method, by simulating only the implementation, the templates can be refined. Since the templates are generated from the original C description, their structures are very similar to each other. With the original C description as a specification, we can simulate or formally check the equivalence between the refined template and the original C description, thereby indirectly achieving the equivalence checking of the C-based systems design and RTL/netlist implementation design. The experimental results on several practical examples demonstrate the effectiveness of the proposed method.
|
|---|