source: vis_dev/vis-2.1/examples/treearbiter/4-arbit.mv @ 12

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

Add vis
File size: 22.8 KB
Line 
1# /home/sharma/vl2mv/i586/bin/vl2mv 4-arbit.v
2# version: 0.2
3# date:    20:34:06 07/21/96 (CDT)
4.model main
5# I/O ports
6
7.mv constFALSE 2 myTRUE myFALSE
8.mv sa 2 myTRUE myFALSE
9.mv ur1 4 idle request lock release
10.mv xa 2 myTRUE myFALSE
11.mv ur2 4 idle request lock release
12.mv yr 4 idle request lock release
13.mv ur3 4 idle request lock release
14.mv ua1 2 myTRUE myFALSE
15.mv ur4 4 idle request lock release
16.mv ua2 2 myTRUE myFALSE
17.mv sr 4 idle request lock release
18.mv ua3 2 myTRUE myFALSE
19.mv ua4 2 myTRUE myFALSE
20.mv xr 4 idle request lock release
21.mv ya 2 myTRUE myFALSE
22.mv constTRUE 2 myTRUE myFALSE
23# assign constTRUE  = 0
24.mv constTRUE$raw_n0 2 myTRUE myFALSE
25.names constTRUE$raw_n0
26myTRUE
27# assign constFALSE  = 1
28.mv constFALSE$raw_n1 2 myTRUE myFALSE
29.names constFALSE$raw_n1
30myFALSE
31# assign sa  = constFALSE
32.mv sa$raw_n2 2 myTRUE myFALSE
33.names constFALSE sa$raw_n2
34- =constFALSE
35.subckt arbitCell C0 topCell=constTRUE  urLeft=xr  urRight=yr  uaLeft=xa  uaRight=ya  xr=sr  xa=sa 
36.subckt arbitCell C1 topCell=constFALSE  urLeft=ur1  urRight=ur2  uaLeft=ua1  uaRight=ua2  xr=xr  xa=xa 
37.subckt arbitCell C2 topCell=constFALSE  urLeft=ur3  urRight=ur4  uaLeft=ua3  uaRight=ua4  xr=yr  xa=ya 
38.subckt procModel P1 ack=ua1  req=ur1 
39.subckt procModel P2 ack=ua2  req=ur2 
40.subckt procModel P3 ack=ua3  req=ur3 
41.subckt procModel P4 ack=ua4  req=ur4 
42# conflict arbitrators
43.names constFALSE$raw_n1  constFALSE
44- =constFALSE$raw_n1
45.names sa$raw_n2  sa
46- =sa$raw_n2
47.names constTRUE$raw_n0  constTRUE
48- =constTRUE$raw_n0
49# non-blocking assignments
50# latches
51# quasi-continuous assignment
52.end
53
54
55.model arbitCell
56# I/O ports
57.outputs uaLeft
58.inputs topCell
59.inputs xa
60.inputs urRight
61.inputs urLeft
62.outputs xr
63.outputs uaRight
64
65.mv processedLeft 2 myTRUE myFALSE
66.mv prevLeft 2 myTRUE myFALSE
67.mv holdToken 2 myTRUE myFALSE
68.mv processedRight 2 myTRUE myFALSE
69.mv uaLeft 2 myTRUE myFALSE
70.mv topCell 2 myTRUE myFALSE
71.mv xa 2 myTRUE myFALSE
72.mv urRight 4 idle request lock release
73.mv giveChild 2 myTRUE myFALSE
74.mv urLeft 4 idle request lock release
75.mv mustGiveParent 2 myTRUE myFALSE
76.mv xr 4 idle request lock release
77.mv uaRight 2 myTRUE myFALSE
78.mv childOwns 2 myTRUE myFALSE
79.mv prevRight 2 myTRUE myFALSE
80# prevLeft  = 1
81.mv prevLeft$raw_n3 2 myTRUE myFALSE
82.names prevLeft$raw_n3
83myFALSE
84# non-blocking assignments for initial
85# prevRight  = 0
86.mv prevRight$raw_n4 2 myTRUE myFALSE
87.names prevRight$raw_n4
88myTRUE
89# non-blocking assignments for initial
90# processedLeft  = 1
91.mv processedLeft$raw_n5 2 myTRUE myFALSE
92.names processedLeft$raw_n5
93myFALSE
94# non-blocking assignments for initial
95# processedRight  = 1
96.mv processedRight$raw_n6 2 myTRUE myFALSE
97.names processedRight$raw_n6
98myFALSE
99# non-blocking assignments for initial
100# assign mustGiveParent  = (processedLeft  == 0) && (processedRight  == 0) && (!(topCell  == 0)) ? 0 : 1
101.mv mustGiveParent$raw_n7 2 myTRUE myFALSE
102.mv _n9 2 myTRUE myFALSE
103.names _n9
104myTRUE
105# processedLeft  == 0
106.names processedLeft _n9 _n8
107.def 0
108- =processedLeft 1
109.mv _nb 2 myTRUE myFALSE
110.names _nb
111myTRUE
112# processedRight  == 0
113.names processedRight _nb _na
114.def 0
115- =processedRight 1
116# (processedLeft  == 0) && (processedRight  == 0)
117.names _n8 _na _nc
118.def 0
1191 1 1
120.mv _ne 2 myTRUE myFALSE
121.names _ne
122myTRUE
123# topCell  == 0
124.names topCell _ne _nd
125.def 0
126- =topCell 1
127.names _nd _nf
1280 1 
1291 0 
130# (processedLeft  == 0) && (processedRight  == 0) && (!(topCell  == 0))
131.names _nc _nf _n10
132.def 0
1331 1 1
134.mv _n11 2 myTRUE myFALSE
135.names _n11
136myTRUE
137.mv _n12 2 myTRUE myFALSE
138.names _n12
139myFALSE
140# (processedLeft  == 0) && (processedRight  == 0) && (!(topCell  == 0)) ? 0 : 1
141.mv _n13 2 myTRUE myFALSE
142.names _n11 _n12 _n10 _n13
143- - 0 =_n12
144- - 1 =_n11
145.names _n13 mustGiveParent$raw_n7
146- =_n13
147# holdToken  = topCell
148.mv holdToken$raw_n14 2 myTRUE myFALSE
149.names topCell holdToken$raw_n14
150- =topCell
151# non-blocking assignments for initial
152# assign childOwns  = (urLeft  == lock  || urRight  == lock ) ? 0 : 1
153.mv childOwns$raw_n15 2 myTRUE myFALSE
154.mv _n17 4 idle request lock release
155.names _n17
156lock
157# urLeft  == 2
158.names urLeft _n17 _n16
159.def 0
160- =urLeft 1
161.mv _n19 4 idle request lock release
162.names _n19
163lock
164# urRight  == 2
165.names urRight _n19 _n18
166.def 0
167- =urRight 1
168# urLeft  == 2 || urRight  == 2
169.names _n16 _n18 _n1a
170.def 1
1710 0 0
172.mv _n1b 2 myTRUE myFALSE
173.names _n1b
174myTRUE
175.mv _n1c 2 myTRUE myFALSE
176.names _n1c
177myFALSE
178# (urLeft  == 2 || urRight  == 2) ? 0 : 1
179.mv _n1d 2 myTRUE myFALSE
180.names _n1b _n1c _n1a _n1d
181- - 0 =_n1c
182- - 1 =_n1b
183.names _n1d childOwns$raw_n15
184- =_n1d
185# assign giveChild  = (uaLeft  == 0 || uaRight  == 0) ? 0 : 1
186.mv giveChild$raw_n1e 2 myTRUE myFALSE
187.mv _n20 2 myTRUE myFALSE
188.names _n20
189myTRUE
190# uaLeft  == 0
191.names uaLeft _n20 _n1f
192.def 0
193- =uaLeft 1
194.mv _n22 2 myTRUE myFALSE
195.names _n22
196myTRUE
197# uaRight  == 0
198.names uaRight _n22 _n21
199.def 0
200- =uaRight 1
201# uaLeft  == 0 || uaRight  == 0
202.names _n1f _n21 _n23
203.def 1
2040 0 0
205.mv _n24 2 myTRUE myFALSE
206.names _n24
207myTRUE
208.mv _n25 2 myTRUE myFALSE
209.names _n25
210myFALSE
211# (uaLeft  == 0 || uaRight  == 0) ? 0 : 1
212.mv _n26 2 myTRUE myFALSE
213.names _n24 _n25 _n23 _n26
214- - 0 =_n25
215- - 1 =_n24
216.names _n26 giveChild$raw_n1e
217- =_n26
218# assign uaLeft  = (!(mustGiveParent  == 0) && (holdToken  == 0 && urLeft  == request  && (!(urRight  == request ) || prevRight  == 0))) ? 0 : 1
219.mv uaLeft$raw_n27 2 myTRUE myFALSE
220.mv _n29 2 myTRUE myFALSE
221.names _n29
222myTRUE
223# mustGiveParent  == 0
224.names mustGiveParent _n29 _n28
225.def 0
226- =mustGiveParent 1
227.names _n28 _n2a
2280 1 
2291 0 
230.mv _n2c 2 myTRUE myFALSE
231.names _n2c
232myTRUE
233# holdToken  == 0
234.names holdToken _n2c _n2b
235.def 0
236- =holdToken 1
237.mv _n2e 4 idle request lock release
238.names _n2e
239request
240# urLeft  == 1
241.names urLeft _n2e _n2d
242.def 0
243- =urLeft 1
244# holdToken  == 0 && urLeft  == 1
245.names _n2b _n2d _n2f
246.def 0
2471 1 1
248.mv _n31 4 idle request lock release
249.names _n31
250request
251# urRight  == 1
252.names urRight _n31 _n30
253.def 0
254- =urRight 1
255.names _n30 _n32
2560 1 
2571 0 
258.mv _n34 2 myTRUE myFALSE
259.names _n34
260myTRUE
261# prevRight  == 0
262.names prevRight _n34 _n33
263.def 0
264- =prevRight 1
265# !(urRight  == 1) || prevRight  == 0
266.names _n32 _n33 _n35
267.def 1
2680 0 0
269# holdToken  == 0 && urLeft  == 1 && (!(urRight  == 1) || prevRight  == 0)
270.names _n2f _n35 _n36
271.def 0
2721 1 1
273# !(mustGiveParent  == 0) && (holdToken  == 0 && urLeft  == 1 && (!(urRight  == 1) || prevRight  == 0))
274.names _n2a _n36 _n37
275.def 0
2761 1 1
277.mv _n38 2 myTRUE myFALSE
278.names _n38
279myTRUE
280.mv _n39 2 myTRUE myFALSE
281.names _n39
282myFALSE
283# (!(mustGiveParent  == 0) && (holdToken  == 0 && urLeft  == 1 && (!(urRight  == 1) || prevRight  == 0))) ? 0 : 1
284.mv _n3a 2 myTRUE myFALSE
285.names _n38 _n39 _n37 _n3a
286- - 0 =_n39
287- - 1 =_n38
288.names _n3a uaLeft$raw_n27
289- =_n3a
290# assign uaRight  = (!(mustGiveParent  == 0) && (holdToken  == 0 && urRight  == request  && (!(urLeft  == request ) || prevLeft  == 0))) ? 0 : 1
291.mv uaRight$raw_n3b 2 myTRUE myFALSE
292.mv _n3d 2 myTRUE myFALSE
293.names _n3d
294myTRUE
295# mustGiveParent  == 0
296.names mustGiveParent _n3d _n3c
297.def 0
298- =mustGiveParent 1
299.names _n3c _n3e
3000 1 
3011 0 
302.mv _n40 2 myTRUE myFALSE
303.names _n40
304myTRUE
305# holdToken  == 0
306.names holdToken _n40 _n3f
307.def 0
308- =holdToken 1
309.mv _n42 4 idle request lock release
310.names _n42
311request
312# urRight  == 1
313.names urRight _n42 _n41
314.def 0
315- =urRight 1
316# holdToken  == 0 && urRight  == 1
317.names _n3f _n41 _n43
318.def 0
3191 1 1
320.mv _n45 4 idle request lock release
321.names _n45
322request
323# urLeft  == 1
324.names urLeft _n45 _n44
325.def 0
326- =urLeft 1
327.names _n44 _n46
3280 1 
3291 0 
330.mv _n48 2 myTRUE myFALSE
331.names _n48
332myTRUE
333# prevLeft  == 0
334.names prevLeft _n48 _n47
335.def 0
336- =prevLeft 1
337# !(urLeft  == 1) || prevLeft  == 0
338.names _n46 _n47 _n49
339.def 1
3400 0 0
341# holdToken  == 0 && urRight  == 1 && (!(urLeft  == 1) || prevLeft  == 0)
342.names _n43 _n49 _n4a
343.def 0
3441 1 1
345# !(mustGiveParent  == 0) && (holdToken  == 0 && urRight  == 1 && (!(urLeft  == 1) || prevLeft  == 0))
346.names _n3e _n4a _n4b
347.def 0
3481 1 1
349.mv _n4c 2 myTRUE myFALSE
350.names _n4c
351myTRUE
352.mv _n4d 2 myTRUE myFALSE
353.names _n4d
354myFALSE
355# (!(mustGiveParent  == 0) && (holdToken  == 0 && urRight  == 1 && (!(urLeft  == 1) || prevLeft  == 0))) ? 0 : 1
356.mv _n4e 2 myTRUE myFALSE
357.names _n4c _n4d _n4b _n4e
358- - 0 =_n4d
359- - 1 =_n4c
360.names _n4e uaRight$raw_n3b
361- =_n4e
362# assign xr  = (holdToken  == myFALSE  && (urLeft  == 1 || urRight  == 1)) ? 1 : (childOwns  == myTRUE ) ? 2 : (holdToken  == myTRUE  && (((mustGiveParent  == myTRUE ) || !((urLeft  == 1 || urRight  == 1))) && !(topCell  == myTRUE ))) ? 3 : 0
363.mv xr$raw_n4f 4 idle request lock release
364.mv _n51 2 myTRUE myFALSE
365.names _n51
366myFALSE
367# holdToken  == 1
368.names holdToken _n51 _n50
369.def 0
370- =holdToken 1
371.mv _n53 4 idle request lock release
372.names _n53
373request
374# urLeft  == 1
375.names urLeft _n53 _n52
376.def 0
377- =urLeft 1
378.mv _n55 4 idle request lock release
379.names _n55
380request
381# urRight  == 1
382.names urRight _n55 _n54
383.def 0
384- =urRight 1
385# urLeft  == 1 || urRight  == 1
386.names _n52 _n54 _n56
387.def 1
3880 0 0
389# holdToken  == 1 && (urLeft  == 1 || urRight  == 1)
390.names _n50 _n56 _n57
391.def 0
3921 1 1
393.mv _n59 2 myTRUE myFALSE
394.names _n59
395myTRUE
396# childOwns  == 0
397.names childOwns _n59 _n58
398.def 0
399- =childOwns 1
400.mv _n5b 2 myTRUE myFALSE
401.names _n5b
402myTRUE
403# holdToken  == 0
404.names holdToken _n5b _n5a
405.def 0
406- =holdToken 1
407.mv _n5d 2 myTRUE myFALSE
408.names _n5d
409myTRUE
410# mustGiveParent  == 0
411.names mustGiveParent _n5d _n5c
412.def 0
413- =mustGiveParent 1
414.mv _n5f 4 idle request lock release
415.names _n5f
416request
417# urLeft  == 1
418.names urLeft _n5f _n5e
419.def 0
420- =urLeft 1
421.mv _n61 4 idle request lock release
422.names _n61
423request
424# urRight  == 1
425.names urRight _n61 _n60
426.def 0
427- =urRight 1
428# urLeft  == 1 || urRight  == 1
429.names _n5e _n60 _n62
430.def 1
4310 0 0
432.names _n62 _n63
4330 1 
4341 0 
435# (mustGiveParent  == 0) || !((urLeft  == 1 || urRight  == 1))
436.names _n5c _n63 _n64
437.def 1
4380 0 0
439.mv _n66 2 myTRUE myFALSE
440.names _n66
441myTRUE
442# topCell  == 0
443.names topCell _n66 _n65
444.def 0
445- =topCell 1
446.names _n65 _n67
4470 1 
4481 0 
449# ((mustGiveParent  == 0) || !((urLeft  == 1 || urRight  == 1))) && !(topCell  == 0)
450.names _n64 _n67 _n68
451.def 0
4521 1 1
453# holdToken  == 0 && (((mustGiveParent  == 0) || !((urLeft  == 1 || urRight  == 1))) && !(topCell  == 0))
454.names _n5a _n68 _n69
455.def 0
4561 1 1
457.mv _n6a 4 idle request lock release
458.names _n6a
459release
460.mv _n6b 4 idle request lock release
461.names _n6b
462idle
463# (holdToken  == 0 && (((mustGiveParent  == 0) || !((urLeft  == 1 || urRight  == 1))) && !(topCell  == 0))) ? 3 : 0
464.mv _n6c 4 idle request lock release
465.names _n6a _n6b _n69 _n6c
466- - 0 =_n6b
467- - 1 =_n6a
468.mv _n6d 4 idle request lock release
469.names _n6d
470lock
471# (childOwns  == 0) ? 2 : (holdToken  == 0 && (((mustGiveParent  == 0) || !((urLeft  == 1 || urRight  == 1))) && !(topCell  == 0))) ? 3 : 0
472.mv _n6e 4 idle request lock release
473.names _n6d _n6c _n58 _n6e
474- - 0 =_n6c
475- - 1 =_n6d
476.mv _n6f 4 idle request lock release
477.names _n6f
478request
479# (holdToken  == 1 && (urLeft  == 1 || urRight  == 1)) ? 1 : (childOwns  == 0) ? 2 : (holdToken  == 0 && (((mustGiveParent  == 0) || !((urLeft  == 1 || urRight  == 1))) && !(topCell  == 0))) ? 3 : 0
480.mv _n70 4 idle request lock release
481.names _n6f _n6e _n57 _n70
482- - 0 =_n6e
483- - 1 =_n6f
484.names _n70 xr$raw_n4f
485- =_n70
486.mv _n72 2 myTRUE myFALSE
487.names _n72
488myTRUE
489# xa  == 0
490.names xa _n72 _n71
491.def 0
492- =xa 1
493.names _n71 _n73
494- =_n71
495# holdToken  = 0
496.mv holdToken$_n71_n74$true 2 myTRUE myFALSE
497.names holdToken$_n71_n74$true
498myTRUE
499.mv _n76 2 myTRUE myFALSE
500.names _n76
501myTRUE
502# giveChild  == 0
503.names giveChild _n76 _n75
504.def 0
505- =giveChild 1
506.names _n75 _n77
507- =_n75
508# holdToken  = 1
509.mv holdToken$_n75_n78$true 2 myTRUE myFALSE
510.names holdToken$_n75_n78$true
511myFALSE
512.mv _n7a 4 idle request lock release
513.names _n7a
514release
515# urLeft  == 3
516.names urLeft _n7a _n79
517.def 0
518- =urLeft 1
519.mv _n7c 4 idle request lock release
520.names _n7c
521release
522# urRight  == 3
523.names urRight _n7c _n7b
524.def 0
525- =urRight 1
526# urLeft  == 3 || urRight  == 3
527.names _n79 _n7b _n7d
528.def 1
5290 0 0
530.names _n7d _n7e
531- =_n7d
532# holdToken  = 0
533.mv holdToken$_n7d_n7f$true 2 myTRUE myFALSE
534.names holdToken$_n7d_n7f$true
535myTRUE
536.mv _n81 4 idle request lock release
537.names _n81
538release
539# xr  == 3
540.names xr _n81 _n80
541.def 0
542- =xr 1
543.names _n80 _n82
544- =_n80
545# holdToken  = 1
546.mv holdToken$_n80_n83$true 2 myTRUE myFALSE
547.names holdToken$_n80_n83$true
548myFALSE
549# if/else (xr  == 3)
550.mv holdToken$_n80$raw_n86 2 myTRUE myFALSE
551.names holdToken$_n80_n83$true holdToken _n80 holdToken$_n80$raw_n86
552- - 0 =holdToken
553- - 1 =holdToken$_n80_n83$true
554# if/else (urLeft  == 3 || urRight  == 3)
555.mv holdToken$_n7d$raw_n88 2 myTRUE myFALSE
556.names holdToken$_n7d_n7f$true holdToken$_n80$raw_n86 _n7d holdToken$_n7d$raw_n88
557- - 0 =holdToken$_n80$raw_n86
558- - 1 =holdToken$_n7d_n7f$true
559# if/else (giveChild  == 0)
560.mv holdToken$_n75$raw_n8c 2 myTRUE myFALSE
561.names holdToken$_n75_n78$true holdToken$_n7d$raw_n88 _n75 holdToken$_n75$raw_n8c
562- - 0 =holdToken$_n7d$raw_n88
563- - 1 =holdToken$_n75_n78$true
564# if/else (xa  == 0)
565.mv holdToken$_n71$raw_n90 2 myTRUE myFALSE
566.names holdToken$_n71_n74$true holdToken$_n75$raw_n8c _n71 holdToken$_n71$raw_n90
567- - 0 =holdToken$_n75$raw_n8c
568- - 1 =holdToken$_n71_n74$true
569.mv _n94 2 myTRUE myFALSE
570.names _n94
571myTRUE
572# uaLeft  == 0
573.names uaLeft _n94 _n93
574.def 0
575- =uaLeft 1
576.names _n93 _n95
577- =_n93
578# prevLeft  = 0
579.mv prevLeft$_n93_n96$true 2 myTRUE myFALSE
580.names prevLeft$_n93_n96$true
581myTRUE
582# prevRight  = 1
583.mv prevRight$_n93_n97$true 2 myTRUE myFALSE
584.names prevRight$_n93_n97$true
585myFALSE
586.mv _n99 2 myTRUE myFALSE
587.names _n99
588myTRUE
589# uaRight  == 0
590.names uaRight _n99 _n98
591.def 0
592- =uaRight 1
593.names _n98 _n9a
594- =_n98
595# prevLeft  = 1
596.mv prevLeft$_n98_n9b$true 2 myTRUE myFALSE
597.names prevLeft$_n98_n9b$true
598myFALSE
599# prevRight  = 0
600.mv prevRight$_n98_n9c$true 2 myTRUE myFALSE
601.names prevRight$_n98_n9c$true
602myTRUE
603# if/else (uaRight  == 0)
604.mv prevLeft$_n98$raw_na3 2 myTRUE myFALSE
605.names prevLeft$_n98_n9b$true prevLeft _n98 prevLeft$_n98$raw_na3
606- - 0 =prevLeft
607- - 1 =prevLeft$_n98_n9b$true
608.mv prevRight$_n98$raw_na5 2 myTRUE myFALSE
609.names prevRight$_n98_n9c$true prevRight _n98 prevRight$_n98$raw_na5
610- - 0 =prevRight
611- - 1 =prevRight$_n98_n9c$true
612# if/else (uaLeft  == 0)
613.mv prevLeft$_n93$raw_naa 2 myTRUE myFALSE
614.names prevLeft$_n93_n96$true prevLeft$_n98$raw_na3 _n93 prevLeft$_n93$raw_naa
615- - 0 =prevLeft$_n98$raw_na3
616- - 1 =prevLeft$_n93_n96$true
617.mv prevRight$_n93$raw_nac 2 myTRUE myFALSE
618.names prevRight$_n93_n97$true prevRight$_n98$raw_na5 _n93 prevRight$_n93$raw_nac
619- - 0 =prevRight$_n98$raw_na5
620- - 1 =prevRight$_n93_n97$true
621.mv _nb4 4 idle request lock release
622.names _nb4
623release
624# urLeft  == 3
625.names urLeft _nb4 _nb3
626.def 0
627- =urLeft 1
628.names _nb3 _nb5
629- =_nb3
630# processedLeft  = 0
631.mv processedLeft$_nb3_nb6$true 2 myTRUE myFALSE
632.names processedLeft$_nb3_nb6$true
633myTRUE
634.mv _nb8 4 idle request lock release
635.names _nb8
636release
637# urRight  == 3
638.names urRight _nb8 _nb7
639.def 0
640- =urRight 1
641.names _nb7 _nb9
642- =_nb7
643# processedRight  = 0
644.mv processedRight$_nb7_nba$true 2 myTRUE myFALSE
645.names processedRight$_nb7_nba$true
646myTRUE
647.mv _nbc 2 myTRUE myFALSE
648.names _nbc
649myTRUE
650# processedLeft  == 0
651.names processedLeft _nbc _nbb
652.def 0
653- =processedLeft 1
654.mv _nbe 2 myTRUE myFALSE
655.names _nbe
656myTRUE
657# processedRight  == 0
658.names processedRight _nbe _nbd
659.def 0
660- =processedRight 1
661# (processedLeft  == 0) && (processedRight  == 0)
662.names _nbb _nbd _nbf
663.def 0
6641 1 1
665.names _nbf _nc0
666- =_nbf
667# processedLeft  = 1
668.mv processedLeft$_nbf_nc1$true 2 myTRUE myFALSE
669.names processedLeft$_nbf_nc1$true
670myFALSE
671# processedRight  = 1
672.mv processedRight$_nbf_nc2$true 2 myTRUE myFALSE
673.names processedRight$_nbf_nc2$true
674myFALSE
675# if/else ((processedLeft  == 0) && (processedRight  == 0))
676.mv processedLeft$_nbf$raw_ncd 2 myTRUE myFALSE
677.names processedLeft$_nbf_nc1$true processedLeft _nbf processedLeft$_nbf$raw_ncd
678- - 0 =processedLeft
679- - 1 =processedLeft$_nbf_nc1$true
680.mv processedRight$_nbf$raw_ncf 2 myTRUE myFALSE
681.names processedRight$_nbf_nc2$true processedRight _nbf processedRight$_nbf$raw_ncf
682- - 0 =processedRight
683- - 1 =processedRight$_nbf_nc2$true
684# if/else (urRight  == 3)
685.mv processedRight$_nb7$raw_nda 2 myTRUE myFALSE
686.names processedRight$_nb7_nba$true processedRight$_nbf$raw_ncf _nb7 processedRight$_nb7$raw_nda
687- - 0 =processedRight$_nbf$raw_ncf
688- - 1 =processedRight$_nb7_nba$true
689.mv processedLeft$_nb7$raw_ne1 2 myTRUE myFALSE
690.names processedLeft processedLeft$_nbf$raw_ncd _nb7 processedLeft$_nb7$raw_ne1
691- - 0 =processedLeft$_nbf$raw_ncd
692- - 1 =processedLeft
693# if/else (urLeft  == 3)
694.mv processedLeft$_nb3$raw_nea 2 myTRUE myFALSE
695.names processedLeft$_nb3_nb6$true processedLeft$_nb7$raw_ne1 _nb3 processedLeft$_nb3$raw_nea
696- - 0 =processedLeft$_nb7$raw_ne1
697- - 1 =processedLeft$_nb3_nb6$true
698.mv processedRight$_nb3$raw_nf4 2 myTRUE myFALSE
699.names processedRight processedRight$_nb7$raw_nda _nb3 processedRight$_nb3$raw_nf4
700- - 0 =processedRight$_nb7$raw_nda
701- - 1 =processedRight
702# conflict arbitrators
703.names _nb5 _nb9 _nc0 _nf7
704.def 0
705 1 - - 1
706 0 0 1 1
707.mv _nf8 2 myTRUE myFALSE
708.names _nf7 processedLeft$_nb3$raw_nea processedLeft _nf8
7091 - - =processedLeft$_nb3$raw_nea
7100 - - =processedLeft
711.names _n95 _n9a _n105
712.def 0
713 1 - 1
714 0 1 1
715.mv _n106 2 myTRUE myFALSE
716.names _n105 prevLeft$_n93$raw_naa prevLeft _n106
7171 - - =prevLeft$_n93$raw_naa
7180 - - =prevLeft
719.names _n73 _n77 _n7e _n82 _n113
720.def 0
721 1 - - - 1
722 0 1 - - 1
723 0 0 1 - 1
724 0 0 0 1 1
725.mv _n114 2 myTRUE myFALSE
726.names _n113 holdToken$_n71$raw_n90 holdToken _n114
7271 - - =holdToken$_n71$raw_n90
7280 - - =holdToken
729.names _nb5 _nb9 _nc0 _n121
730.def 0
731 0 1 - 1
732 0 0 1 1
733.mv _n122 2 myTRUE myFALSE
734.names _n121 processedRight$_nb3$raw_nf4 processedRight _n122
7351 - - =processedRight$_nb3$raw_nf4
7360 - - =processedRight
737.names uaLeft$raw_n27  uaLeft
738- =uaLeft$raw_n27
739.names giveChild$raw_n1e  giveChild
740- =giveChild$raw_n1e
741.names mustGiveParent$raw_n7  mustGiveParent
742- =mustGiveParent$raw_n7
743.names xr$raw_n4f  xr
744- =xr$raw_n4f
745.names uaRight$raw_n3b  uaRight
746- =uaRight$raw_n3b
747.names childOwns$raw_n15  childOwns
748- =childOwns$raw_n15
749.names _n95 _n9a _n12f
750.def 0
751 1 - 1
752 0 1 1
753.mv _n130 2 myTRUE myFALSE
754.names _n12f prevRight$_n93$raw_nac prevRight _n130
7551 - - =prevRight$_n93$raw_nac
7560 - - =prevRight
757# non-blocking assignments
758# latches
759.r prevLeft$raw_n3 prevLeft
760- =prevLeft$raw_n3
761.latch _n106 prevLeft
762.r processedLeft$raw_n5 processedLeft
763- =processedLeft$raw_n5
764.latch _nf8 processedLeft
765.r processedRight$raw_n6 processedRight
766- =processedRight$raw_n6
767.latch _n122 processedRight
768.r holdToken$raw_n14 holdToken
769- =holdToken$raw_n14
770.latch _n114 holdToken
771.r prevRight$raw_n4 prevRight
772- =prevRight$raw_n4
773.latch _n130 prevRight
774# quasi-continuous assignment
775.end
776
777
778.model procModel
779# I/O ports
780.outputs req
781.inputs ack
782
783.mv req 4 idle request lock release
784.mv procState 4 idle request lock release
785.mv ack 2 myTRUE myFALSE
786# assign req  = procState
787.mv req$raw_n13d 4 idle request lock release
788.names procState req$raw_n13d
789- =procState
790# procState  = 0
791.mv procState$raw_n13e 4 idle request lock release
792.names procState$raw_n13e
793idle
794# non-blocking assignments for initial
795# assign randChoice  = $NDset ( 0,1,2,3,4,5,6,7 )
796.names -> randChoice<0> randChoice<1> randChoice<2>
7970 0 0
7981 0 0
7990 1 0
8001 1 0
8010 0 1
8021 0 1
8030 1 1
8041 1 1
805.mv _n142 4 idle request lock release
806.names _n142
807idle
808# procState  == 0
809.names procState _n142 _n141
810.def 0
811- =procState 1
812.names _n144<0>
8131
814.names _n144<1>
8151
816.names _n144<2>
8171
818# randChoice  == 7
819.names randChoice<0> _n144<0> _n145<0>
820.def 0
8210 1 1
8221 0 1
823.names randChoice<1> _n144<1> _n145<1>
824.def 0
8250 1 1
8261 0 1
827.names randChoice<2> _n144<2> _n145<2>
828.def 0
8290 1 1
8301 0 1
831.names _n145<0> _n145<1> _n145<2> _n146
832.def 1
8330 0 0 0
834.names _n146 _n143
8350 1 
8361 0 
837# procState  == 0 && (randChoice  == 7)
838.names _n141 _n143 _n147
839.def 0
8401 1 1
841.names _n147 _n148
842- =_n147
843# procState  = 1
844.mv procState$_n147_n149$true 4 idle request lock release
845.names procState$_n147_n149$true
846request
847.mv _n14b 4 idle request lock release
848.names _n14b
849request
850# procState  == 1
851.names procState _n14b _n14a
852.def 0
853- =procState 1
854.mv _n14d 2 myTRUE myFALSE
855.names _n14d
856myTRUE
857# ack  == 0
858.names ack _n14d _n14c
859.def 0
860- =ack 1
861# procState  == 1 && ack  == 0
862.names _n14a _n14c _n14e
863.def 0
8641 1 1
865.names _n14e _n14f
866- =_n14e
867# procState  = 2
868.mv procState$_n14e_n150$true 4 idle request lock release
869.names procState$_n14e_n150$true
870lock
871.mv _n152 4 idle request lock release
872.names _n152
873lock
874# procState  == 2
875.names procState _n152 _n151
876.def 0
877- =procState 1
878.names _n153<0>
8791
880.names _n153<1>
8811
882.names _n153<2>
8830
884# randChoice  > 3
885.names _n156
8860
887.names randChoice<0> _n153<0> _n156 _n155<0>
888.def 0
8890 0 1 1
8900 1 0 1
8911 0 0 1
8921 1 1 1
893# carry/borrow
894.names _n158
8950
896.names randChoice<0> _n153<0> _n158 _n157
897.def 0
8980 0 1 1
8990 1 0 1
9000 1 1 1
9011 1 1 1
902.names randChoice<1> _n153<1> _n157 _n155<1>
903.def 0
9040 0 1 1
9050 1 0 1
9061 0 0 1
9071 1 1 1
908# carry/borrow
909.names randChoice<1> _n153<1> _n157 _n159
910.def 0
9110 0 1 1
9120 1 0 1
9130 1 1 1
9141 1 1 1
915.names randChoice<2> _n153<2> _n159 _n155<2>
916.def 0
9170 0 1 1
9180 1 0 1
9191 0 0 1
9201 1 1 1
921# carry/borrow
922.names randChoice<2> _n153<2> _n159 _n15a
923.def 0
9240 0 1 1
9250 1 0 1
9260 1 1 1
9271 1 1 1
928.names _n155<0> _n155<1> _n155<2> _n15b
929.def 0
9300 0 0 1
931.names _n15a _n15b _n15c
932.def 1
9330 0 0
934.names _n15c _n154
9350 1 
9361 0 
937# procState  == 2 && (randChoice  > 3)
938.names _n151 _n154 _n15d
939.def 0
9401 1 1
941.names _n15d _n15e
942- =_n15d
943# procState  = 3
944.mv procState$_n15d_n15f$true 4 idle request lock release
945.names procState$_n15d_n15f$true
946release
947.mv _n161 4 idle request lock release
948.names _n161
949release
950# procState  == 3
951.names procState _n161 _n160
952.def 0
953- =procState 1
954.names _n160 _n162
955- =_n160
956# procState  = 0
957.mv procState$_n160_n163$true 4 idle request lock release
958.names procState$_n160_n163$true
959idle
960# if/else (procState  == 3)
961.mv procState$_n160$raw_n166 4 idle request lock release
962.names procState$_n160_n163$true procState _n160 procState$_n160$raw_n166
963- - 0 =procState
964- - 1 =procState$_n160_n163$true
965# if/else (procState  == 2 && (randChoice  > 3))
966.mv procState$_n15d$raw_n168 4 idle request lock release
967.names procState$_n15d_n15f$true procState$_n160$raw_n166 _n15d procState$_n15d$raw_n168
968- - 0 =procState$_n160$raw_n166
969- - 1 =procState$_n15d_n15f$true
970# if/else (procState  == 1 && ack  == 0)
971.mv procState$_n14e$raw_n16c 4 idle request lock release
972.names procState$_n14e_n150$true procState$_n15d$raw_n168 _n14e procState$_n14e$raw_n16c
973- - 0 =procState$_n15d$raw_n168
974- - 1 =procState$_n14e_n150$true
975# if/else (procState  == 0 && (randChoice  == 7))
976.mv procState$_n147$raw_n170 4 idle request lock release
977.names procState$_n147_n149$true procState$_n14e$raw_n16c _n147 procState$_n147$raw_n170
978- - 0 =procState$_n14e$raw_n16c
979- - 1 =procState$_n147_n149$true
980# conflict arbitrators
981.names req$raw_n13d  req
982- =req$raw_n13d
983.names _n148 _n14f _n15e _n162 _n173
984.def 0
985 1 - - - 1
986 0 1 - - 1
987 0 0 1 - 1
988 0 0 0 1 1
989.mv _n174 4 idle request lock release
990.names _n173 procState$_n147$raw_n170 procState _n174
9911 - - =procState$_n147$raw_n170
9920 - - =procState
993# non-blocking assignments
994# latches
995.r procState$raw_n13e procState
996- =procState$raw_n13e
997.latch _n174 procState
998# quasi-continuous assignment
999.end
1000
1001
Note: See TracBrowser for help on using the repository browser.