Wed, 15 May 91 17:54:02 GMT

Related articles |
---|

Re: symbolic simulation/abstract execution of HDL's kgg@lfcs.ed.ac.uk (1991-05-15) |

Newsgroups: | comp.compilers |

From: | kgg@lfcs.ed.ac.uk (Kees Goossens) |

Summary: | This (and more) is possible _now_ |

Keywords: | optimization, interpreter |

Organization: | The Lavatory for the Foundations of Computer Science |

References: | <1991May10.165316.22625@fs7.ece.cmu.edu> |

Date: | Wed, 15 May 91 17:54:02 GMT |

[reposted by the author from comp.lang.vhdl -John]

In article <1991May10.165316.22625@fs7.ece.cmu.edu> rajen@edsel.ece.cmu.edu (Ramchandani Rajen Sham) writes:

*>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. ...*

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 rule which characterises the behaviour of a CASE we can

rewrite this to

|- answer = zero

---------------------------

|- AND (one,zero) => answer

and then 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 rules:

|- 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.

(Here is a variable, not a value in the value domain.)

This has been established by doing a straightforward symbolic 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 of

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.

Suppose 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 "Semantics for picoELLA" is a manuscript describing a

formal semantics for a minimal subset of ELLA. "An Operational Semantics

for a Subset of the HDDL ELLA" is a manuscript describing a formal

semantics for a maximal 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 LFCS-91-155 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.

--

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.