Estamos estudiando el modelado y la verificación de un protocolo simple de coherencia de tejido de malla para verificar la simulación RTL. En el pasado, hemos desarrollado completamente nuestra propia solución para escuchar paquetes en la RTL y luego generar una respuesta esperada o múltiples respuestas posibles esperadas.
por ejemplo para un flujo como este:
Core Memory Controller
| |
| Request $Line in E-state |
+------------------------->|
| |
| Data |
<--------------------------|
| |
El verificador del controlador de memoria debe predecir que el paquete Data se devolverá al Core y cuál será la carga útil de ese paquete.
¿Cuáles son los marcos disponibles para modelar estos flujos? Soy consciente de TLM y lo estoy investigando. ¿Hay otros? Estoy abierto a cualquier idioma. ¿Existen herramientas de protocolo de verificación formal que también pueden generar comprobadores o aserciones?