Go backward to
A Simple Cached Memory
Go up to
Top
Go forward to
Formal Specification
A Simple Cached Memory (Contd)
A
get
(
m
)
<=>
cache
(
m
) =
bottom
and
A
(
cache
,
m
,
main
(
m
))
and
Unchanged
<
op
,
adr
,
val
,
main
>
A
cch
<=>
op
= "read"
and
cache
(
adr
)
notequal
bottom
and
op
' = "ready"
and
val
' =
cache
(
adr
)
and
Unchanged
<
main
,
cache
>
A
cch
<=>
op
= "write"
and
op
' = "ready"
and
A
(
cache
,
adr
,
val
)
and
Unchanged
main
A
fl
(
m
)
<=>
cache
(
m
)
notequal
bottom
and
(
op
notequal
"read"
or
m
notequal
adr
)
and
A
(
main
,
m
,
A
(
m
))
and
A
(
cache
,
m
,
bottom
)
and
Unchanged
<
op
,
adr
,
val
>
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998