Simulation in Hardware Design and Testing

Integrating Hardware Description

Languages and Proof Systems?

K.G.W.Goossens

Laboratory for Foundations of Computer Science

Department of Computer Science

University of Edinburgh

Scotland,UK

1The Problem

Simulation in Hardware Design and Testing

Hardware description languages(hdl s)have been used in industry since the1960s to document and simulate hardware designs.Simulation of hdl descriptions is very useful to ?nd design faults without the need to manufacture the design.A well known drawback of simulation,however,is that the number of input combinations(or test vectors)increases exponentially.For modern designs,it would take years to fully simulate a design.In practice a limited number of test vectors are used to probe the circuit,possibly failing to uncover faults.

Formal Hardware Veri?cation

Research into formal hardware veri?cation of hardware designs aims to address this prob-lem.A circuit and its speci?cation are given by mathematical descriptions.A mathe-matical proof system is then used to prove correctness of the design with respect to its speci?cation.Although the hardware veri?cation?eld is still young,notable achieve-ments include the formally veri?ed viper microprocessor which is manufactured and used commercially.However,most proposed methodologies are not automated,and need considerable expertise to be used.Although formal veri?cation methods remove the exponential explosion occurring for simulation,veri?cation takes substantial time.

A severe drawback is that many di?erent notations and tools are employed.Indus-trial hardware description languages have not yet been used,alienating the hardware veri?cation?eld from the industrial designers.

2The Solution

Our approach advocates the use of a hdl in conjunction with a proof system [3].

To be able to use a hdl in conjunction with a proof system,it must have a precise de?nition.We have provided a formal semantics for (a small subset of)a widely used industrial hardware description language called ella 1[1].Using a formal semantics it is possible to prove results about the behaviour of circuits.

This semantics has been embedded in the Lambda 2[2]proof 54df1f43be1e650e52ea99e5mbda is a higher order logic proof system which allows speci?cations of designs to be stated in a natural and succinct 54df1f43be1e650e52ea99e5ing the proof system,a number of results have been proved which con?rm the correctness of the simulation model which is used in the industrial simulator for ella .

ella circuit descriptions reside inside the proof system which allows their formal manipulation.It is now possible for industrial users to describe designs in a formal setting,while retaining a familiar ella notation.

formal HDL descriptions simulation results description

of behaviour or properties

speci?cations counter examples formal semantics formal synthesis formal circuit optimisations o G layout generators

handcrafted designs

synthesis tools

c r r r r r r r r r r r r r r r E

prove correct proof system

simulation ....

....export import

Figure 1:Embedding a hdl in a Proof System

We combine familiar notations (hdl )and techniques (e.g.simulation)with mathe-matical rigour (formal semantics,proof system).The fusion of a hdl and a proof system allows a number of di?erent methodologies and tools to be integrated into one framework.Moreover,we can easily interface with existing tools because the hdl provides a common medium.We will discuss some of the applications in more detail below.

3Proving General Properties About Circuits

Circuit descriptions are part of the proof 54df1f43be1e650e52ea99e5ing conventional hardware veri?cation methodologies we can prove,for example,that a circuit meets its speci?cation.We can also prove properties about all circuits,classes of circuits(such as N bit adders)or inpidual circuits.

??c:circuit.simulation of c cannot loop,and is monotone.

Proving a property about a class of circuits may be harder than proving it for a particular member,but the proof needs to be done only once.We can also deal with circuits which are parametrised on word length(e.g.N bit adders),or other circuits(i.e.contain plug-in components).

??N.adder N(x,y)(s,c)→s=abs?1((abs x+abs y)mod2N)∧

c=abs?1((abs x+abs y)p2N)

This example also illustrates the use of data abstraction.

4Abstractions in Hardware Design

Hardware designs span many levels of abstraction from behavioural descriptions down to,for example,gate level.Most hdl s do not provide facilities to link di?erent levels of abstraction.Although di?erent levels may be simulated and their outputs compared, they are only“proven correct”through exhaustive 54df1f43be1e650e52ea99e5ing a proof system di?erent levels of abstraction may be related formally,thus ensuring that no errors are introduced when going from one level to another.

Data Abstraction The representation of integers by bitstrings above,is an example of data abstraction.By de?ning the abstraction function abs,boundary problems such as over?ow often become more explicit.

Structural Abstraction Decomposition of hardware modules is essential in top-down design methodologies.Formal synthesis of hardware and re?nement based synthesis are paradigms which have been used in conjunction with proof systems. Temporal Abstraction Time is often observed di?erently at adjacent levels of abstrac-tion.A microcode instruction may take several clock cycles,and a whole microcode program may implement a single instruction level operation.Temporal abstraction functions relate various time scales in a formal manner,facilitating proofs of cor-rectness.

Behavioural Abstraction Often it is not desirable to specify the behaviour of a hard-ware module fully.We may not care what the behaviour of the component is for input combinations which will not occur.Loose speci?cations do not unnecessarily constrain implementations.

3

5Formal Symbolic Simulation

Simulating circuit descriptions using simple values(1and0)leads to an exponential increase in the number of test 54df1f43be1e650e52ea99e5ing extra values in the value domain,such as don’t care X,and don’t know U,somewhat relieves this problem.Symbolic simulation goes one step further and allows the use of variables x and formulae x∨y as inputs and outputs.The variable x is not a value in value domain,but ranges over all these values.Proof systems provide exactly the right environment for this sort of simulation. With the use of an industrial hdl,such as ella,we can perform any of the conventional (symbolic)simulations[4].

?simulate andgate x(y∨1)?x

andgate is part of the proof system,and we could replace it by any proof system term, as long as it evaluates to a circuit.For example,we can simulate N bit adders,for arbitrary N.

A very useful application is abstract hardware.During the course of a design,we often want to simulate it,even when some subcomponents have not been 54df1f43be1e650e52ea99e5ing variables to stand for unimplemented hardware we can still simulate the whole design, because we should know the speci?cations of the 54df1f43be1e650e52ea99e5ing proof system facilities the speci?cations can be used instead of a future implementation to compute the outputs.

6Formal Synthesis and Optimisation

Circuits may be produced inside the proof system,by formally veri?ed hardware gener-ators.The hardware generating function is proved correct once.All outputs from the function are then guaranteed to be correct.This output can then be exported out of the proof system to conventional tools such as layout generators.Of course,it is also possible to verify output from conventional synthesis tools,by importing the circuit de-scription into the proof system.Our work?ts in with interactive paradigms such as formal synthesis and re?nement based synthesis.

Other applications include formally veri?ed circuit optimisations.Semantically equiv-alent circuit descriptions may be swapped without changing the meaning of the circuit. It may also be possible to prove correct previously informal transformations and opti-misations.Transformational design methodologies have also been used successfully in conjunction with proof systems.

References

[1]Computer General Electronic Design,The New Church,Henry St,Bath BA11JR,England.The ELLA Language

Reference Manual,issue4.0,1990.

[2]Mick Francis,Simon Finn,and Ellie Mayger.Reference Manual for the Lambda System.Abstract Hardware Limited,

version3.2edition,November1990.

[3]K G W Goossens.Embedding a CHDDL in a proof system.In P Prinetto and P Camurati,editors,Advanced Research

Workshop on Correct Hardware Design Methodologies,pages359–374.North Holland,June1991.

[4]K G W Goossens.Operational semantics based formal symbolic simulation.In Higher Order Logic Theorem Proving

and Its Applications,September1992.A longer version is available as LFCS Report ECS-LFCS-91-231.

4

本文来源：https://www.bwwdw.com/article/mlal.html