wanted information on Symbolic simulation of procedural languages

[Ramchandani Rajen Sham]

WANTED: Symbolic simulation/Abstract Execution Source code


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.  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 at edsel.ece.cmu.edu