source: vis_dev/vis-2.1/examples/gigamax/gigamax.v @ 12

Last change on this file since 12 was 11, checked in by cecile, 13 years ago

Add vis

File size: 7.9 KB
Line 
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
14typedef enum { idle, read_shared, read_owned, write_invalid, write_shared, 
15               write_resp_invalid, write_resp_shared, invalidate, response } 
16        command;
17typedef enum { invalid, shared, owned } status;
18typedef enum {r0,r1,r2,r3,r4,r5,r6,r7,r8} nine;
19
20
21module main (clk);
22
23input clk;
24
25command wire CMD;
26wire REPLY_OWNED, REPLY_WAITING, REPLY_STALL;
27command wire p0_cmd, p1_cmd, p2_cmd, m_cmd;
28wire 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;
32command wire nond_CMD;
33wire nond0_master;
34wire nond1_master;
35wire nond2_master;
36wire nondm_master;
37
38processor p0(clk, CMD, p0_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL,
39             p0_cmd, p0_reply_owned, p0_reply_waiting, p0_reply_stall);
40processor p1(clk, CMD, p1_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL,
41             p1_cmd, p1_reply_owned, p1_reply_waiting, p1_reply_stall);
42processor p2(clk, CMD, p2_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL,
43             p2_cmd, p2_reply_owned, p2_reply_waiting, p2_reply_stall);
44memory m(clk, CMD, m_master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL,
45         m_cmd, m_reply_owned, m_reply_waiting, m_reply_stall);
46
47assign 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
52assign 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
57assign p0_master = nond0_master;
58assign p1_master = (p0_master) ? 0 : nond1_master;
59assign p2_master = (p0_master || p1_master) ? 0 : nond2_master;
60assign m_master  = ( (p0_master || p1_master) || p2_master) ? 0 : nondm_master;
61
62assign nond0_master = $ND(0,1);
63assign nond1_master = $ND(0,1);
64assign nond2_master = $ND(0,1);
65assign nondm_master = $ND(0,1);
66
67assign nond_CMD = $ND(idle, read_shared, read_owned, write_invalid, 
68                      write_shared, write_resp_invalid, write_resp_shared, invalidate, response);
69
70endmodule
71
72
73
74module cache_device (clk, CMD, master, abort, waiting, state,snoop, reply_owned,
75                     readable, writable);
76input clk;
77input CMD;
78input master;
79input abort;
80input waiting;
81output state;
82output snoop;
83output reply_owned;
84output readable, writable;
85
86command wire CMD;
87wire master;
88wire abort;
89wire waiting;
90status reg state, snoop;
91wire readable, writable, reply_owned;
92
93status wire nond_snoop;
94status wire nond_state;
95
96assign readable = ((state == shared) || (state == owned)) && !waiting;
97assign writable = (state == owned) && (!waiting);
98assign reply_owned = (!master) && (state == owned);
99assign nond_snoop = $ND(shared,owned);
100assign nond_state = $ND(shared,invalid);
101
102initial begin state = invalid; end
103initial begin snoop = invalid; end
104
105always @(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
133end
134
135endmodule
136
137
138
139module bus_device(clk, CMD, master, REPLY_STALL, REPLY_WAITING, 
140                  waiting, reply_waiting, abort);
141input clk;
142input CMD;
143input master;
144input REPLY_STALL;
145input REPLY_WAITING;
146output waiting;
147output reply_waiting;
148output abort;
149
150command wire CMD;
151wire master;
152wire REPLY_STALL, REPLY_WAITING;
153reg waiting;
154wire reply_waiting;
155wire abort;
156
157wire reply_waiting, abort;
158
159assign reply_waiting = !master && waiting;
160assign abort = REPLY_STALL || 
161               ((CMD == read_shared || CMD == read_owned) && REPLY_WAITING);
162
163initial waiting = 0;
164always @(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
171end
172
173endmodule
174
175
176
177module processor(clk, CMD, master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL,
178                 cmd, reply_owned, reply_waiting, reply_stall);
179input clk;
180input CMD;
181input master;
182input REPLY_OWNED, REPLY_WAITING, REPLY_STALL;
183output cmd;
184output reply_owned;
185output reply_waiting;
186output reply_stall;
187
188command wire CMD;
189wire master;
190wire REPLY_OWNED, REPLY_WAITING, REPLY_STALL;
191command wire cmd;
192wire reply_owned, reply_waiting, reply_stall;
193
194command wire nond_cmd;
195wire abort, waiting;
196status wire state, snoop;
197wire readable, writable;
198
199bus_device Bdevice(clk, CMD, master, REPLY_STALL, REPLY_WAITING,
200                   waiting, reply_waiting, abort);
201cache_device Cdevice(clk, CMD, master, abort, waiting, state,snoop, reply_owned, 
202                     readable, writable);
203
204assign 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
210assign nond_cmd = $ND(read_shared,read_owned);
211assign reply_stall = $ND(0,1);
212endmodule
213
214
215
216module memory (clk, CMD, master, REPLY_OWNED, REPLY_WAITING, REPLY_STALL,
217               cmd, reply_owned, reply_waiting, reply_stall);
218input clk;
219input CMD;
220input master;
221input REPLY_OWNED, REPLY_WAITING, REPLY_STALL;
222output cmd;
223output reply_owned, reply_waiting, reply_stall;
224
225command wire CMD;
226wire master;
227wire REPLY_OWNED, REPLY_WAITING, REPLY_STALL;
228command wire cmd;
229wire reply_owned, reply_waiting, reply_stall;
230
231wire abort;
232reg busy;
233command wire nond_cmd;
234wire nond_reply_stall;
235
236assign reply_owned = 0;
237assign reply_waiting = 0;
238assign abort = REPLY_STALL || 
239               (CMD == read_shared || CMD == read_owned) && REPLY_WAITING || 
240               (CMD == read_shared || CMD == read_owned) && REPLY_OWNED;
241
242assign cmd = (master && busy) ? nond_cmd : idle;
243assign 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
248assign nond_reply_stall = $ND(0,1);
249assign nond_cmd = $ND(response,idle);
250
251initial busy = 0;
252
253always @(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
257end
258
259endmodule
Note: See TracBrowser for help on using the repository browser.