1(* -*-sml-*- *)
2(*****************************************************************************)
3(* Example from FoCs Manual                                                  *)
4(* Not for compiling.                                                        *)
5(*****************************************************************************)
6
7loadPath := "../official-semantics" :: "../regexp" :: !loadPath;
8app load ["bossLib","intLib","regexpLib","ExecuteTools"];
9
10quietdec := true;
11open bossLib regexpLib;
12quietdec := false;
13
14(******************************************************************************
15* Set the trace level of the regular expression library:
16* 0: silent
17* 1: 1 character (either - or +) for each list element processed
18* 2: matches as they are discovered
19* 3: transitions as they are calculated
20* 4: internal state of the automata
21******************************************************************************)
22set_trace "regexpTools" 1;
23
24(******************************************************************************
25* Set default parsing to natural numbers rather than integers
26******************************************************************************)
27val _ = intLib.deprecate_int();
28
29(******************************************************************************
30* Generated this from a Verilog model of the BUF example in
31* Chapter 4 of FoCs User's Manual (see test.v)
32* (www.haifa.il.ibm.com/projects/verification/focs/)
33******************************************************************************)
34
35(******************************************************************************
36* String version
37* val StoB_REQ = ``"StoB_REQ"``;
38* val BtoS_ACK = ``"BtoS_ACK"``;
39* val BtoR_REQ = ``"BtoR_REQ"``;
40* val RtoB_ACK = ``"RtoB_ACK"``;
41******************************************************************************)
42
43(******************************************************************************
44* Num version
45******************************************************************************)
46val StoB_REQ_def = Define `StoB_REQ = 0`;
47val BtoS_ACK_def = Define `BtoS_ACK = 1`;
48val BtoR_REQ_def = Define `BtoR_REQ = 2`;
49val RtoB_ACK_def = Define `RtoB_ACK = 3`;
50
51quietdec := true;
52val SimRun_def =
53 Define
54  `SimRun =
55      [{};
56       {StoB_REQ};
57       {StoB_REQ; BtoS_ACK};
58       {BtoS_ACK};
59       {BtoS_ACK; BtoR_REQ};
60       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
61       {BtoS_ACK; RtoB_ACK};
62       {};
63       {StoB_REQ};
64       {StoB_REQ; BtoS_ACK};
65       {BtoS_ACK};
66       {BtoS_ACK; BtoR_REQ};
67       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
68       {BtoS_ACK; RtoB_ACK};
69       {};
70       {StoB_REQ};
71       {StoB_REQ; BtoS_ACK};
72       {BtoS_ACK};
73       {BtoS_ACK; BtoR_REQ};
74       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
75       {BtoS_ACK; RtoB_ACK};
76       {};
77       {StoB_REQ};
78       {StoB_REQ; BtoS_ACK};
79       {BtoS_ACK};
80       {BtoS_ACK; BtoR_REQ};
81       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
82       {BtoS_ACK; RtoB_ACK};
83       {};
84       {StoB_REQ};
85       {StoB_REQ; BtoS_ACK};
86       {BtoS_ACK};
87       {BtoS_ACK; BtoR_REQ};
88       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
89       {BtoS_ACK; RtoB_ACK};
90       {};
91       {StoB_REQ};
92       {StoB_REQ; BtoS_ACK};
93       {BtoS_ACK};
94       {BtoS_ACK; BtoR_REQ};
95       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
96       {BtoS_ACK; RtoB_ACK};
97       {};
98       {StoB_REQ};
99       {StoB_REQ; BtoS_ACK};
100       {BtoS_ACK};
101       {BtoS_ACK; BtoR_REQ};
102       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
103       {BtoS_ACK; RtoB_ACK};
104       {};
105       {StoB_REQ};
106       {StoB_REQ; BtoS_ACK};
107       {BtoS_ACK};
108       {BtoS_ACK; BtoR_REQ};
109       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
110       {BtoS_ACK; RtoB_ACK};
111       {};
112       {StoB_REQ};
113       {StoB_REQ; BtoS_ACK};
114       {BtoS_ACK};
115       {BtoS_ACK; BtoR_REQ};
116       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
117       {BtoS_ACK; RtoB_ACK};
118       {};
119       {StoB_REQ};
120       {StoB_REQ; BtoS_ACK};
121       {BtoS_ACK};
122       {BtoS_ACK; BtoR_REQ};
123       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
124       {BtoS_ACK; RtoB_ACK};
125       {};
126       {StoB_REQ};
127       {StoB_REQ; BtoS_ACK};
128       {BtoS_ACK};
129       {BtoS_ACK; BtoR_REQ};
130       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
131       {BtoS_ACK; RtoB_ACK};
132       {};
133       {StoB_REQ};
134       {StoB_REQ; BtoS_ACK};
135       {BtoS_ACK};
136       {BtoS_ACK; BtoR_REQ};
137       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
138       {BtoS_ACK; RtoB_ACK};
139       {};
140       {StoB_REQ};
141       {StoB_REQ; BtoS_ACK};
142       {BtoS_ACK};
143       {BtoS_ACK; BtoR_REQ};
144       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
145       {BtoS_ACK; RtoB_ACK};
146       {};
147       {StoB_REQ};
148       {StoB_REQ; BtoS_ACK};
149       {BtoS_ACK};
150       {BtoS_ACK; BtoR_REQ};
151       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
152       {BtoS_ACK; RtoB_ACK};
153       {};
154       {StoB_REQ};
155       {StoB_REQ; BtoS_ACK};
156       {BtoS_ACK};
157       {BtoS_ACK; BtoR_REQ};
158       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
159       {BtoS_ACK; RtoB_ACK};
160       {};
161       {StoB_REQ};
162       {StoB_REQ; BtoS_ACK};
163       {BtoS_ACK};
164       {BtoS_ACK; BtoR_REQ};
165       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
166       {BtoS_ACK; RtoB_ACK};
167       {};
168       {StoB_REQ};
169       {StoB_REQ; BtoS_ACK};
170       {BtoS_ACK};
171       {BtoS_ACK; BtoR_REQ};
172       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
173       {BtoS_ACK; RtoB_ACK};
174       {};
175       {StoB_REQ};
176       {StoB_REQ; BtoS_ACK};
177       {BtoS_ACK};
178       {BtoS_ACK; BtoR_REQ};
179       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
180       {BtoS_ACK; RtoB_ACK};
181       {};
182       {StoB_REQ};
183       {StoB_REQ; BtoS_ACK};
184       {BtoS_ACK};
185       {BtoS_ACK; BtoR_REQ};
186       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
187       {BtoS_ACK; RtoB_ACK};
188       {};
189       {StoB_REQ};
190       {StoB_REQ; BtoS_ACK};
191       {BtoS_ACK};
192       {BtoS_ACK; BtoR_REQ};
193       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
194       {BtoS_ACK; RtoB_ACK};
195       {};
196       {StoB_REQ};
197       {StoB_REQ; BtoS_ACK};
198       {BtoS_ACK};
199       {BtoS_ACK; BtoR_REQ};
200       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
201       {BtoS_ACK; RtoB_ACK};
202       {};
203       {StoB_REQ};
204       {StoB_REQ; BtoS_ACK};
205       {BtoS_ACK};
206       {BtoS_ACK; BtoR_REQ};
207       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
208       {BtoS_ACK; RtoB_ACK};
209       {};
210       {StoB_REQ};
211       {StoB_REQ; BtoS_ACK};
212       {BtoS_ACK};
213       {BtoS_ACK; BtoR_REQ};
214       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
215       {BtoS_ACK; RtoB_ACK};
216       {};
217       {StoB_REQ};
218       {StoB_REQ; BtoS_ACK};
219       {BtoS_ACK};
220       {BtoS_ACK; BtoR_REQ};
221       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
222       {BtoS_ACK; RtoB_ACK};
223       {};
224       {StoB_REQ};
225       {StoB_REQ; BtoS_ACK};
226       {BtoS_ACK};
227       {BtoS_ACK; BtoR_REQ};
228       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
229       {BtoS_ACK; RtoB_ACK};
230       {};
231       {StoB_REQ};
232       {StoB_REQ; BtoS_ACK};
233       {BtoS_ACK};
234       {BtoS_ACK; BtoR_REQ};
235       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
236       {BtoS_ACK; RtoB_ACK};
237       {};
238       {StoB_REQ};
239       {StoB_REQ; BtoS_ACK};
240       {BtoS_ACK};
241       {BtoS_ACK; BtoR_REQ};
242       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
243       {BtoS_ACK; RtoB_ACK};
244       {};
245       {StoB_REQ};
246       {StoB_REQ; BtoS_ACK};
247       {BtoS_ACK};
248       {BtoS_ACK; BtoR_REQ};
249       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
250       {BtoS_ACK; RtoB_ACK};
251       {};
252       {StoB_REQ};
253       {StoB_REQ; BtoS_ACK};
254       {BtoS_ACK};
255       {BtoS_ACK; BtoR_REQ};
256       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
257       {BtoS_ACK; RtoB_ACK};
258       {};
259       {StoB_REQ};
260       {StoB_REQ; BtoS_ACK};
261       {BtoS_ACK};
262       {BtoS_ACK; BtoR_REQ};
263       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
264       {BtoS_ACK; RtoB_ACK};
265       {};
266       {StoB_REQ};
267       {StoB_REQ; BtoS_ACK};
268       {BtoS_ACK};
269       {BtoS_ACK; BtoR_REQ};
270       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
271       {BtoS_ACK; RtoB_ACK};
272       {};
273       {StoB_REQ};
274       {StoB_REQ; BtoS_ACK};
275       {BtoS_ACK};
276       {BtoS_ACK; BtoR_REQ};
277       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
278       {BtoS_ACK; RtoB_ACK};
279       {};
280       {StoB_REQ};
281       {StoB_REQ; BtoS_ACK};
282       {BtoS_ACK};
283       {BtoS_ACK; BtoR_REQ};
284       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
285       {BtoS_ACK; RtoB_ACK};
286       {};
287       {StoB_REQ};
288       {StoB_REQ; BtoS_ACK};
289       {BtoS_ACK};
290       {BtoS_ACK; BtoR_REQ};
291       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
292       {BtoS_ACK; RtoB_ACK};
293       {};
294       {StoB_REQ};
295       {StoB_REQ; BtoS_ACK};
296       {BtoS_ACK};
297       {BtoS_ACK; BtoR_REQ};
298       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
299       {BtoS_ACK; RtoB_ACK};
300       {};
301       {StoB_REQ};
302       {StoB_REQ; BtoS_ACK};
303       {BtoS_ACK};
304       {BtoS_ACK; BtoR_REQ};
305       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
306       {BtoS_ACK; RtoB_ACK};
307       {};
308       {StoB_REQ};
309       {StoB_REQ; BtoS_ACK};
310       {BtoS_ACK};
311       {BtoS_ACK; BtoR_REQ};
312       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
313       {BtoS_ACK; RtoB_ACK};
314       {};
315       {StoB_REQ};
316       {StoB_REQ; BtoS_ACK};
317       {BtoS_ACK};
318       {BtoS_ACK; BtoR_REQ};
319       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
320       {BtoS_ACK; RtoB_ACK};
321       {};
322       {StoB_REQ};
323       {StoB_REQ; BtoS_ACK};
324       {BtoS_ACK};
325       {BtoS_ACK; BtoR_REQ};
326       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
327       {BtoS_ACK; RtoB_ACK};
328       {};
329       {StoB_REQ};
330       {StoB_REQ; BtoS_ACK};
331       {BtoS_ACK};
332       {BtoS_ACK; BtoR_REQ};
333       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
334       {BtoS_ACK; RtoB_ACK};
335       {};
336       {StoB_REQ};
337       {StoB_REQ; BtoS_ACK};
338       {BtoS_ACK};
339       {BtoS_ACK; BtoR_REQ};
340       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
341       {BtoS_ACK; RtoB_ACK};
342       {};
343       {StoB_REQ};
344       {StoB_REQ; BtoS_ACK};
345       {BtoS_ACK};
346       {BtoS_ACK; BtoR_REQ};
347       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
348       {BtoS_ACK; RtoB_ACK};
349       {};
350       {StoB_REQ};
351       {StoB_REQ; BtoS_ACK};
352       {BtoS_ACK};
353       {BtoS_ACK; BtoR_REQ};
354       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
355       {BtoS_ACK; RtoB_ACK};
356       {};
357       {StoB_REQ};
358       {StoB_REQ; BtoS_ACK};
359       {BtoS_ACK};
360       {BtoS_ACK; BtoR_REQ};
361       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
362       {BtoS_ACK; RtoB_ACK};
363       {};
364       {StoB_REQ};
365       {StoB_REQ; BtoS_ACK};
366       {BtoS_ACK};
367       {BtoS_ACK; BtoR_REQ};
368       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
369       {BtoS_ACK; RtoB_ACK};
370       {};
371       {StoB_REQ};
372       {StoB_REQ; BtoS_ACK};
373       {BtoS_ACK};
374       {BtoS_ACK; BtoR_REQ};
375       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
376       {BtoS_ACK; RtoB_ACK};
377       {};
378       {StoB_REQ};
379       {StoB_REQ; BtoS_ACK};
380       {BtoS_ACK};
381       {BtoS_ACK; BtoR_REQ};
382       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
383       {BtoS_ACK; RtoB_ACK};
384       {};
385       {StoB_REQ};
386       {StoB_REQ; BtoS_ACK};
387       {BtoS_ACK};
388       {BtoS_ACK; BtoR_REQ};
389       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
390       {BtoS_ACK; RtoB_ACK};
391       {};
392       {StoB_REQ};
393       {StoB_REQ; BtoS_ACK};
394       {BtoS_ACK};
395       {BtoS_ACK; BtoR_REQ};
396       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
397       {BtoS_ACK; RtoB_ACK};
398       {};
399       {StoB_REQ};
400       {StoB_REQ; BtoS_ACK};
401       {BtoS_ACK};
402       {BtoS_ACK; BtoR_REQ};
403       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
404       {BtoS_ACK; RtoB_ACK};
405       {};
406       {StoB_REQ};
407       {StoB_REQ; BtoS_ACK};
408       {BtoS_ACK};
409       {BtoS_ACK; BtoR_REQ};
410       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
411       {BtoS_ACK; RtoB_ACK};
412       {};
413       {StoB_REQ};
414       {StoB_REQ; BtoS_ACK};
415       {BtoS_ACK};
416       {BtoS_ACK; BtoR_REQ};
417       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
418       {BtoS_ACK; RtoB_ACK};
419       {};
420       {StoB_REQ};
421       {StoB_REQ; BtoS_ACK};
422       {BtoS_ACK};
423       {BtoS_ACK; BtoR_REQ};
424       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
425       {BtoS_ACK; RtoB_ACK};
426       {};
427       {StoB_REQ};
428       {StoB_REQ; BtoS_ACK};
429       {BtoS_ACK};
430       {BtoS_ACK; BtoR_REQ};
431       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
432       {BtoS_ACK; RtoB_ACK};
433       {};
434       {StoB_REQ};
435       {StoB_REQ; BtoS_ACK};
436       {BtoS_ACK};
437       {BtoS_ACK; BtoR_REQ};
438       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
439       {BtoS_ACK; RtoB_ACK};
440       {};
441       {StoB_REQ};
442       {StoB_REQ; BtoS_ACK};
443       {BtoS_ACK};
444       {BtoS_ACK; BtoR_REQ};
445       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
446       {BtoS_ACK; RtoB_ACK};
447       {};
448       {StoB_REQ};
449       {StoB_REQ; BtoS_ACK};
450       {BtoS_ACK};
451       {BtoS_ACK; BtoR_REQ};
452       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
453       {BtoS_ACK; RtoB_ACK};
454       {};
455       {StoB_REQ};
456       {StoB_REQ; BtoS_ACK};
457       {BtoS_ACK};
458       {BtoS_ACK; BtoR_REQ};
459       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
460       {BtoS_ACK; RtoB_ACK};
461       {};
462       {StoB_REQ};
463       {StoB_REQ; BtoS_ACK};
464       {BtoS_ACK};
465       {BtoS_ACK; BtoR_REQ};
466       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
467       {BtoS_ACK; RtoB_ACK};
468       {};
469       {StoB_REQ};
470       {StoB_REQ; BtoS_ACK};
471       {BtoS_ACK};
472       {BtoS_ACK; BtoR_REQ};
473       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
474       {BtoS_ACK; RtoB_ACK};
475       {};
476       {StoB_REQ};
477       {StoB_REQ; BtoS_ACK};
478       {BtoS_ACK};
479       {BtoS_ACK; BtoR_REQ};
480       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
481       {BtoS_ACK; RtoB_ACK};
482       {};
483       {StoB_REQ};
484       {StoB_REQ; BtoS_ACK};
485       {BtoS_ACK};
486       {BtoS_ACK; BtoR_REQ};
487       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
488       {BtoS_ACK; RtoB_ACK};
489       {};
490       {StoB_REQ};
491       {StoB_REQ; BtoS_ACK};
492       {BtoS_ACK};
493       {BtoS_ACK; BtoR_REQ};
494       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
495       {BtoS_ACK; RtoB_ACK};
496       {};
497       {StoB_REQ};
498       {StoB_REQ; BtoS_ACK};
499       {BtoS_ACK};
500       {BtoS_ACK; BtoR_REQ};
501       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
502       {BtoS_ACK; RtoB_ACK};
503       {};
504       {StoB_REQ};
505       {StoB_REQ; BtoS_ACK};
506       {BtoS_ACK};
507       {BtoS_ACK; BtoR_REQ};
508       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
509       {BtoS_ACK; RtoB_ACK};
510       {};
511       {StoB_REQ};
512       {StoB_REQ; BtoS_ACK};
513       {BtoS_ACK};
514       {BtoS_ACK; BtoR_REQ};
515       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
516       {BtoS_ACK; RtoB_ACK};
517       {};
518       {StoB_REQ};
519       {StoB_REQ; BtoS_ACK};
520       {BtoS_ACK};
521       {BtoS_ACK; BtoR_REQ};
522       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
523       {BtoS_ACK; RtoB_ACK};
524       {};
525       {StoB_REQ};
526       {StoB_REQ; BtoS_ACK};
527       {BtoS_ACK};
528       {BtoS_ACK; BtoR_REQ};
529       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
530       {BtoS_ACK; RtoB_ACK};
531       {};
532       {StoB_REQ};
533       {StoB_REQ; BtoS_ACK};
534       {BtoS_ACK};
535       {BtoS_ACK; BtoR_REQ};
536       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
537       {BtoS_ACK; RtoB_ACK};
538       {};
539       {StoB_REQ};
540       {StoB_REQ; BtoS_ACK};
541       {BtoS_ACK};
542       {BtoS_ACK; BtoR_REQ};
543       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
544       {BtoS_ACK; RtoB_ACK};
545       {};
546       {StoB_REQ};
547       {StoB_REQ; BtoS_ACK};
548       {BtoS_ACK};
549       {BtoS_ACK; BtoR_REQ};
550       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
551       {BtoS_ACK; RtoB_ACK};
552       {};
553       {StoB_REQ};
554       {StoB_REQ; BtoS_ACK};
555       {BtoS_ACK};
556       {BtoS_ACK; BtoR_REQ};
557       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
558       {BtoS_ACK; RtoB_ACK};
559       {};
560       {StoB_REQ};
561       {StoB_REQ; BtoS_ACK};
562       {BtoS_ACK};
563       {BtoS_ACK; BtoR_REQ};
564       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
565       {BtoS_ACK; RtoB_ACK};
566       {};
567       {StoB_REQ};
568       {StoB_REQ; BtoS_ACK};
569       {BtoS_ACK};
570       {BtoS_ACK; BtoR_REQ};
571       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
572       {BtoS_ACK; RtoB_ACK};
573       {};
574       {StoB_REQ};
575       {StoB_REQ; BtoS_ACK};
576       {BtoS_ACK};
577       {BtoS_ACK; BtoR_REQ};
578       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
579       {BtoS_ACK; RtoB_ACK};
580       {};
581       {StoB_REQ};
582       {StoB_REQ; BtoS_ACK};
583       {BtoS_ACK};
584       {BtoS_ACK; BtoR_REQ};
585       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
586       {BtoS_ACK; RtoB_ACK};
587       {};
588       {StoB_REQ};
589       {StoB_REQ; BtoS_ACK};
590       {BtoS_ACK};
591       {BtoS_ACK; BtoR_REQ};
592       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
593       {BtoS_ACK; RtoB_ACK};
594       {};
595       {StoB_REQ};
596       {StoB_REQ; BtoS_ACK};
597       {BtoS_ACK};
598       {BtoS_ACK; BtoR_REQ};
599       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
600       {BtoS_ACK; RtoB_ACK};
601       {};
602       {StoB_REQ};
603       {StoB_REQ; BtoS_ACK};
604       {BtoS_ACK};
605       {BtoS_ACK; BtoR_REQ};
606       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
607       {BtoS_ACK; RtoB_ACK};
608       {};
609       {StoB_REQ};
610       {StoB_REQ; BtoS_ACK};
611       {BtoS_ACK};
612       {BtoS_ACK; BtoR_REQ};
613       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
614       {BtoS_ACK; RtoB_ACK};
615       {};
616       {StoB_REQ};
617       {StoB_REQ; BtoS_ACK};
618       {BtoS_ACK};
619       {BtoS_ACK; BtoR_REQ};
620       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
621       {BtoS_ACK; RtoB_ACK};
622       {};
623       {StoB_REQ};
624       {StoB_REQ; BtoS_ACK};
625       {BtoS_ACK};
626       {BtoS_ACK; BtoR_REQ};
627       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
628       {BtoS_ACK; RtoB_ACK};
629       {};
630       {StoB_REQ};
631       {StoB_REQ; BtoS_ACK};
632       {BtoS_ACK};
633       {BtoS_ACK; BtoR_REQ};
634       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
635       {BtoS_ACK; RtoB_ACK};
636       {};
637       {StoB_REQ};
638       {StoB_REQ; BtoS_ACK};
639       {BtoS_ACK};
640       {BtoS_ACK; BtoR_REQ};
641       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
642       {BtoS_ACK; RtoB_ACK};
643       {};
644       {StoB_REQ};
645       {StoB_REQ; BtoS_ACK};
646       {BtoS_ACK};
647       {BtoS_ACK; BtoR_REQ};
648       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
649       {BtoS_ACK; RtoB_ACK};
650       {};
651       {StoB_REQ};
652       {StoB_REQ; BtoS_ACK};
653       {BtoS_ACK};
654       {BtoS_ACK; BtoR_REQ};
655       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
656       {BtoS_ACK; RtoB_ACK};
657       {};
658       {StoB_REQ};
659       {StoB_REQ; BtoS_ACK};
660       {BtoS_ACK};
661       {BtoS_ACK; BtoR_REQ};
662       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
663       {BtoS_ACK; RtoB_ACK};
664       {};
665       {StoB_REQ};
666       {StoB_REQ; BtoS_ACK};
667       {BtoS_ACK};
668       {BtoS_ACK; BtoR_REQ};
669       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
670       {BtoS_ACK; RtoB_ACK};
671       {};
672       {StoB_REQ};
673       {StoB_REQ; BtoS_ACK};
674       {BtoS_ACK};
675       {BtoS_ACK; BtoR_REQ};
676       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
677       {BtoS_ACK; RtoB_ACK};
678       {};
679       {StoB_REQ};
680       {StoB_REQ; BtoS_ACK};
681       {BtoS_ACK};
682       {BtoS_ACK; BtoR_REQ};
683       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
684       {BtoS_ACK; RtoB_ACK};
685       {};
686       {StoB_REQ};
687       {StoB_REQ; BtoS_ACK};
688       {BtoS_ACK};
689       {BtoS_ACK; BtoR_REQ};
690       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
691       {BtoS_ACK; RtoB_ACK};
692       {};
693       {StoB_REQ};
694       {StoB_REQ; BtoS_ACK};
695       {BtoS_ACK};
696       {BtoS_ACK; BtoR_REQ};
697       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
698       {BtoS_ACK; RtoB_ACK};
699       {};
700       {StoB_REQ};
701       {StoB_REQ; BtoS_ACK};
702       {BtoS_ACK};
703       {BtoS_ACK; BtoR_REQ};
704       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
705       {BtoS_ACK; RtoB_ACK};
706       {};
707       {StoB_REQ};
708       {StoB_REQ; BtoS_ACK};
709       {BtoS_ACK};
710       {BtoS_ACK; BtoR_REQ};
711       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
712       {BtoS_ACK; RtoB_ACK};
713       {};
714       {StoB_REQ};
715       {StoB_REQ; BtoS_ACK};
716       {BtoS_ACK};
717       {BtoS_ACK; BtoR_REQ};
718       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
719       {BtoS_ACK; RtoB_ACK};
720       {};
721       {StoB_REQ};
722       {StoB_REQ; BtoS_ACK};
723       {BtoS_ACK};
724       {BtoS_ACK; BtoR_REQ};
725       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
726       {BtoS_ACK; RtoB_ACK};
727       {};
728       {StoB_REQ};
729       {StoB_REQ; BtoS_ACK};
730       {BtoS_ACK};
731       {BtoS_ACK; BtoR_REQ};
732       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
733       {BtoS_ACK; RtoB_ACK};
734       {};
735       {StoB_REQ};
736       {StoB_REQ; BtoS_ACK};
737       {BtoS_ACK};
738       {BtoS_ACK; BtoR_REQ};
739       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
740       {BtoS_ACK; RtoB_ACK};
741       {};
742       {StoB_REQ};
743       {StoB_REQ; BtoS_ACK};
744       {BtoS_ACK};
745       {BtoS_ACK; BtoR_REQ};
746       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
747       {BtoS_ACK; RtoB_ACK};
748       {};
749       {StoB_REQ};
750       {StoB_REQ; BtoS_ACK};
751       {BtoS_ACK};
752       {BtoS_ACK; BtoR_REQ};
753       {BtoS_ACK; BtoR_REQ; RtoB_ACK};
754       {BtoS_ACK; RtoB_ACK};
755       {}]`;
756
757quietdec := false;
758
759(******************************************************************************
760* Make "&" into an infix for F_AND
761******************************************************************************)
762val _ = set_fixity "&" (Infixl 500);
763val F_AND_IX_def = xDefine "F_AND_IX" `$& f1 f2 = F_AND(f1,f2)`;
764
765(******************************************************************************
766* Make ";;" into an infix for S_CAT
767******************************************************************************)
768val _ = set_fixity ";;" (Infixl 500);
769val S_CAT_IX_def = xDefine "S_CAT_IX" `$;; r1 r2 = S_CAT(r1,r2)`;
770
771(******************************************************************************
772* A single property characterising a four-phase handshake
773******************************************************************************)
774val FOUR_PHASE_def =
775 Define
776  `FOUR_PHASE req ack =
777    F_NEVER
778     (S_REPEAT S_TRUE ;;
779      S_BOOL(B_AND(B_NOT(B_PROP req),B_PROP ack)) ;;
780      S_BOOL(B_PROP req))
781    &
782    F_NEVER
783     (S_REPEAT S_TRUE ;;
784      S_BOOL(B_AND(B_PROP req,B_NOT(B_PROP ack))) ;;
785      S_BOOL(B_NOT(B_PROP req)))
786    &
787    F_NEVER
788     (S_REPEAT S_TRUE ;;
789      S_BOOL(B_AND(B_NOT(B_PROP ack),B_NOT(B_PROP req))) ;;
790      S_BOOL(B_PROP ack))
791    &
792    F_NEVER
793     (S_REPEAT S_TRUE ;;
794      S_BOOL(B_AND(B_PROP ack,B_PROP req)) ;;
795      S_BOOL(B_NOT(B_PROP ack)))`;
796
797(* Version without S_REPEAT S_TRUE
798val FOUR_PHASE_def =
799 Define
800  `FOUR_PHASE req ack =
801    F_NEVER
802     (
803      S_BOOL(B_AND(B_NOT(B_PROP req),B_PROP ack)) ;;
804      S_BOOL(B_PROP req))
805    &
806    F_NEVER
807     (
808      S_BOOL(B_AND(B_PROP req,B_NOT(B_PROP ack))) ;;
809      S_BOOL(B_NOT(B_PROP req)))
810    &
811    F_NEVER
812     (
813      S_BOOL(B_AND(B_NOT(B_PROP ack),B_NOT(B_PROP req))) ;;
814      S_BOOL(B_PROP ack))
815    &
816    F_NEVER
817     (
818      S_BOOL(B_AND(B_PROP ack,B_PROP req)) ;;
819      S_BOOL(B_NOT(B_PROP ack)))`;
820*)
821
822(******************************************************************************
823* Making Verilog finite state machines from FOUR_PHASE regular expressions.
824******************************************************************************)
825val alph = [``StoB_REQ``, ``BtoS_ACK``, ``BtoR_REQ``, ``RtoB_ACK``];
826
827fun regexp_ra req ack =
828  ``sere2regexp
829    (S_REPEAT S_TRUE ;;
830     S_BOOL(B_AND(B_NOT(B_PROP ^req),B_PROP ^ack)) ;;
831     S_BOOL(B_PROP ^req)) : (num -> bool) regexp``;
832
833val r1 = regexp_ra ``StoB_REQ`` ``BtoS_ACK``;
834
835val d1 = try (extract_dfa alph) r1;
836
837val inp1 = {name = "Checker1", alphabet = alph, regexp = r1};
838
839val s1 = print ("\n\n" ^ verilog_dfa inp1 ^ "\n");
840
841val r2 =
842  ``sere2regexp
843    (S_REPEAT(S_BOOL B_TRUE) ;;
844     S_BOOL(B_NOT(B_PROP BtoS_ACK)) ;;
845     S_BOOL(B_PROP BtoS_ACK) ;;
846     S_REPEAT(S_BOOL(B_AND(B_PROP BtoS_ACK,
847                           B_NOT(B_PROP RtoB_ACK)))) ;;
848     S_REPEAT(S_BOOL(B_AND(B_NOT(B_PROP BtoS_ACK),
849                           B_NOT(B_PROP RtoB_ACK)))) ;;
850     S_BOOL(B_PROP BtoS_ACK))``;
851
852val d2 = try (extract_dfa alph) r2;
853
854val inp2 = {name = "Checker2", alphabet = alph, regexp = r2};
855
856val s2 = print ("\n\n" ^ verilog_dfa inp2 ^ "\n");
857
858(******************************************************************************
859* vunit four_phase_handskake_left (page 23, FoCs User's Manual, Version 1.0)
860* FOUR_PHASE StoB_REQ BtoS_ACK
861******************************************************************************)
862
863val four_phase_handskake_left =
864 time EVAL ``F_SEM (FINITE SimRun) B_TRUE (FOUR_PHASE StoB_REQ BtoS_ACK)``;
865
866(******************************************************************************
867* vunit four_phase_handskake_right (page 24, FoCs User's Manual, Version 1.0)
868* FOUR_PHASE BtoR_REQ RtoB_ACK
869******************************************************************************)
870
871val four_phase_handskake_right =
872time EVAL ``F_SEM (FINITE SimRun) B_TRUE (FOUR_PHASE BtoR_REQ RtoB_ACK)``;
873
874(******************************************************************************
875* f1 before f2 = [not f2 W (f1 & not f2)]
876******************************************************************************)
877val F_BEFORE_def =
878 Define
879  `F_BEFORE(f1,f2) = F_W(F_NOT f2, F_AND(f1, F_NOT f2))`;
880
881(******************************************************************************
882* No underflow: ack1 is asserted between any two ack2 assertions
883******************************************************************************)
884
885val ACK_INTERLEAVE_def =
886 Define
887  `ACK_INTERLEAVE ack1 ack2 =
888    F_SUFFIX_IMP
889     ((S_REPEAT(S_BOOL B_TRUE) ;;
890       S_BOOL(B_NOT(B_PROP ack1)) ;;
891       S_BOOL(B_PROP ack1)),
892      F_BEFORE
893       (F_AND(F_NOT(F_BOOL(B_PROP ack2)),
894              F_NEXT(F_BOOL(B_PROP ack2))),
895        F_AND(F_NOT(F_BOOL(B_PROP ack1)),
896              F_NEXT(F_BOOL(B_PROP ack1)))))`;
897
898(******************************************************************************
899* vunit ack_interleaving  (page 22, FoCs User's Manual, Version 1.0)
900******************************************************************************)
901
902val ack_interleaving =
903 time
904  EVAL
905  ``F_SEM (FINITE SimRun) B_TRUE (ACK_INTERLEAVE BtoS_ACK RtoB_ACK)
906    /\
907    F_SEM (FINITE SimRun) B_TRUE (ACK_INTERLEAVE RtoB_ACK BtoS_ACK)``;
908