Resumen

El diseño aritmético de la suma juega un papel crucial en los sistemas digitales de alto rendimiento. El documento propone un método sistemático para formalizar y verificar sumadores en un asistente de prueba formal C. El enfoque propuesto tiene éxito en la formalización de las implementaciones a nivel de compuertas y en verificar la corrección funcional de los sumadores más importantes de interés en la industria, de una manera fiel, escalable y modularizada. La metodología también se puede extender a otras arquitecturas de sumadores.

• Materias:Modelos matemáticos Conjuntos difusos Ecuaciones integrales Fusión de características Algoritmo de optimización
• Subjects:Mathematical models Fuzzy sets Integral equations Feature fusion Optimization algorithm
• Palabras claves:Suma; Aritmética; Diseño; Alto rendimiento; Sistemas digitales; Asistente de demostración formal.
• Keywords:Addition; Arithmetic; Design; High performance; Digital systems; Formal proof assistant c