Abstract Execution of HLL's, HDL's

I am looking for any code that will enable me to perform symbolic
simulation/ abstract execution of any hardware description language, like
verilog, vhdl or isp or a high level procedural language like pascal or C.
I believe that such work is routinely done in optimizing compilers. It
would be nice if it has the capability of resolving brach conditions
whenever possible. Or on the other hand if you have some program that is
capable of deciding if a statement is true or false depending on the
conditions it has seen so far i would like to hear from you.


what is mean is: given the following hypothetical code fragment


sum = 0;
loop
    read ( x, y); -(1)
    if x > 2 then sum = sum + x - 2 else sum = sum + x ; -(2)
    if y > x && y > 2 then sum = sum + y - 2 else sum = sum + y; -(3)
end loop


the executer would trace a path thus
PC(1): input x1, y1;
PC(2): ( x1 > 2 AND sum = x1 - 2 ) OR
              (x1 <= 2 AND sum = x1)
PC(3): ( x1 > 2 AND sum = x1 - 2) AND (y1 > x1 && y1 > 2
                                                                                      AND sum = sum + y1 -2 )
              pruned to ( x1 > 2 AND y1 > x1 AND sum = x1 + y1 -4) by the resolver
[ i.e it was able to deduce that y1 >2 was redundant]
OR ( ...............................)


The last thing on this wish list of mine is if you have some program that
generates input data values to satisfy a given set of conditions, will be
equalities, inequalities and contain boolean operations.


If you have any pointers to similar work being done elsewhere i could like
to hear from you.


Thanks a lot
please email responses to rajen@edsel.ece.cmu.edu
--

Return to the comp.compilers page.
Search the comp.compilers archives again.