🚀 go-pugleaf

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