← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/pipeline/non-deterministic-systems/int/ma-int.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/manolios/pipeline/pipeline/non-deterministic-systems/int/ma-int.lisp
 
1
;  Copyright (C) 2000 Panagiotis Manolios
 
2
 
 
3
;  This program is free software; you can redistribute it and/or modify
 
4
;  it under the terms of the GNU General Public License as published by
 
5
;  the Free Software Foundation; either version 2 of the License, or
 
6
;  (at your option) any later version.
 
7
 
 
8
;  This program is distributed in the hope that it will be useful,
 
9
;  but WITHOUT ANY WARRANTY; without even the implied warranty of
 
10
;  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 
11
;  GNU General Public License for more details.
 
12
 
 
13
;  You should have received a copy of the GNU General Public License
 
14
;  along with this program; if not, write to the Free Software
 
15
;  Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 
16
 
 
17
;  Written by Panagiotis Manolios who can be reached as follows.
 
18
 
 
19
;  Email: pete@cs.utexas.edu
 
20
 
 
21
;  Postal Mail:
 
22
;  Department of Computer Science
 
23
;  The University of Texas at Austin
 
24
;  Austin, TX 78701 USA
 
25
 
 
26
#|
 
27
 
 
28
The MA specification of Sawada's machine with interrupts.
 
29
 
 
30
|#
 
31
 
 
32
(in-package "ACL2")
 
33
 
 
34
(include-book "isa-int")
 
35
(include-book "../top/non-det-macros")
 
36
 
 
37
(defun latch1 (validp op rc ra rb)
 
38
  (list 'latch1 validp op rc ra rb))
 
39
 
 
40
(defmacro latch1-validp () 1)
 
41
 
 
42
(defmacro latch1-op () 2)
 
43
 
 
44
(defmacro latch1-rc () 3)
 
45
 
 
46
(defmacro latch1-ra () 4)
 
47
 
 
48
(defmacro latch1-rb () 5)
 
49
 
 
50
(defun latch2 (validp op rc ra-val rb-val)
 
51
  (list 'latch2 validp op rc ra-val rb-val))
 
52
 
 
53
(defmacro latch2-validp () 1)
 
54
 
 
55
(defmacro latch2-op () 2)
 
56
 
 
57
(defmacro latch2-rc () 3)
 
58
 
 
59
(defmacro latch2-ra-val () 4)
 
60
 
 
61
(defmacro latch2-rb-val () 5)
 
62
 
 
63
(defun MA-state (pc regs mem latch1 latch2 int)
 
64
  (list 'MA pc regs mem latch1 latch2 int))
 
65
 
 
66
(defun MA-p (x)
 
67
  (equal (car x) 'MA))
 
68
 
 
69
(defmacro MA-pc () 1)
 
70
 
 
71
(defmacro MA-regs () 2)
 
72
 
 
73
(defmacro MA-mem () 3)
 
74
 
 
75
(defmacro MA-latch1 () 4)
 
76
 
 
77
(defmacro MA-latch2 () 5)
 
78
 
 
79
(defmacro MA-int () 6)
 
80
 
 
81
(defun ALU-output (op val1 val2)
 
82
  (cond ((equal op 0) 
 
83
         (+ val1 val2))
 
84
        (t (* val1 val2))))
 
85
 
 
86
(defun step-regs (MA)
 
87
  (let ((latch2 (nth (MA-latch2) MA)))
 
88
    (if (and (nth (latch2-validp) latch2)
 
89
             (bor (equal (nth (latch2-op) latch2) 0)
 
90
                  (equal (nth (latch2-op) latch2) 1)))
 
91
        (update-valuation (nth (latch2-rc) latch2)
 
92
                          (ALU-output (nth (latch2-op) latch2)
 
93
                                      (nth (latch2-ra-val) latch2)
 
94
                                      (nth (latch2-rb-val) latch2))
 
95
                          (nth (MA-regs) MA))
 
96
      (nth (MA-regs) MA))))
 
97
 
 
98
(defun stall-condp (MA)
 
99
  (let ((latch1 (nth (MA-latch1) MA))
 
100
        (latch2 (nth (MA-latch2) MA)))
 
101
    (and (nth (latch2-validp) latch2)
 
102
         (nth (latch1-validp) latch1)
 
103
         (bor (equal (nth (latch1-ra) latch1) 
 
104
                     (nth (latch2-rc) latch2))
 
105
              (equal (nth (latch1-rb) latch1) 
 
106
                     (nth (latch2-rc) latch2))))))
 
107
 
 
108
(defun step-latch1 (MA)
 
109
  (let ((latch1 (nth (MA-latch1) MA))
 
110
        (inst (value-of (nth (MA-pc) MA) (nth (MA-mem) MA))))
 
111
    (cond ((stall-condp MA)
 
112
           latch1)
 
113
          (t (latch1 t
 
114
                     (nth (Inst-opcode) inst)
 
115
                     (nth (Inst-rc) inst)
 
116
                     (nth (Inst-ra) inst)
 
117
                     (nth (Inst-rb) inst))))))
 
118
 
 
119
(defun step-latch2 (MA)
 
120
  (let ((latch1 (nth (MA-latch1) MA)))
 
121
    (if (nth (latch1-validp) latch1)
 
122
        (latch2 (not (stall-condp MA))
 
123
                (nth (latch1-op) latch1)
 
124
                (nth (latch1-rc) latch1)
 
125
                (value-of (nth (latch1-ra) latch1) 
 
126
                          (nth (MA-regs) MA))
 
127
                (value-of (nth (latch1-rb) latch1) 
 
128
                          (nth (MA-regs) MA)))
 
129
      (update-nth (latch2-validp) nil (nth (MA-latch2) MA)))))
 
130
 
 
131
(defun step-pc (MA)
 
132
  (if (stall-condp MA)
 
133
      (nth (MA-pc) MA)
 
134
    (1+ (nth (MA-pc) MA))))
 
135
 
 
136
(defun b-to-num (x)
 
137
  (if x 1 0))
 
138
 
 
139
(defun shift-pc (latch1 latch2)
 
140
  (+ (b-to-num (nth (latch1-validp) latch1))
 
141
     (b-to-num (nth (latch2-validp) latch2))))
 
142
 
 
143
(defun committed-MA (MA)
 
144
  (let ((pc (nth (MA-pc) MA))
 
145
        (regs (nth (MA-regs) MA))
 
146
        (mem (nth (MA-mem) MA))
 
147
        (latch1 (nth (MA-latch1) MA))
 
148
        (latch2 (nth (MA-latch2) MA))
 
149
        (int (nth (MA-int) MA)))
 
150
    (MA-state
 
151
     (- pc (shift-pc latch1 latch2))
 
152
     regs
 
153
     mem
 
154
     (update-nth (latch1-validp) nil latch1)
 
155
     (update-nth (latch2-validp) nil latch2)
 
156
     int)))
 
157
 
 
158
(defun MA-step (MA i)
 
159
  (cond ((nth (MA-int) MA)
 
160
         (update-nth (MA-mem) 
 
161
                     (int-handler (nth (MA-regs) MA) 
 
162
                                  (nth (MA-mem) MA) 
 
163
                                  (nth (MA-int) MA))
 
164
                     (update-nth (MA-int) 
 
165
                                 nil
 
166
                                 (committed-MA MA))))
 
167
        (i (update-nth (MA-int) i (committed-MA MA)))
 
168
        (t (MA-state (step-pc MA)
 
169
                     (step-regs MA)
 
170
                     (nth (MA-mem) MA)
 
171
                     (step-latch1 MA)
 
172
                     (step-latch2 MA)
 
173
                     nil))))