Subject: FW: property examples for the database
From: Harry Foster (foster@rsn.hp.com)
Date: Wed May 02 2001 - 07:57:47 PDT
Hello Group,
Attached is a general list of example properties provided to
the committee by IBM.
Regards,
-Harry
-----Original Message-----
From: Ed Clarke [mailto:emc@cs.cmu.edu]
Subject: Fwd: property examples for the database
[Harry], can you forward this to the OVI group so that they will have
it for the next meeting. --Ed
-----Original Message-----
>From: eisner@il.ibm.com
>
>ed,
>
>attached are some properties, in english, that i have gathered for the
>database. i've collected them from a number of different designs. you can
>ignore the design number i note for each one, that is for internal use.
>
>regards,
>
>cindy.
>
>Cindy Eisner
>Formal Methods Group Tel: +972-4-8296-266
>IBM Haifa Research Laboratory Fax: +972-4-855-0070
>Haifa 31905, Israel e-mail:
>eisner@il.ibm.com
1. If a snoop hits a modified line in the l1 cache, then the next
transaction
must be a snoop writeback. (design 1)
2. If signal "enable" rises, then a clock after the fourth transfer signal
"pending" must rise. (design 1)
3. If signal "boff" is asserted, then if the first request which is
accepted
after the assertion of "boff" is not a snoop request, then it is a write
request. (design 1)
4. If signal "hit" is active and signal "pending" is not, then then next
time
signal "pending" is active, signal "sel5" is active. (design 1)
5. An urgent request should be the next handled. (design 2)
6. Between a request and its acknowledge the busy signal must remain
asserted.
(design 2)
7. If a data packet of any size starts and eventually gets a LAST bit,
then next data packet must have the FIRST bit asserted. (design 3)
8. If a write command starts and size=N (N=1 through 8), then N assertions
of signal "gx_start" should occur before the LAST bit goes active.
(design 3)
9. The address queue ptr increment consecutively (cyclic). In other words,
every time that an address is entered into the queue with queue ptr = N,
the next time that an address is entered into the queue, the address
will
be N+1 (cyclically). (design 4)
10. If data grant received then as soon as dbusy is high for two clocks,
take
the data bus. (design 5)
11. The data that returns for read is the last data that was written to the
register before the read was issued. (design 5)
12. Every buffer will be read before it is overwritten. (design 6)
13. A write request of a certain transfer size will result in an equivalent
number of data transfers. (design 6)
14. For every write, data transfers must alternate between odd and even
entries.
In other words, if there is a write, then as long as we are transferring
data belonging to this write, consecutive data transfers must alternate
between even and odd addresses. (design 6)
15. Two consecutive writes cannot be to the same address. (design 6)
16. If an address was set valid then the next time the "retire" signal is
asserted for this address, the address will be invalidated 3-8 clocks
laters. (design 6)
17. If read req is received, then either the next output req to PLB is read,
or
the one after that. (design 7)
18. If read req is received and then write req is received before read req
is
output, then read req will be output before write req is output. (design
7)
This archive was generated by hypermail 2b28 : Wed May 02 2001 - 07:58:56 PDT