Estoy tratando de averiguar los casos de esquina para verificar un FIFO síncrono durante la verificación del hardware.
Mi configuración es un FIFO síncrono (escritura / lectura) muy simple de dos puertos y la frecuencia de escritura de clk es la misma que la frecuencia de lectura de clk.
Para probar si se produce el desbordamiento de FIFO o no, ¿puede alguien ayudarme a identificar esos casos de esquina para que podamos verificar completamente este simple FIFO sincrónico?
Bien, se parece un poco más a un FIFO sincrónico normal pero:
Los casos de esquina de prueba son:
Los casos de prueba normales son foreach x en 1..N
Ejecutar siempre con cobertura de código y verificar la puntuación.
Puede que no se aplique a una pregunta de entrevista, pero en el mundo real, yo diría que usa una verificación formal.
Tuve que hacer esto una vez de verdad. Un diseño probado en silicio no hubiera funcionado en las frecuencias de reloj requiere el siguiente producto. Determinamos que los quince tenían problemas estructurales. Los rediseñé y quise asegurarme de que no rompí el diseño. Se verificó con estímulos aleatorios y algunas pruebas adicionales para llegar a los casos de esquina y se veía bien. Pero ...
Luego intenté verificar formalmente que las salidas serían equivalentes al diseño anterior en cada ciclo. En ningún momento la herramienta formal encontró una secuencia de entrada en la que teníamos el fifo vacío, lo llenábamos, lo dejábamos drenar y luego realizábamos una secuencia impar de lecturas con escrituras simultáneas, lo que hacía que los fifos difirieran en su salida. Era una traza de 11 ciclos y solo una entrada de 4 * fifo.
La moraleja es que para verificar algo simple como un solo quince, la verificación formal es tu amiga.
Lea otras preguntas en las etiquetas synchronous fifo