trunk/verif/Spin/Test/snoopy

   1 /* snooping cache algorithm
   2  */
   3 #define QSZ     2
   4
   5 mtype = {       r, w, raw,
   6                 RD, WR, RX,
   7                 MX, MXdone,
   8                 req0, req1,
   9                 CtoB, BtoC,
  10                 grant, done
  11         };
  12
  13 chan tocpu0     = [QSZ] of { mtype };
  14 chan fromcpu0   = [QSZ] of { mtype };
  15 chan tobus0     = [QSZ] of { mtype };
  16 chan frombus0   = [QSZ] of { mtype };
  17 chan grant0     = [QSZ] of { mtype };
  18
  19 chan tocpu1     = [QSZ] of { mtype };
  20 chan fromcpu1   = [QSZ] of { mtype };
  21 chan tobus1     = [QSZ] of { mtype };
  22 chan frombus1   = [QSZ] of { mtype };
  23 chan grant1     = [QSZ] of { mtype };
  24
  25 chan claim0     = [QSZ] of { mtype };
  26 chan claim1     = [QSZ] of { mtype };
  27 chan release0   = [QSZ] of { mtype };
  28 chan release1   = [QSZ] of { mtype };
  29
  30 #define W       1
  31 #define R       2
  32 #define X       3
  33
  34 proctype cpu0()
  35 {
  36         xs fromcpu0;
  37         xr tocpu0;
  38         do
  39         :: fromcpu0!r   -> tocpu0?done
  40         :: fromcpu0!w   -> tocpu0?done
  41         :: fromcpu0!raw -> tocpu0?done
  42         od
  43 }
  44
  45 proctype cpu1()
  46 {
  47         xs fromcpu1;
  48         xr tocpu1;
  49         do
  50         :: fromcpu1!r   -> tocpu1?done
  51         :: fromcpu1!w   -> tocpu1?done
  52         :: fromcpu1!raw -> tocpu1?done
  53         od
  54 }
  55
  56 proctype cache0()
  57 {       byte state = X;
  58         byte which;
  59
  60         xr frombus0;
  61         xr fromcpu0;
  62         xs tocpu0;
  63         xs tobus0;
  64         xr grant0;
  65         xs claim0;
  66         xs release0;
  67 resume:
  68         do
  69         :: frombus0?RD ->
  70                 if
  71                 :: (state == W) -> state = R; tobus0!CtoB
  72                 :: (state != W) -> tobus0!done
  73                 fi
  74         :: frombus0?MX -> state = X; tobus0!MXdone
  75         :: frombus0?RX ->
  76                 if
  77                 :: (state == W) -> state = X; tobus0!CtoB
  78                 :: (state == R) -> state = X; tobus0!done
  79                 :: (state == X) -> tobus0!done
  80                 fi
  81
  82         :: fromcpu0?r ->
  83                 if
  84                 :: (state != X) -> tocpu0!done
  85                 :: (state == X) -> which = RD; goto buscycle
  86                 fi
  87         :: fromcpu0?w ->
  88                 if
  89                 :: (state == W) -> tocpu0!done
  90                 :: (state != W) -> which = MX; goto buscycle
  91                 fi
  92         :: fromcpu0?raw ->
  93                 if
  94                 :: (state == W) -> tocpu0!done
  95                 :: (state != W) -> which = RX; goto buscycle
  96                 fi
  97         od;
  98 buscycle:
  99         claim0!req0;
 100         do
 101         :: frombus0?RD ->
 102                 if
 103                 :: (state == W) -> state = R; tobus0!CtoB
 104                 :: (state != W) -> tobus0!done
 105                 fi
 106         :: frombus0?MX -> state = X; tobus0!MXdone
 107         :: frombus0?RX ->
 108                 if
 109                 :: (state == W) -> state = X; tobus0!CtoB
 110                 :: (state == R) -> state = X; tobus0!done
 111                 :: (state == X) -> tobus0!done
 112                 fi
 113         :: grant0?grant ->
 114                 if
 115                 :: (which == RD) -> state = R
 116                 :: (which == MX) -> state = W
 117                 :: (which == RX) -> state = W
 118                 fi;
 119                 tocpu0!done;
 120                 break
 121         od;
 122         release0!done;
 123
 124         if
 125         :: (which == RD) -> tobus0!RD -> frombus0?BtoC
 126         :: (which == MX) -> tobus0!MX -> frombus0?done
 127         :: (which == RX) -> tobus0!RX -> frombus0?BtoC
 128         fi;
 129         goto resume
 130 }
 131
 132 proctype cache1()
 133 {       byte state = X;
 134         byte which;
 135
 136         xr frombus1;
 137         xr fromcpu1;
 138         xs tobus1;
 139         xs tocpu1;
 140         xr grant1;
 141         xs claim1;
 142         xs release1;
 143 resume:
 144         do
 145         :: frombus1?RD ->
 146                 if
 147                 :: (state == W) -> state = R; tobus1!CtoB
 148                 :: (state != W) -> tobus1!done
 149                 fi
 150         :: frombus1?MX -> state = X; tobus1!MXdone
 151         :: frombus1?RX ->
 152                 if
 153                 :: (state == W) -> state = X; tobus1!CtoB
 154                 :: (state == R) -> state = X; tobus1!done
 155                 :: (state == X) -> tobus1!done
 156                 fi
 157
 158         :: fromcpu1?r ->
 159                 if
 160                 :: (state != X) -> tocpu1!done
 161                 :: (state == X) -> which = RD; goto buscycle
 162                 fi
 163         :: fromcpu1?w ->
 164                 if
 165                 :: (state == W) -> tocpu1!done
 166                 :: (state != W) -> which = MX; goto buscycle
 167                 fi
 168         :: fromcpu1?raw ->
 169                 if
 170                 :: (state == W) -> tocpu1!done
 171                 :: (state != W) -> which = RX; goto buscycle
 172                 fi
 173         od;
 174 buscycle:
 175         claim1!req1;
 176         do
 177         :: frombus1?RD ->
 178                 if
 179                 :: (state == W) -> state = R; tobus1!CtoB
 180                 :: (state != W) -> tobus1!done
 181                 fi
 182         :: frombus1?MX -> state = X; tobus1!MXdone
 183         :: frombus1?RX ->
 184                 if
 185                 :: (state == W) -> state = X; tobus1!CtoB
 186                 :: (state == R) -> state = X; tobus1!done
 187                 :: (state == X) -> tobus1!done
 188                 fi
 189         :: grant1?grant ->
 190                 if
 191                 :: (which == RD) -> state = R
 192                 :: (which == MX) -> state = W
 193                 :: (which == RX) -> state = W
 194                 fi;
 195                 tocpu1!done;
 196                 break
 197         od;
 198         release1!done;
 199
 200         if
 201         :: (which == RD) -> tobus1!RD -> frombus1?BtoC
 202         :: (which == MX) -> tobus1!MX -> frombus1?done
 203         :: (which == RX) -> tobus1!RX -> frombus1?BtoC
 204         fi;
 205         goto resume
 206 }
 207
 208 proctype busarbiter()
 209 {
 210         xs grant0;
 211         xs grant1;
 212         xr claim0;
 213         xr claim1;
 214         xr release0;
 215         xr release1;
 216
 217         do
 218         :: claim0?req0 -> grant0!grant; release0?done
 219         :: claim1?req1 -> grant1!grant; release1?done
 220         od
 221 }
 222
 223 proctype bus()          /* models real bus + main memory */
 224 {
 225         xs frombus1;
 226         xs frombus0;
 227         xr tobus0;
 228         xr tobus1;
 229
 230         do
 231         :: tobus0?CtoB -> frombus1!BtoC
 232         :: tobus1?CtoB -> frombus0!BtoC
 233
 234         :: tobus0?done -> /* M -> B */ frombus1!BtoC
 235         :: tobus1?done -> /* M -> B */ frombus0!BtoC
 236
 237         :: tobus0?MXdone -> /* B -> M */ frombus1!done
 238         :: tobus1?MXdone -> /* B -> M */ frombus0!done
 239
 240         :: tobus0?RD -> frombus1!RD
 241         :: tobus1?RD -> frombus0!RD
 242
 243         :: tobus0?MX -> frombus1!MX
 244         :: tobus1?MX -> frombus0!MX
 245
 246         :: tobus0?RX -> frombus1!RX
 247         :: tobus1?RX -> frombus0!RX
 248         od
 249 }
 250
 251 init {
 252         atomic {
 253                 run cpu0(); run cpu1();
 254                 run cache0(); run cache1();
 255                 run bus(); run busarbiter()
 256         }
 257 }