Can I order PCB/chip manufacture from provided LOTOS specification?

Question

Is there a way to automatically deduct PCB and/or chip design from formal problem specification of a problem (task) which supposed to be solved on a PCB/chip?

I'm currently implementing solution with OpenCL to be run on GPGPU in conjunction with CPU. To decide which part of an algorithm must be run on CPU and which on GPU I had to manually calculate speed of sorting on CPU and GPU and divide by speed of GPU <-> CPU communication.

All sorts of such problems, I think, can be solved automatically by applying of problem description upon hardware specification. Googling all of these brought me to pretty complicated and abstract topic of formal methods where LOTOS seems to be one of them. I learned a little bit of electronics and know that in-circuit electronic processes and components are very well mathematically defined and deterministic, so automatic PCB/chip layout must be able to be deducted from problem description. But I can't find any working tools/libs which can already do it.

I wonder if there is already working solution of how to do it?

P.S. Problem I'm trying to solve is about ~50 lines of somewhat close-to-machine specification, but I had to write already ~5000 OpenCL/C++ code to run the solution upon a device which at first glance is at least 10000(!) times less effective (speed*power-wise) than analog ASIC would be. I feel like I wanna cry :(

Somewhat close task specification of my problem in C-like pseudocode:

[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 );

And I would like to tweak MEM_COUNT, CUR_COUNT and FARTHEST_COUNT to see the resulting speed/price/power/etc. As I know, today's CPUs designed so that a program needs to do ~300 operations per every memory access, but in algorithm above it goes up to FARTHEST_COUNT accesses per operation. So, ASIC would be 300*FARTHEST_COUNT times more efficient?

Answer 1

Currently, no. Formal methods have successful uses in restricted domains : static timing analysis (that an FPGA or other digital circuit) meets the timing constraints you ask for, for one example.

It can also prove properties about software or hardware - such as correctness of a program written in SPARK (based on Ada) - eliminating the need for runtime checks, guaranteeing the impossibility of buffer overruns, integer overflows, etc.

A little more generally, formal can potentially prove the equivalence of two designs - or a design and a higher level specification - exposing errors in the design, for example. See "equivalence checking" in ASIC design - hasn't made it down to FPGA tools yet, as far as I know.

But formal methods don't - yet - allow synthesis of a detailed design at a high level. (One could argue that a compiler is a formal translation of a "high level" specification in C or Ada, into an assembly language design, but I don't think you'd regard C as sufficiently high level, and I'd agree.

In any case, comments suggest you are dealing in the analog domain, which is arguably even more backward, SPICE netlists still seem to be state of the art. You may wish to flesh out the question with something specific - perhaps illustrating 1 or 5 of your 50 lines of specification, to give us a better idea what you're asking.