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