kami/Kami/Ex/Names.v at 779e2a500d44c6d9882f42528d727b30e07a6062 · andres-erbsen/kami · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
From Coq Require Import String.

Local Open Scope string.
Definition procRqValidReg := "procRqValid".
Definition procRqReplaceReg := "procRqReplace".
Definition procRqWaitReg := "procRqWait".
Definition procRqReg := "procRq".
Definition l1MissByState := "l1MissByState".
Definition l1MissByLine := "l1MissByLine".
Definition l1Hit := "l1Hit".
Definition writeback := "writeback".
Definition upgRq := "upgRq".
Definition upgRs := "upgRs".
Definition ld := "ld".
Definition st := "st".
Definition drop := "drop".
Definition pProcess := "pProcess".

Definition cRqValidReg := "cRqValid".
Definition cRqDirwReg := "cRqDirw".
Definition cRqReg := "cRqReg".
Definition missByState := "missByState".
Definition dwnRq := "dwnRq".
Definition dwnRs_wait := "dwnRs_wait".
Definition dwnRs_noWait := "dwnRs_noWait".
Definition deferred := "deferred".

Definition rqFromProc := "rqFromProc".
Definition rsToProc := "rsToProc".
Definition rqToParent := "rqToParent".
Definition rsToParent := "rsToParent".
Definition rqFromChild := "rqFromChild".
Definition rsFromChild := "rsFromChild".
Definition fromParent := "fromParent".
Definition toChild := "toChild".
Definition line := "line".
Definition tag := "tag".
Definition cs := "cs".
Definition mcs := "mcs".
Definition mline := "mline".

Definition elt := "elt".
Definition enqName := "enq".
Definition deqName := "deq".
Definition enqP := "enqP".
Definition deqP := "deqP".
Definition empty := "empty".
Definition full := "full".
Definition firstEltName := "firstElt".

Definition addr := "addr".
Definition data := "data".
Definition dataArray := "dataArray".
Definition read := "read".
Definition write := "write".

Definition rqFromCToPRule := "rqFromCToP".
Definition rsFromCToPRule := "rsFromCToP".
Definition fromPToCRule := "fromPToC".

Definition read0 := "read0".
Definition read1 := "read1".
Definition read2 := "read2".
Definition read3 := "read3".
Definition read4 := "read4".
Definition read5 := "read5".
Definition read6 := "read6".
Definition read7 := "read7".
Definition read8 := "read8".
Definition read9 := "read9".

Close Scope string.

#[global] Hint Unfold
     procRqValidReg procRqReplaceReg procRqWaitReg procRqReg
     l1MissByState l1MissByLine l1Hit writeback
     upgRq upgRs ld st drop pProcess

     cRqValidReg cRqDirwReg cRqReg missByState
     dwnRq dwnRs_wait dwnRs_noWait deferred

     rqFromProc rsToProc rqToParent rsToParent
     rqFromChild rsFromChild fromParent toChild
     line tag cs mcs mline

     elt enqName deqName enqP deqP empty full firstEltName

     addr data dataArray read write
     read0 read1 read2 read3 read4 read5 read6 read7 read8 read9

     rqFromCToPRule rsFromCToPRule fromPToCRule
  : NameDefs.