lustrec / test / src / kind_fmcad08 / memory2 / MOESI_1.lus @ 22fe1c93
History | View | Annotate | Download (2.88 KB)
| 1 |
|
|---|---|
| 2 |
node Sofar( X : bool ) returns ( Sofar : bool ); |
| 3 |
let |
| 4 |
Sofar = X -> X and pre Sofar; |
| 5 |
tel |
| 6 |
|
| 7 |
node excludes4( X1, X2, X3, X4 : bool ) returns ( excludes : bool ); |
| 8 |
let |
| 9 |
excludes = not ( X1 and X2 or X1 and X3 or X1 and X4 or |
| 10 |
X2 and X3 or X2 and X4 or |
| 11 |
X3 and X4 ); |
| 12 |
tel |
| 13 |
|
| 14 |
node moesi(init_invalid_mo : int; etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool)returns( |
| 15 |
modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; erreur_mo : bool |
| 16 |
); |
| 17 |
var |
| 18 |
garde_mo1, garde_mo2, garde_mo3, garde_mo4 : bool; |
| 19 |
let |
| 20 |
|
| 21 |
garde_mo1 = pre invalid_mo >= 1; |
| 22 |
garde_mo2 = pre exclusive_mo>=1; |
| 23 |
garde_mo3 = pre shared_mo + pre owned_mo>=1; |
| 24 |
garde_mo4 = pre invalid_mo>=1; |
| 25 |
|
| 26 |
erreur_mo = false -> exclusive_mo >= 2; |
| 27 |
|
| 28 |
modified_mo = 0 -> |
| 29 |
if(etat_mo1) then if(garde_mo1) then 0 else pre modified_mo else |
| 30 |
if(etat_mo2) then if(garde_mo2) then pre modified_mo+1 else pre modified_mo else |
| 31 |
if(etat_mo3) then if(garde_mo3) then 0 else pre modified_mo else |
| 32 |
if(etat_mo4) then if(garde_mo4) then 0 else pre modified_mo else |
| 33 |
pre modified_mo; |
| 34 |
|
| 35 |
exclusive_mo = 0 -> |
| 36 |
if(etat_mo1) then if(garde_mo1) then 0 else pre exclusive_mo else |
| 37 |
if(etat_mo2) then if(garde_mo2) then pre exclusive_mo-1 else pre exclusive_mo else |
| 38 |
if(etat_mo3) then if(garde_mo3) then 1 else pre exclusive_mo else |
| 39 |
if(etat_mo4) then if(garde_mo4) then 1 else pre exclusive_mo else |
| 40 |
pre exclusive_mo; |
| 41 |
|
| 42 |
shared_mo = 0 -> |
| 43 |
if(etat_mo1) then if(garde_mo1) then pre shared_mo + pre exclusive_mo + 1 else pre shared_mo else |
| 44 |
if(etat_mo3) then if(garde_mo3) then 0 else pre shared_mo else |
| 45 |
if(etat_mo4) then if(garde_mo4) then 0 else pre shared_mo else |
| 46 |
pre shared_mo; |
| 47 |
|
| 48 |
invalid_mo = init_invalid_mo -> |
| 49 |
if(etat_mo1) then if(garde_mo1) then pre invalid_mo-1 else pre invalid_mo else |
| 50 |
if(etat_mo3) then if(garde_mo3) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else |
| 51 |
if(etat_mo4) then if(garde_mo4) then pre invalid_mo + pre modified_mo + pre exclusive_mo + pre shared_mo + pre owned_mo -1 else pre invalid_mo else |
| 52 |
pre invalid_mo; |
| 53 |
|
| 54 |
owned_mo = 0 -> |
| 55 |
if(etat_mo1) then if(garde_mo1) then pre owned_mo + pre modified_mo else pre owned_mo else |
| 56 |
if(etat_mo3) then if(garde_mo3) then 0 else pre owned_mo else |
| 57 |
if(etat_mo4) then if(garde_mo4) then 0 else pre owned_mo else |
| 58 |
pre owned_mo; |
| 59 |
|
| 60 |
tel |
| 61 |
|
| 62 |
node top( init_invalid_mo : int; |
| 63 |
etat_mo1, etat_mo2, etat_mo3, etat_mo4 : bool ) |
| 64 |
returns ( OK : bool ); |
| 65 |
var modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo: int; |
| 66 |
erreur_mo : bool; |
| 67 |
let |
| 68 |
( modified_mo, exclusive_mo, shared_mo, invalid_mo, owned_mo, erreur_mo ) = |
| 69 |
moesi(init_invalid_mo, etat_mo1, etat_mo2, etat_mo3, etat_mo4 ); |
| 70 |
OK = Sofar( excludes4(etat_mo1, etat_mo2, etat_mo3, etat_mo4) |
| 71 |
and init_invalid_mo > 0 ) |
| 72 |
=> not erreur_mo; |
| 73 |
--%PROPERTY OK=true; |
| 74 |
--%MAIN; |
| 75 |
tel |