symbolic simulation/abstract execution of HDL's 
Author Message
 symbolic simulation/abstract execution of 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 .  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



Wed, 27 Oct 1993 00:53:16 GMT  
 symbolic simulation/abstract execution of HDL's

Quote:

>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


I am working on embedding CHDDLs in proof systems. In particular a subset
of ELLA (see below) in the Lambda proof system. Having written a formal
operational semantics for ELLA, and embedding it in Lambda I am now working
on some small examples dealing with symbolic simulation.

My system allows you to do things like:

---------------------------     [1]
|- AND (one,zero) => zero

meaning that AND 1 0 evaluates to 0. This is done by expanding the
definition of the AND:

|- ...
-------------------------
|- CASE (one,zero) OF (one,one): one ELSE zero ESAC => answer
---------------------------
|- AND (one,zero) => answer

by applying a ruel which characterises the behaviour of a CASE we can
rewrite this to

|- answer = zero
---------------------------
|- AND (one,zero) => answer

and to [1]

More interestingly, however we can a symbolic simulation:

|- CASE (x,y) OF (one,one): one ELSE zero ESAC => answer
----------------------
|- AND (x,y) => answer

Because we don't have any more information about x and y this is what we
get stuck with. We can however, push the computation into the answer so
that we get:

----------------------
|- AND (x,y) => CASE (x,y) OF (one,one): one ELSE zero ESAC

This is not very useful in this case, but when dealing with an adder say we
can prove the following rule:

|- sum = (x+y+c) mod n  |- carry = (x+y+c) div n
---------------------------------------------------     [2]
|- ADD n (x,y,c) => (sum,carry)

or:

---------------------------------------------------     [3]
|- ADD n (x,y,c) => ( (x+y+c) mod n, (x+y+c) div n )

Here we have a general n bit adder, which we have proved correct with
respect to its specification (ie its output is the sum, carry pair)
Using this, we can derive the rules [2] and [3]. That is,
once we have proved a circuit implements its specification we can use the
specification when simulating the circuit. This is one example of mixed
level simulation which this framework allows.

We can prove for example that

------------------------------
|- HALFADDER x zero => (x,zero)

i.e. the carry will be zero, and the sum the as yet unknown value x.
This has been established by doing a straightforward symbloic simulation,
and may be saved as a derived rule. Derived rules are very useful, in that
once we have symbolically simulated a circuit, we can reapply this
simulation with known values in place of the variables *in one step*.

A very interesting and novel way of using symblic simulation is not to
allow not just symbolic variables, but also *symbolic circuits*. Think opf
plug in components as a circuit of which you know the specification, but
not its actual body/implementation. A normal simulator cannot work with
this, but in my framework you can still simulate it.

We know that the component satisfies its specification:

-----------------------------
|- PLUGIN_SPEC (unknown_impl)

PLUGIN_SPEC(unknown_impl) |- derive output here, using spec.
-----------------------------------
PLUGIN_SPEC(unknown_impl) |- PLUGIN unknown_impl => output

For example, if the component is an adder the spec would be as in [2], [3]
above and the we'd derive that output is in fact the sum and carry.
Other usages of symbolic circuit simulations include simulations of general
design decompositions. Various design methodologies for creating
mathematically correct hardware can be used in conjunction with this approach.

The model behaves sensibly with delayless feedbacks and oscillating
circuits, buses (bidirectional wires) etc.
The examples so far have been at the gate level, but it is possible to
model circuits at the transistor level, using stored charge, overpowering,
multiple signal strengths etc etc. All the power of symbolic simulation may
be use at this level too.

Any way, all of this is not up to industrial strength yet, and not very
fast. However, I think it will become possible to deal with medium sized
circuits in the not so distant future. Witness the VIPER chip, which was
partially verified using the HOL higher order logic proof system.

Kees Goossens

I have written
"A Semantics for picoELLA" is a manuscript describing a formal
semantics for a subset of ELLA.
"Embedding CHDDLs in Proof systems" describes the general approach.
It will be presented as a paper in Turin at the
advanced research workshop on correct hardware design methodologies
in June 1991. It will be available as a LFCS technical report soon.
(Laboratory for the foundations of Computer Science, Department of computer
science, Edinburgh University, Scotland)
Send me some email for more information.

ELLA is a trademark of the Secretary of State for Defence, United Kingdom,
and is marketed by Computer General Electronic Design, The New Church,
Henry St, Bath, UK. ELLA was designed at the Royal Radar and Signals
Establishment (RSRE) in Malvern, UK, where ELLA research is ongoing.
I have no affiliation with either CGED or RSRE.
--
Kees Goossens                       Keep in Touch with the Dutch:

University of Edinburgh, Scotland   UUCP:  ..!mcsun!ukc!lfcs!kgg
Wiskunde is bouwen in de geest. --- Luitzen Egbertus Jan Brouwer.



Wed, 27 Oct 1993 23:37:16 GMT  
 
 [ 2 post ] 

 Relevant Pages 

1. C-based simulation faster than HDL-based simulation?

2. C-based simulation faster than HDL-based simulation?

3. Symbolic Execution, Paths Conditions and Constraints

4. Symbolic Simulation Position @ Rambus, Inc.

5. some questions on simulation using ACTIVE-HDL

6. verilog execution problem in rtl simulation

7. Execution Time for VHDL Simulations

8. CFP (2nd): Parallel Symbolic Computation Symposium '94 (PASCO'94)

9. CFP (2nd): Parallel Symbolic Computation Symposium '94 (PASCO'94)

10. Method type 'abstract'

11. 'Class'Input and abstract types

12. Hassan Ait-Kaci's _Warren's Abstract Machine_

 

 
Powered by phpBB® Forum Software