-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMesi_pro1.smv
259 lines (241 loc) · 9.41 KB
/
Mesi_pro1.smv
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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
-- Nusmv specification for MESI protocol with trasient state
-- Single cache line per processor with 1-bit data
-- Hyeonwoo 2/14/2023
-- ******************************************************************
MODULE Cache(port_IO,bus_cmd,ack)
-- port_IO : 통로를 open,block 하는 param
-- message : 통롤르 통해 전달 받는 message(bus_rd,bus_rdx)
VAR
-- mode를 두개로
-- 1. 내가 할일 처리하는 => cpu로부터 state
-- 2. 받은 신호에 대한 처리를 하는
mode : {type1,type2,none};
state : {modified,exclusive, shared, invalid, i_trans,
modified_done,shared_done,invalid_done,exclusive_done,m_pending,s_pending};
-- cpu 의 요청 cache의 반응
cpu_request : {cpu_wr,cpu_rd,none}; -- cpu가 -> cache로 보내는 요청
-- cpu_request task_status에 따라 동작
-- 활동 권한
task_status : {ready,rd_status,wr_status,complete};
-- ready 는 준비상태 , rd,wr는 진행 상태 , complete는 state 가 변경되고 완료된 상태
bus_req : {bus_rd,bus_rdx,invalidate,none};
--/ task_status는 idle이다가 cache_port 가 열려 있으면서
--/ cache가 bus에게 메세지를 보낼때 rd_wait 또는 wr_wait 상태로 전환
--/ 이때 cpu가 다음 동작을 결정
-- DEFINE
-- RD_wait := state = invalid & cpu_request = cpu_rd;
-- WR_wait := state = invalid & cpu_request = cpu_wr;
ASSIGN
-- 1.내가 할일을 처리 하는 cpu
init(task_status) := ready;
next(task_status) :=
case
state = modified_done | state = exclusive_done | state = shared_done | state = invalid_done : complete;
task_status = complete : ready;
mode = type1 :
case
task_status = ready :
case
cpu_request = none : ready;
cpu_request = cpu_rd : rd_status;
cpu_request = cpu_wr : wr_status;
esac;
TRUE : task_status;
esac;
mode = type2 : -- bus 로 부터 받은 데이터 존재
case
task_status = ready :
case
bus_cmd = bus_rd : rd_status;
bus_cmd = bus_rdx : wr_status;
TRUE : task_status;
esac;
TRUE: task_status;
esac;
TRUE: task_status;
esac;
init(cpu_request) := none;
next(cpu_request):=
case
mode = type1 :
case
cpu_request = none & task_status = ready : {cpu_wr,cpu_rd};
task_status = rd_status | task_status = wr_status : cpu_request;
task_status = complete : none;
TRUE : cpu_request;
esac;
-- mode = type2 : none;
TRUE : none;
esac;
-- mode state 구현
init(bus_req) := none;
next(bus_req) :=
case
mode = type1 :
case
state = i_trans & task_status = wr_status : bus_rdx;
state = i_trans & task_status = rd_status : bus_rd;
state = modified & cpu_request = cpu_wr : bus_rdx;
state = shared & cpu_request = cpu_wr : bus_rdx;
TRUE : bus_req;
esac;
task_status = complete : none;
TRUE : bus_req;
esac;
init(mode) := none;
next(mode) :=
case
port_IO = TRUE : type1;
port_IO = FALSE : type2;
TRUE : mode;
esac;
init(state) := invalid;
next(state) := -- 시간을 맞춰주기 위해
case
state = exclusive_done : exclusive;
state = modified_done : modified;
state = shared_done : shared;
state = invalid_done : invalid;
mode = type1 :-- cpu_로부터
case
-- 1.0 cpu_request = none
cpu_request = none : state;
-- 1.1 invalid state --> bus를 통해 요청
state = invalid & cpu_request = cpu_wr & task_status = wr_status : i_trans;
state = invalid & cpu_request = cpu_rd & task_status = rd_status : i_trans;
-- 1.2 shared state -> 그대로 또는 변경
state = shared & cpu_request = cpu_wr : m_pending; -- 다른 cache 한테 invalidate 보내기
state = shared & cpu_request = cpu_rd : shared_done;
-- 1.3 exclusive state -> 그대로
state = exclusive & cpu_request = cpu_wr : exclusive_done;
state = exclusive & cpu_request = cpu_rd : exclusive_done;
-- 1.4 modified state
state = modified & cpu_request = cpu_wr : m_pending;
state = modified & cpu_request = cpu_rd : modified_done;
-- 1.5 i_trans state -> cpu_requset에 상관없이 그대로 유지
state = i_trans & ack = TRUE : s_pending;
state = i_trans & ack = FALSE : exclusive_done;
state = m_pending :
case
ack = TRUE : m_pending;
ack = FALSE : modified_done;
esac;
state = s_pending:
case
ack = TRUE : s_pending;
ack = FALSE : shared_done;
esac;
TRUE : state;
esac;
-- port_IO = FALSE & mode = type1 : state;
mode = type2 :
case
bus_cmd = invalidate : invalid_done;
task_status = ready : state;
task_status = rd_status :
case
state = invalid : invalid_done;
state = modified : shared_done;
state = exclusive : shared_done;
state = shared : shared_done;
TRUE : state;
esac;
task_status = wr_status : invalid_done;
task_status = invalidate : invalid_done;
TRUE : state;
esac;
TRUE : state;
esac;
-- END Cache
-- START main ******************************************************************
MODULE main
VAR
BUS_CMD : {bus_rd,bus_rdx,invalidate,none};
port_IO : array 0..1 of boolean; -- TRUE : open , FALSE : block
ack0 : boolean;
ack1 : boolean;
arbiter : {p0,p1,none};
c0 : Cache(port_IO[0],BUS_CMD,ack0);
c1 : Cache(port_IO[1],BUS_CMD,ack1);
ASSIGN
init(arbiter) := none;
next(arbiter) := {p0,p1,none};
ack0 :=
case
c1.state = invalid : FALSE;
c1.state = i_trans : FALSE;
TRUE : TRUE;
esac;
ack1 :=
case
c0.state = invalid : FALSE;
c0.state = i_trans : FALSE;
TRUE : TRUE;
esac;
-- ack2 :=
-- case
-- esac;
-- ack3 :=
-- case
-- esac;
init(port_IO[0]) := FALSE;
next(port_IO[0]) :=
case
port_IO[0] = TRUE :
case
c0.task_status = complete : FALSE; -- 열든 말든
TRUE : port_IO[0]; -- c0.task_status 가 아니면 유지
esac;
port_IO[0] = FALSE :
case
port_IO[1] = TRUE : FALSE;
port_IO[1] = FALSE :
case
arbiter = p0 : TRUE;
arbiter = p1 : FALSE;
-- ++++++++++++++++++++++++++++++++++++++++
-- arbiter = p2 : FALSE;
-- arbiter = p3 : TRUE;
-- ++++++++++++++++++++++++++++++++++++++++
arbiter = none : FALSE;
TRUE : FALSE;
esac;
TRUE : port_IO[0];
esac;
-- TRUE : port_IO[0];
esac;
init(port_IO[1]) := FALSE;
next(port_IO[1]) :=
case
port_IO[1] = TRUE :
case
c1.task_status = complete : FALSE;
TRUE : port_IO[1];
esac;
port_IO[1] = FALSE :
case
port_IO[0] = TRUE : FALSE;
port_IO[0] = FALSE :
case
arbiter = p0 : FALSE;
arbiter = p1 : TRUE;
arbiter = none : FALSE;
TRUE : FALSE;
esac;
esac;
TRUE : port_IO[1];
esac;
init(BUS_CMD) := none;
next(BUS_CMD) :=
case
port_IO[0] = TRUE : c0.bus_req;
port_IO[1] = TRUE : c1.bus_req;
TRUE : none;
esac;
-- END main ******************************************************************
SPEC AG!(c0.state = modified & c1.state = modified)
SPEC AG!(c0.state = modified & c1.state = exclusive)
SPEC AG!(c0.state = modified & c1.state = shared)
SPEC AG!(c0.state = exclusive & c1.state = shared)
SPEC AG!(c0.state = exclusive & c1.state = exclusive)
-- // 수정할 부분 ack 부분 , port 부분