Leí que las pruebas y la verificación son diferentes, pero ¿de qué manera? Leí que alguien escribe teoría para probar que el hardware es "correcto" pero, ¿cómo se hace eso? Intenté leer Wikipedia y buscar en Google, pero terminé en una investigación demasiado avanzada (HOL4 y pruebas teóricas) o en marcas, estándares o en una capa obsoleta de abstracción de hardware obsoleta ("HAL") que parece que ya no se usa en general.
He creado una ALU de 4 bits (con Quartus) que realmente funciona si carga el FPGA con la ALU. Utilicé los primitivos lógicos y escribí pruebas para la ALU. Ahora quiero aprender más y entender la diferencia entre probar y verificar en general y cómo probar que un hardware real está funcionando correctamente.
Veo que ML se usa en proyectos que usan el proverbio del teorema HOL. ¿Es eso algo a mi alcance de comprensión y manejo si soy un programador e ingeniero intermedios? Conozco las matemáticas y la programación, pero no soy bueno en física.
Mi ALU funcionó y podría probarlo en Quartus, pero no sé qué es la "verificación formal". ¿Puedo hacerlo y, en caso afirmativo, cómo y qué debería aprender?
Probé con la asistente de pruebas Isabelle y escribiendo teoremas triviales con HOL que podría compilar y obtener el resultado esperado. No tengo mucha experiencia con ML pero creo que podría usarla ya que tengo experiencia en la escritura de C, ensamblaje y código de máquina.
¿Puede ayudarme a encontrar qué leer o responder a lo que debería aprender y estudiar?