1 | /* |
---|
2 | * gigamax.v |
---|
3 | * |
---|
4 | * author: Szu-Tsung Cheng (stcheng@ic.berkeley.edu) |
---|
5 | * date: 7/26/93 |
---|
6 | * |
---|
7 | * A verilog program using symbolic extension of vl2mv for |
---|
8 | * gigamax multiprocessor distributed, shared memory architecture |
---|
9 | * |
---|
10 | * from the example of gigamax.smv example in SMV system by |
---|
11 | * K. L. McMillan, et. al. |
---|
12 | */ |
---|
13 | |
---|
14 | typedef enum { idle, read_shared, read_owned, write_invalid, write_shared, |
---|
15 | write_resp_invalid, write_resp_shared, invalidate, response } |
---|
16 | command; |
---|
17 | typedef enum { invalid, shared, owned } status; |
---|
18 | typedef enum {r0,r1,r2,r3,r4,r5,r6,r7,r8} nine; |
---|
19 | |
---|
20 | |
---|
21 | module main (clk); |
---|
22 | |
---|
23 | input clk; |
---|
24 | |
---|
25 | command wire CMD; |
---|
26 | wire REPLY_OWNED, REPLY_WAITING, REPLY_STALL; |
---|
27 | command wire p0_cmd, p1_cmd, p2_cmd, m_cmd; |
---|
28 | wire p0_master, p0_reply_owned, p0_reply_waiting, p0_reply_stall, |
---|
29 | p1_master, p1_reply_owned, p1_reply_waiting, p1_reply_stall, |
---|
30 | p2_master, p2_reply_owned, p2_reply_waiting, p2_reply_stall, |
---|
31 | m_master, m_reply_owned, m_reply_waiting, m_reply_stall; |
---|
32 | command wire nond_CMD; |
---|
33 | wire nond0_master; |
---|
34 | wire nond1_master; |
---|
35 | wire nond2_master; |
---|
36 | wire nondm_master; |
---|
37 | |
---|
38 | processor p0(clk, CMD, p0_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL, |
---|
39 | p0_cmd, p0_reply_owned, p0_reply_waiting, p0_reply_stall); |
---|
40 | processor p1(clk, CMD, p1_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL, |
---|
41 | p1_cmd, p1_reply_owned, p1_reply_waiting, p1_reply_stall); |
---|
42 | processor p2(clk, CMD, p2_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL, |
---|
43 | p2_cmd, p2_reply_owned, p2_reply_waiting, p2_reply_stall); |
---|
44 | memory m(clk, CMD, m_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL, |
---|
45 | m_cmd, m_reply_owned, m_reply_waiting, m_reply_stall); |
---|
46 | |
---|
47 | assign REPLY_OWNED = p0_reply_owned | p1_reply_owned | p2_reply_owned, |
---|
48 | REPLY_WAITING = p0_reply_waiting | p1_reply_waiting | p2_reply_waiting, |
---|
49 | REPLY_STALL = p0_reply_stall | p1_reply_stall | p2_reply_stall | |
---|
50 | m_reply_stall; |
---|
51 | |
---|
52 | assign CMD = (p1_cmd==idle && p2_cmd==idle && m_cmd==idle) ? p0_cmd : |
---|
53 | (p0_cmd==idle && p2_cmd==idle && m_cmd==idle) ? p1_cmd : |
---|
54 | (p0_cmd==idle && p1_cmd==idle && m_cmd==idle) ? p2_cmd : |
---|
55 | (p0_cmd==idle && p1_cmd==idle && p2_cmd==idle) ? m_cmd : nond_CMD; |
---|
56 | |
---|
57 | assign p0_master = nond0_master; |
---|
58 | assign p1_master = (p0_master) ? 0 : nond1_master; |
---|
59 | assign p2_master = (p0_master || p1_master) ? 0 : nond2_master; |
---|
60 | assign m_master = ( (p0_master || p1_master) || p2_master) ? 0 : nondm_master; |
---|
61 | |
---|
62 | assign nond0_master = $ND(0,1); |
---|
63 | assign nond1_master = $ND(0,1); |
---|
64 | assign nond2_master = $ND(0,1); |
---|
65 | assign nondm_master = $ND(0,1); |
---|
66 | |
---|
67 | assign nond_CMD = $ND(idle, read_shared, read_owned, write_invalid, |
---|
68 | write_shared, write_resp_invalid, write_resp_shared, invalidate, response); |
---|
69 | |
---|
70 | endmodule |
---|
71 | |
---|
72 | |
---|
73 | |
---|
74 | module cache_device (clk, CMD, master, abort, waiting, state,snoop, reply_owned, |
---|
75 | readable, writable); |
---|
76 | input clk; |
---|
77 | input CMD; |
---|
78 | input master; |
---|
79 | input abort; |
---|
80 | input waiting; |
---|
81 | output state; |
---|
82 | output snoop; |
---|
83 | output reply_owned; |
---|
84 | output readable, writable; |
---|
85 | |
---|
86 | command wire CMD; |
---|
87 | wire master; |
---|
88 | wire abort; |
---|
89 | wire waiting; |
---|
90 | status reg state, snoop; |
---|
91 | wire readable, writable, reply_owned; |
---|
92 | |
---|
93 | status wire nond_snoop; |
---|
94 | status wire nond_state; |
---|
95 | |
---|
96 | assign readable = ((state == shared) || (state == owned)) && !waiting; |
---|
97 | assign writable = (state == owned) && (!waiting); |
---|
98 | assign reply_owned = (!master) && (state == owned); |
---|
99 | assign nond_snoop = $ND(shared,owned); |
---|
100 | assign nond_state = $ND(shared,invalid); |
---|
101 | |
---|
102 | initial begin state = invalid; end |
---|
103 | initial begin snoop = invalid; end |
---|
104 | |
---|
105 | always @(posedge clk) begin |
---|
106 | |
---|
107 | if (abort) begin snoop = snoop; end |
---|
108 | else if (!master && state==owned && CMD==read_shared) begin snoop = nond_snoop; end |
---|
109 | else if (master && CMD == write_resp_invalid) begin snoop = invalid; end |
---|
110 | else if (master && CMD == write_resp_shared) begin snoop = invalid; end |
---|
111 | |
---|
112 | if (abort) begin state = state; end |
---|
113 | else if (master == 1) |
---|
114 | begin |
---|
115 | case (CMD) |
---|
116 | read_shared: begin state = shared; end |
---|
117 | read_owned: begin state = owned; end |
---|
118 | write_invalid: begin state = invalid; end |
---|
119 | write_resp_invalid: begin state = invalid; end |
---|
120 | write_shared:begin state = shared; end |
---|
121 | write_resp_shared:begin state = shared; end |
---|
122 | endcase |
---|
123 | end |
---|
124 | else if (!master && state == shared && |
---|
125 | (CMD == read_owned || CMD == invalidate)) |
---|
126 | begin |
---|
127 | state = invalid; |
---|
128 | end |
---|
129 | else if (state == shared) |
---|
130 | begin |
---|
131 | state = nond_state; |
---|
132 | end |
---|
133 | end |
---|
134 | |
---|
135 | endmodule |
---|
136 | |
---|
137 | |
---|
138 | |
---|
139 | module bus_device(clk, CMD, master, REPLY_STALL, REPLY_WAITING, |
---|
140 | waiting, reply_waiting, abort); |
---|
141 | input clk; |
---|
142 | input CMD; |
---|
143 | input master; |
---|
144 | input REPLY_STALL; |
---|
145 | input REPLY_WAITING; |
---|
146 | output waiting; |
---|
147 | output reply_waiting; |
---|
148 | output abort; |
---|
149 | |
---|
150 | command wire CMD; |
---|
151 | wire master; |
---|
152 | wire REPLY_STALL, REPLY_WAITING; |
---|
153 | reg waiting; |
---|
154 | wire reply_waiting; |
---|
155 | wire abort; |
---|
156 | |
---|
157 | wire reply_waiting, abort; |
---|
158 | |
---|
159 | assign reply_waiting = !master && waiting; |
---|
160 | assign abort = REPLY_STALL || |
---|
161 | ((CMD == read_shared || CMD == read_owned) && REPLY_WAITING); |
---|
162 | |
---|
163 | initial waiting = 0; |
---|
164 | always @(posedge clk) begin |
---|
165 | if (abort) begin waiting = waiting; end |
---|
166 | else if (master && CMD == read_shared) begin waiting = 1; end |
---|
167 | else if (master && CMD == read_owned) begin waiting = 1; end |
---|
168 | else if (!master && CMD == response) begin waiting = 0; end |
---|
169 | else if (!master && CMD == write_resp_invalid) begin waiting = 0; end |
---|
170 | else if (!master && CMD == write_resp_shared) begin waiting = 0; end |
---|
171 | end |
---|
172 | |
---|
173 | endmodule |
---|
174 | |
---|
175 | |
---|
176 | |
---|
177 | module processor(clk, CMD, master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL, |
---|
178 | cmd, reply_owned, reply_waiting, reply_stall); |
---|
179 | input clk; |
---|
180 | input CMD; |
---|
181 | input master; |
---|
182 | input REPLY_OWNED, REPLY_WAITING, REPLY_STALL; |
---|
183 | output cmd; |
---|
184 | output reply_owned; |
---|
185 | output reply_waiting; |
---|
186 | output reply_stall; |
---|
187 | |
---|
188 | command wire CMD; |
---|
189 | wire master; |
---|
190 | wire REPLY_OWNED, REPLY_WAITING, REPLY_STALL; |
---|
191 | command wire cmd; |
---|
192 | wire reply_owned, reply_waiting, reply_stall; |
---|
193 | |
---|
194 | command wire nond_cmd; |
---|
195 | wire abort, waiting; |
---|
196 | status wire state, snoop; |
---|
197 | wire readable, writable; |
---|
198 | |
---|
199 | bus_device Bdevice(clk, CMD, master, REPLY_STALL, REPLY_WAITING, |
---|
200 | waiting, reply_waiting, abort); |
---|
201 | cache_device Cdevice(clk, CMD, master, abort, waiting, state,snoop, reply_owned, |
---|
202 | readable, writable); |
---|
203 | |
---|
204 | assign cmd = (master && state==invalid) ? nond_cmd : |
---|
205 | (master && state==shared) ? read_owned : |
---|
206 | (master && state==owned && snoop==owned) ? write_resp_invalid : |
---|
207 | (master && state==owned && snoop==shared) ? write_resp_shared : |
---|
208 | (master && state==owned && snoop==invalid) ? write_invalid : idle; |
---|
209 | |
---|
210 | assign nond_cmd = $ND(read_shared,read_owned); |
---|
211 | assign reply_stall = $ND(0,1); |
---|
212 | endmodule |
---|
213 | |
---|
214 | |
---|
215 | |
---|
216 | module memory (clk, CMD, master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL, |
---|
217 | cmd, reply_owned, reply_waiting, reply_stall); |
---|
218 | input clk; |
---|
219 | input CMD; |
---|
220 | input master; |
---|
221 | input REPLY_OWNED, REPLY_WAITING, REPLY_STALL; |
---|
222 | output cmd; |
---|
223 | output reply_owned, reply_waiting, reply_stall; |
---|
224 | |
---|
225 | command wire CMD; |
---|
226 | wire master; |
---|
227 | wire REPLY_OWNED, REPLY_WAITING, REPLY_STALL; |
---|
228 | command wire cmd; |
---|
229 | wire reply_owned, reply_waiting, reply_stall; |
---|
230 | |
---|
231 | wire abort; |
---|
232 | reg busy; |
---|
233 | command wire nond_cmd; |
---|
234 | wire nond_reply_stall; |
---|
235 | |
---|
236 | assign reply_owned = 0; |
---|
237 | assign reply_waiting = 0; |
---|
238 | assign abort = REPLY_STALL || |
---|
239 | (CMD == read_shared || CMD == read_owned) && REPLY_WAITING || |
---|
240 | (CMD == read_shared || CMD == read_owned) && REPLY_OWNED; |
---|
241 | |
---|
242 | assign cmd = (master && busy) ? nond_cmd : idle; |
---|
243 | assign reply_stall = (busy && (CMD == read_shared || CMD == read_owned || |
---|
244 | CMD == write_invalid || CMD == write_shared || |
---|
245 | CMD == write_resp_invalid || CMD == write_resp_shared)) ? |
---|
246 | 1 : nond_reply_stall; |
---|
247 | |
---|
248 | assign nond_reply_stall = $ND(0,1); |
---|
249 | assign nond_cmd = $ND(response,idle); |
---|
250 | |
---|
251 | initial busy = 0; |
---|
252 | |
---|
253 | always @(posedge clk) begin |
---|
254 | if (abort) begin busy = busy; end |
---|
255 | else if (master && CMD == response)begin busy = 0; end |
---|
256 | else if (!master && CMD == read_owned || CMD == read_shared)begin busy = 1; end |
---|
257 | end |
---|
258 | |
---|
259 | endmodule |
---|