move everything out of trunk

[lttv.git] / trunk / verif / Spin / Test / snoopy

diff --git a/trunk/verif/Spin/Test/snoopy b/trunk/verif/Spin/Test/snoopy
deleted file mode 100755 (executable)
index 20c0294..0000000
--- a/trunk/verif/Spin/Test/snoopy
+++ /dev/null
@@ -1,257 +0,0 @@
-/* snooping cache algorithm
- */
-#define QSZ    2
-
-mtype = {      r, w, raw,
-               RD, WR, RX,
-               MX, MXdone,
-               req0, req1,
-               CtoB, BtoC,
-               grant, done
-       };
-
-chan tocpu0    = [QSZ] of { mtype };
-chan fromcpu0  = [QSZ] of { mtype };
-chan tobus0    = [QSZ] of { mtype };
-chan frombus0  = [QSZ] of { mtype };
-chan grant0    = [QSZ] of { mtype };
-
-chan tocpu1    = [QSZ] of { mtype };
-chan fromcpu1  = [QSZ] of { mtype };
-chan tobus1    = [QSZ] of { mtype };
-chan frombus1  = [QSZ] of { mtype };
-chan grant1    = [QSZ] of { mtype };
-
-chan claim0    = [QSZ] of { mtype };
-chan claim1    = [QSZ] of { mtype };
-chan release0  = [QSZ] of { mtype };
-chan release1  = [QSZ] of { mtype };
-
-#define W      1
-#define R      2
-#define X      3
-
-proctype cpu0()
-{
-       xs fromcpu0;
-       xr tocpu0;
-       do
-       :: fromcpu0!r   -> tocpu0?done
-       :: fromcpu0!w   -> tocpu0?done
-       :: fromcpu0!raw -> tocpu0?done
-       od
-}
-
-proctype cpu1()
-{
-       xs fromcpu1;
-       xr tocpu1;
-       do
-       :: fromcpu1!r   -> tocpu1?done
-       :: fromcpu1!w   -> tocpu1?done
-       :: fromcpu1!raw -> tocpu1?done
-       od
-}
-
-proctype cache0()
-{      byte state = X;
-       byte which;
-
-       xr frombus0;
-       xr fromcpu0;
-       xs tocpu0;
-       xs tobus0;
-       xr grant0;
-       xs claim0;
-       xs release0;
-resume:
-       do
-       :: frombus0?RD ->
-               if
-               :: (state == W) -> state = R; tobus0!CtoB
-               :: (state != W) -> tobus0!done
-               fi
-       :: frombus0?MX -> state = X; tobus0!MXdone
-       :: frombus0?RX ->
-               if
-               :: (state == W) -> state = X; tobus0!CtoB
-               :: (state == R) -> state = X; tobus0!done
-               :: (state == X) -> tobus0!done
-               fi
-
-       :: fromcpu0?r ->
-               if
-               :: (state != X) -> tocpu0!done
-               :: (state == X) -> which = RD; goto buscycle
-               fi
-       :: fromcpu0?w ->
-               if
-               :: (state == W) -> tocpu0!done
-               :: (state != W) -> which = MX; goto buscycle
-               fi
-       :: fromcpu0?raw ->
-               if
-               :: (state == W) -> tocpu0!done
-               :: (state != W) -> which = RX; goto buscycle
-               fi
-       od;
-buscycle:
-       claim0!req0;
-       do
-       :: frombus0?RD ->
-               if
-               :: (state == W) -> state = R; tobus0!CtoB
-               :: (state != W) -> tobus0!done
-               fi
-       :: frombus0?MX -> state = X; tobus0!MXdone
-       :: frombus0?RX ->
-               if
-               :: (state == W) -> state = X; tobus0!CtoB
-               :: (state == R) -> state = X; tobus0!done
-               :: (state == X) -> tobus0!done
-               fi
-       :: grant0?grant ->
-               if
-               :: (which == RD) -> state = R
-               :: (which == MX) -> state = W
-               :: (which == RX) -> state = W
-               fi;
-               tocpu0!done;
-               break
-       od;
-       release0!done;
-
-       if
-       :: (which == RD) -> tobus0!RD -> frombus0?BtoC
-       :: (which == MX) -> tobus0!MX -> frombus0?done
-       :: (which == RX) -> tobus0!RX -> frombus0?BtoC
-       fi;
-       goto resume
-}
-
-proctype cache1()
-{      byte state = X;
-       byte which;
-
-       xr frombus1;
-       xr fromcpu1;
-       xs tobus1;
-       xs tocpu1;
-       xr grant1;
-       xs claim1;
-       xs release1;
-resume:
-       do
-       :: frombus1?RD ->
-               if
-               :: (state == W) -> state = R; tobus1!CtoB
-               :: (state != W) -> tobus1!done
-               fi
-       :: frombus1?MX -> state = X; tobus1!MXdone
-       :: frombus1?RX ->
-               if
-               :: (state == W) -> state = X; tobus1!CtoB
-               :: (state == R) -> state = X; tobus1!done
-               :: (state == X) -> tobus1!done
-               fi
-
-       :: fromcpu1?r ->
-               if
-               :: (state != X) -> tocpu1!done
-               :: (state == X) -> which = RD; goto buscycle
-               fi
-       :: fromcpu1?w ->
-               if
-               :: (state == W) -> tocpu1!done
-               :: (state != W) -> which = MX; goto buscycle
-               fi
-       :: fromcpu1?raw ->
-               if
-               :: (state == W) -> tocpu1!done
-               :: (state != W) -> which = RX; goto buscycle
-               fi
-       od;
-buscycle:
-       claim1!req1;
-       do
-       :: frombus1?RD ->
-               if
-               :: (state == W) -> state = R; tobus1!CtoB
-               :: (state != W) -> tobus1!done
-               fi
-       :: frombus1?MX -> state = X; tobus1!MXdone
-       :: frombus1?RX ->
-               if
-               :: (state == W) -> state = X; tobus1!CtoB
-               :: (state == R) -> state = X; tobus1!done
-               :: (state == X) -> tobus1!done
-               fi
-       :: grant1?grant ->
-               if
-               :: (which == RD) -> state = R
-               :: (which == MX) -> state = W
-               :: (which == RX) -> state = W
-               fi;
-               tocpu1!done;
-               break
-       od;
-       release1!done;
-
-       if
-       :: (which == RD) -> tobus1!RD -> frombus1?BtoC
-       :: (which == MX) -> tobus1!MX -> frombus1?done
-       :: (which == RX) -> tobus1!RX -> frombus1?BtoC
-       fi;
-       goto resume
-}
-
-proctype busarbiter()
-{
-       xs grant0;
-       xs grant1;
-       xr claim0;
-       xr claim1;
-       xr release0;
-       xr release1;
-
-       do
-       :: claim0?req0 -> grant0!grant; release0?done
-       :: claim1?req1 -> grant1!grant; release1?done
-       od
-}
-
-proctype bus()         /* models real bus + main memory */
-{
-       xs frombus1;
-       xs frombus0;
-       xr tobus0;
-       xr tobus1;
-
-       do
-       :: tobus0?CtoB -> frombus1!BtoC
-       :: tobus1?CtoB -> frombus0!BtoC
-
-       :: tobus0?done -> /* M -> B */ frombus1!BtoC
-       :: tobus1?done -> /* M -> B */ frombus0!BtoC
-
-       :: tobus0?MXdone -> /* B -> M */ frombus1!done
-       :: tobus1?MXdone -> /* B -> M */ frombus0!done
-
-       :: tobus0?RD -> frombus1!RD
-       :: tobus1?RD -> frombus0!RD
-
-       :: tobus0?MX -> frombus1!MX
-       :: tobus1?MX -> frombus0!MX
-
-       :: tobus0?RX -> frombus1!RX
-       :: tobus1?RX -> frombus0!RX
-       od
-}
-
-init {
-       atomic {
-               run cpu0(); run cpu1();
-               run cache0(); run cache1();
-               run bus(); run busarbiter()
-       }
-}