Para garantizar los comportamientos correctos y que no hayan ingresado errores en el diseño, la tecnología de verificación de equivalencia juega un papel importante en el diseño VLSI. En este documento, proponemos un nuevo método de verificación de equivalencia semi-formal basado en plantillas para el diseño de sistemas basados en C y el diseño de implementación de Nivel de Transferencia de Registro (RTL)/netlist, cuyas estructuras internas pueden ser muy diferentes. Comenzando con una descripción basada en C como especificación, primero generamos aleatoriamente un conjunto de plantillas. Cada plantilla tiene una o un pequeño número de frases faltantes basadas en la descripción original en C. Muchos conjuntos de mutantes pueden ser representados por estas plantillas, utilizando constantes simbólicas, variables y operadores. El proceso de encontrar esas porciones faltantes puede formularse como un problema de Fórmula Booleana Cuantificada (QBF). Luego, basándonos en el método guiado por contraejemplos, al simular solo la implementación, las plantillas pueden ser refinadas. Dado que las plantillas se generan a partir de la descripción original en C, sus estructuras son muy similares entre sí. Con la descripción original en C como especificación, podemos simular o verificar formalmente la equivalencia entre la plantilla refinada y la descripción original en C, logrando así indirectamente la verificación de equivalencia del diseño de sistemas basados en C y la implementación de RTL/netlist. Los resultados experimentales en varios ejemplos prácticos demuestran la efectividad del método propuesto.