¿Puedo ordenar la fabricación de PCB / chip de la especificación LOTOS proporcionada?

1

¿Hay una manera de deducir automáticamente el diseño de PCB y / o chip de la especificación formal del problema de un problema (tarea) que se supone que debe resolverse en un PCB / chip?

Actualmente estoy implementando una solución con OpenCL para ejecutarse en GPGPU junto con la CPU. Para decidir qué parte de un algoritmo debe ejecutarse en la CPU y cuál en la GPU tuve que calcular manualmente la velocidad de clasificación de la CPU y la GPU y dividir por la velocidad de la GPU < - > Comunicación de la CPU.

Creo que todo tipo de problemas de este tipo pueden resolverse automáticamente aplicando descripción del problema a especificación de hardware . Buscar en Google todos estos me llevó a un tema bastante complicado y abstracto de métodos formales donde LOTOS parece ser uno de ellos. Aprendí un poco de electrónica y sé que los procesos y componentes electrónicos en el circuito están muy bien definidos matemáticamente y son deterministas, por lo que el diseño automático de PCB / chip debe poder deducirse de la descripción del problema . Pero no puedo encontrar ninguna herramienta / libs de trabajo que ya pueda hacerlo.

Me pregunto si ya existe una solución que funcione sobre cómo hacerlo.

P.S. El problema que estoy tratando de resolver es aproximadamente ~ 50 líneas de especificación algo cercana a la máquina, pero tuve que escribir ya ~ 5000 códigos OpenCL / C ++ para ejecutar la solución en un dispositivo que a primera vista es de al menos 10000 (! ) veces menos efectivas (velocidad * en cuanto a potencia) de lo que sería el ASIC analógico. Siento que quiero llorar :(

Especificación de tarea algo cercana a mi problema en pseudocódigo tipo C:

[declarations]
struct A { float Temp; float Value };
A Mem[ MEM_COUNT ];
A Cur[ CUR_COUNT ];

[process #1]
A S;
S.Value = getCurrentInputValue( attachedCamera/Mic/textFile/etc. );
S.Temp = 1;
Cur[ end ] = S;
for each C in Cur:
    C.Temp += 1 - mod( C.Value - S.Value ) / C.Value;
approximately sort Cur by Temp;

[process #2]
A C = Cur[ 0 ];
for each M in Mem:
    float sum = 0;
    //farthest set is defined as each (MEM_COUNT / FARTHEST_COUNT)'th A starting from M
    for each farthest of M:
        sum += farthest.Value / FARTHEST_COUNT;
    M.Temp -= mod( sum - M.Value );

[process #3]
A M = find M with the most Temp from Mem[];
outputValueToAttachedPin( M.Value );

Y me gustaría ajustar MEM_COUNT, CUR_COUNT y FARTHEST_COUNT para ver la velocidad / precio / potencia / etc resultante. Como sé, las CPU de hoy en día están diseñadas para que un programa tenga que realizar unas 300 operaciones por cada acceso a la memoria, pero en el algoritmo anterior, el acceso a FARTHEST_COUNT depende de cada operación. Entonces, ¿ASIC sería 300 * FARTHEST_COUNT veces más eficiente?

    
pregunta Slav

1 respuesta

1

Actualmente, no. Los métodos formales tienen usos exitosos en dominios restringidos: el análisis de tiempo estático (que un FPGA u otro circuito digital) cumple con las restricciones de tiempo que solicita, por ejemplo.

También puede demostrar propiedades sobre software o hardware, como la corrección de un programa escrito en SPARK (basado en Ada), eliminando la necesidad de verificaciones en tiempo de ejecución, garantizando la imposibilidad de desbordamientos de búfer, desbordamientos de enteros, etc.

Un poco más generalmente, formal puede potencialmente probar la equivalencia de dos diseños, o un diseño y una especificación de nivel superior, por ejemplo, exponiendo errores en el diseño. Vea "verificación de equivalencia" en el diseño ASIC, hasta ahora no he llegado a las herramientas FPGA, por lo que sé.

Pero los métodos formales no permiten, sin embargo, la síntesis de un diseño detallado a un alto nivel. (Se podría argumentar que un compilador es una traducción formal de una especificación de "alto nivel" en C o Ada, en un diseño de lenguaje ensamblador, pero no creo que considere a C como un nivel suficientemente alto, y estoy de acuerdo .

En cualquier caso, los comentarios sugieren que se está tratando con el dominio analógico, que posiblemente sea más atrasado, las listas de redes de SPICE todavía parecen estar a la vanguardia. Es posible que desee desarrollar la pregunta con algo específico, tal vez ilustrando 1 o 5 de sus 50 líneas de especificación, para darnos una mejor idea de lo que está preguntando.

    
respondido por el Brian Drummond

Lea otras preguntas en las etiquetas