More about simulation checking

Subject: More about simulation checking
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Thu Sep 26 2002 - 06:52:36 PDT

I understand that we don't want to get into a discussion of the precise
extent of the on-the-fly subset at this stage, I've got another comment
about useful restrictions for simulation checking:

If we are defining a subset which avoids some complications for implementation
in simulation, it may be worth saying something about the use of "forall".

For example, a property
forall x in {0:4095}
always ((accept & data_in = x) -> next (transmit and data_out = 11x + 9))
is reasonably easy to implement

but
forall x in {0:4095}
always((u = 7x + 3 and v = 5x + 2) -> ........
requires some algorithm to find values of x satisfying the equations

It may be worth pointing out that the implementaion will be easier if
(loosely), when the parameter x occurs in left-hand sides of implications
in the main part of the property, it is by itself on one side of an
equation.

Anthony 

--
Anthony McIsaac

STMicroelectronics Limited
1000 Aztec West
Almondsbury
Bristol BS32 4SQ

Tel: ++44 (0)1454 462466
Fax: ++44 (0)1454 617910

Email: Anthony.McIsaac@st.com

This archive was generated by hypermail 2b28 : Thu Sep 26 2002 - 06:54:12 PDT