← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/workshops/2009/pierre-clavel-leveugle/Fault-tolerance/ATM-TMR.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/2009/pierre-clavel-leveugle/Fault-tolerance/ATM-TMR.lisp
 
1
; -----------------------------------------------------------------------------
 
2
; |                                                                           |
 
3
; | Description : ATM-TMR defines an Automatic Teller Machine control         |
 
4
; |               system that uses a TMR FSM for each register, and has:      |
 
5
; |               o Seven inputs :                                            |
 
6
; |                   - inc        : a card has been inserted                 |
 
7
; |                   - reset      : cancel button                            |
 
8
; |                   - val        : validation (after entering the code)     |
 
9
; |                   - done_op    : banking operations completed             |
 
10
; |                   - take       : card taken                               |
 
11
; |                   - cc         : card code reader output                  |
 
12
; |                   - codin      : user code reader output                  |
 
13
; |               o Four outputs :                                            |
 
14
; |                   - outc       : eject the card                           |
 
15
; |                   - keep       : don't eject the card                     |
 
16
; |                   - start_op   : banking operations can start             |
 
17
; |                   - e_detect   : error detection flag                     |
 
18
; |                                                                           |
 
19
; | The transition and output functions are automatically computed thanks     |
 
20
; | to our VSYML tool.                                                        |
 
21
; -----------------------------------------------------------------------------
 
22
 
 
23
(IN-PACKAGE "ACL2")
 
24
(include-book "register-TMR")
 
25
 
 
26
; -------------------------
 
27
; definition of the ATM FSM
 
28
; -------------------------
 
29
 
 
30
(defspec ATM-TMR
 
31
; - Signatures
 
32
  (((ATMv2-Sp          *) => *) ; State predicate
 
33
   ((ATMv2-next      * *) => *) ; transition function
 
34
   ((ATMv2-start_op  * *) => *) ; start_op output function
 
35
   ((ATMv2-keep      * *) => *) ; keep output function
 
36
   ((ATMv2-outc      * *) => *) ; outc output function
 
37
   ((ATMv2-e_detect  * *) => *) ; e_detect output function
 
38
   ((ATMv2-reach_state *) => *) ; reachable states 
 
39
   ((ATMv2-error       *) => *)); error in a ATM
 
40
 
 
41
; - Definition of type work.local_type.FSM_state
 
42
(local (defun ATMv2-FSM_statep (x)
 
43
         (or (equal x "init")
 
44
             (equal x "card_in")
 
45
             (equal x "test_code")
 
46
             (equal x "code_error")
 
47
             (equal x "code_ok")
 
48
             (equal x "card_out"))))
 
49
 
 
50
; - Constants
 
51
  (local (defconst *ATMv2/n_register*    0))
 
52
  (local (defconst *ATMv2/ok_register*   1))
 
53
  (local (defconst *ATMv2/code_register* 2))
 
54
  (local (defconst *ATMv2/c_state* 3))
 
55
  (defconst *ATMv2/reset* 0)
 
56
  (defconst *ATMv2/inc* 1)
 
57
  (defconst *ATMv2/cc* 2)
 
58
  (defconst *ATMv2/codin* 3)
 
59
  (defconst *ATMv2/val* 4)
 
60
  (defconst *ATMv2/done_op* 5)
 
61
  (defconst *ATMv2/take* 6)
 
62
  (local (defconst *ATMv2/max_try*  3))
 
63
 
 
64
; -Instances
 
65
  (local (encapsulate          ; for register n 
 
66
          (((ATMv2-n_reg-error *) => *))
 
67
          (defun ATMv2-n_reg-Sp (S) (TMR-Sp S))
 
68
          (defun ATMv2-n_reg-next (I S) (TMR-next I S))
 
69
          (defun ATMv2-n_reg-out_value (I S) (TMR-out_value I S))
 
70
          (defun ATMv2-n_reg-e_detect (I S) (TMR-e_detect I S))
 
71
          (defun ATMv2-n_reg-reach_state (S) (TMR-reach_state S))
 
72
          (local (defun ATMv2-n_reg-error (S) (TMR-error S)))
 
73
          (definstance TMR n_register
 
74
            :functional-substitution ((TMR-error ATMv2-n_reg-error))
 
75
            :rule-classes :rewrite)))
 
76
 
 
77
  (local (encapsulate           ; for register ok 
 
78
          (((ATMv2-ok_reg-error *) => *))
 
79
          (defun ATMv2-ok_reg-Sp (S) (TMR-Sp S))
 
80
          (defun ATMv2-ok_reg-next (I S) (TMR-next I S))
 
81
          (defun ATMv2-ok_reg-out_value (I S) (TMR-out_value I S))
 
82
          (defun ATMv2-ok_reg-e_detect (I S) (TMR-e_detect I S))
 
83
          (defun ATMv2-ok_reg-reach_state (S) (TMR-reach_state S))
 
84
          (local (defun ATMv2-ok_reg-error (x) (TMR-error x)))
 
85
          (definstance TMR ok_register
 
86
            :functional-substitution ((TMR-error ATMv2-ok_reg-error))
 
87
            :rule-classes :rewrite)))
 
88
 
 
89
  (local (encapsulate            ; for register code 
 
90
          (((ATMv2-code_reg-error *) => *))
 
91
          (defun ATMv2-code_reg-Sp (S) (TMR-Sp S))
 
92
          (defun ATMv2-code_reg-next (I S) (TMR-next I S))
 
93
          (defun ATMv2-code_reg-out_value (I S) (TMR-out_value I S))
 
94
          (defun ATMv2-code_reg-e_detect (I S) (TMR-e_detect I S))
 
95
          (defun ATMv2-code_reg-reach_state (S) (TMR-reach_state S))
 
96
          (local (defun ATMv2-code_reg-error (x) (TMR-error x)))
 
97
          (definstance TMR code_register
 
98
            :functional-substitution ((TMR-error ATMv2-code_reg-error))
 
99
            :rule-classes :rewrite)))
 
100
 
 
101
; - Witnesses (not "toy" witnesses, actual definitions for this ATM)
 
102
;    + Definition of ATM States
 
103
  (local (defun ATMv2-Sp (x)
 
104
           (and (true-listp x)
 
105
                (ATMv2-n_reg-Sp    (nth *ATMv2/n_register*    x))
 
106
                (ATMv2-ok_reg-Sp   (nth *ATMv2/ok_register*   x))
 
107
                (ATMv2-code_reg-Sp (nth *ATMv2/code_register* x))
 
108
                (ATMv2-FSM_statep  (nth *ATMv2/c_state* x))
 
109
                (equal (len x) 4)))) 
 
110
 
 
111
;    + Definition of the transition function
 
112
  (local (defun ATMv2-next (current_input current_state)
 
113
           (if (and (ATMv2-Sp current_state)
 
114
                    (true-listp current_input)
 
115
                    (booleanp (nth *ATMv2/reset*   current_input))
 
116
                    (booleanp (nth *ATMv2/inc*     current_input))
 
117
                    (natp     (nth *ATMv2/cc*      current_input))
 
118
                    (natp     (nth *ATMv2/codin*   current_input))
 
119
                    (booleanp (nth *ATMv2/val*     current_input))
 
120
                    (booleanp (nth *ATMv2/done_op* current_input))
 
121
                    (booleanp (nth *ATMv2/take*    current_input))
 
122
                    (equal (len current_input) 7))
 
123
               (list
 
124
                ; ATM/n_register
 
125
                (ATMv2-n_reg-next
 
126
                 (list
 
127
                  ; in_value
 
128
                  (cond ((and (equal (nth *ATMv2/c_state* current_state)
 
129
                                     "init")
 
130
                              (nth *ATMv2/inc* current_input))
 
131
                         1)
 
132
                        ((and (equal (nth *ATMv2/c_state* current_state)
 
133
                                     "test_code")
 
134
                              (not (equal 
 
135
                               (ATMv2-code_reg-out_value nil
 
136
                                (nth *ATMv2/code_register* current_state))
 
137
                               (ATMv2-ok_reg-out_value nil
 
138
                                (nth *ATMv2/ok_register* current_state))))
 
139
                              (< (ATMv2-n_reg-out_value nil 
 
140
                                  (nth *ATMv2/n_register* current_state))
 
141
                                 *ATMv2/max_try*))
 
142
                         (1+ (ATMv2-n_reg-out_value nil 
 
143
                              (nth *ATMv2/n_register* current_state))))
 
144
                        (T
 
145
                         (ATMv2-n_reg-out_value nil 
 
146
                          (nth *ATMv2/n_register* current_state))))
 
147
                  ; ld_flag
 
148
                  (or (and (equal (nth *ATMv2/c_state* current_state)
 
149
                                  "init")
 
150
                           (nth *ATMv2/inc* current_input))
 
151
                      (and (equal (nth *ATMv2/c_state* current_state)
 
152
                                  "test_code")
 
153
                           (not (equal 
 
154
                                 (ATMv2-code_reg-out_value nil 
 
155
                                  (nth *ATMv2/code_register* current_state))
 
156
                                 (ATMv2-ok_reg-out_value nil
 
157
                                  (nth *ATMv2/ok_register* current_state))))
 
158
                           (< (ATMv2-n_reg-out_value nil 
 
159
                               (nth *ATMv2/n_register* current_state))
 
160
                              *ATMv2/max_try*))))
 
161
                 (nth *ATMv2/n_register* current_state))
 
162
                ; ATM/ok_register
 
163
                (ATMv2-ok_reg-next
 
164
                 (list 
 
165
                  ; in_value
 
166
                  (cond ((and (equal (nth *ATMv2/c_state* current_state)
 
167
                                     "init")
 
168
                              (nth *ATMv2/inc* current_input))
 
169
                         (nth *ATMv2/cc* current_input))
 
170
                        ((equal (nth *ATMv2/c_state* current_state)
 
171
                                "code_error")
 
172
                         0)
 
173
                        ((and (equal (nth *ATMv2/c_state* current_state)
 
174
                                     "card_out")
 
175
                              (nth *ATMv2/take* current_input))
 
176
                         0)
 
177
                        (T
 
178
                         (ATMv2-ok_reg-out_value nil
 
179
                          (nth *ATMv2/ok_register* current_state))))
 
180
                  ; ld_flag
 
181
                  (or (and (equal (nth *ATMv2/c_state* current_state)
 
182
                                  "init")
 
183
                           (nth *ATMv2/inc* current_input))
 
184
                      (equal (nth *ATMv2/c_state* current_state)
 
185
                             "code_error")
 
186
                      (and (equal (nth *ATMv2/c_state* current_state)
 
187
                                  "card_out")
 
188
                           (nth *ATMv2/take* current_input))))
 
189
                 (nth *ATMv2/ok_register* current_state))
 
190
                ; ATM/code_register
 
191
                (ATMv2-code_reg-next
 
192
                 (list 
 
193
                  ; in_value
 
194
                  (cond ((and (equal (nth *ATMv2/c_state* current_state)
 
195
                                     "card_in")
 
196
                              (nth *ATMv2/val* current_input)
 
197
                              (not (nth *ATMv2/reset* current_input)))
 
198
                         (nth *ATMv2/codin* current_input))
 
199
                        ((equal (nth *ATMv2/c_state* current_state)
 
200
                                "code_error")
 
201
                         0)
 
202
                        ((and (equal (nth *ATMv2/c_state* current_state)
 
203
                                     "card_out")
 
204
                              (nth *ATMv2/take* current_input))
 
205
                         0)
 
206
                        (T
 
207
                         (ATMv2-code_reg-out_value nil
 
208
                          (nth *ATMv2/code_register* current_state))))
 
209
                  ; ld_flag
 
210
                  (or (and (equal (nth *ATMv2/c_state* current_state)
 
211
                                  "card_in")
 
212
                           (nth *ATMv2/val* current_input)
 
213
                           (not (nth *ATMv2/reset* current_input)))
 
214
                      (equal (nth *ATMv2/c_state* current_state)
 
215
                             "code_error")
 
216
                      (and (equal (nth *ATMv2/c_state* current_state)
 
217
                                  "card_out")
 
218
                           (nth *ATMv2/take* current_input))))
 
219
                 (nth *ATMv2/code_register* current_state))
 
220
                ; ATM/c_state
 
221
                (cond ((equal (nth *ATMv2/c_state* current_state)
 
222
                              "init") ; case c_state = init
 
223
                       (if (nth *ATMv2/inc* current_input)
 
224
                           "card_in"
 
225
                           "init"))
 
226
                      ((equal (nth *ATMv2/c_state* current_state)
 
227
                              "card_in") ; case c_state = card_in
 
228
                       (cond ((or (nth *ATMv2/reset* current_input)
 
229
                                  (or (ATMv2-n_reg-e_detect nil
 
230
                                       (nth *ATMv2/n_register* current_state))
 
231
                                      (ATMv2-ok_reg-e_detect nil
 
232
                                       (nth *ATMv2/ok_register* current_state))
 
233
                                      (ATMv2-code_reg-e_detect nil
 
234
                                       (nth *ATMv2/code_register* current_state))))
 
235
                              "card_out")
 
236
                             ((nth *ATMv2/val* current_input)
 
237
                              "test_code")
 
238
                             (T
 
239
                              "card_in")))
 
240
                      ((equal (nth *ATMv2/c_state* current_state)
 
241
                              "test_code") ; case c_state = test_code
 
242
                       (cond ((or (ATMv2-n_reg-e_detect nil
 
243
                                   (nth *ATMv2/n_register* current_state))
 
244
                                  (ATMv2-ok_reg-e_detect nil
 
245
                                   (nth *ATMv2/ok_register* current_state))
 
246
                                  (ATMv2-code_reg-e_detect nil
 
247
                                   (nth *ATMv2/code_register* current_state)))
 
248
                              "card_out")
 
249
                             ((equal (ATMv2-code_reg-out_value nil
 
250
                                      (nth *ATMv2/code_register* current_state))
 
251
                                     (ATMv2-ok_reg-out_value nil
 
252
                                      (nth *ATMv2/ok_register* current_state)))
 
253
                              "code_ok")
 
254
                             ((< (ATMv2-n_reg-out_value nil
 
255
                                   (nth *ATMv2/n_register* current_state))
 
256
                                  *ATMv2/max_try*)
 
257
                              "card_in")
 
258
                             (T
 
259
                              "code_error")))
 
260
                      ((equal (nth *ATMv2/c_state* current_state)
 
261
                              "code_error") ; case c_state = code_error
 
262
                       "init")
 
263
                      ((equal (nth *ATMv2/c_state* current_state)
 
264
                              "code_ok") ; case c_state = code_ok
 
265
                       (if (or (nth *ATMv2/reset* current_input)
 
266
                               (nth *ATMv2/done_op* current_input)
 
267
                               (or (ATMv2-n_reg-e_detect nil
 
268
                                    (nth *ATMv2/n_register* current_state))
 
269
                                   (ATMv2-ok_reg-e_detect nil
 
270
                                    (nth *ATMv2/ok_register* current_state))
 
271
                                   (ATMv2-code_reg-e_detect nil
 
272
                                    (nth *ATMv2/code_register* current_state))))
 
273
                           "card_out"
 
274
                           "code_ok"))
 
275
                      (T ; case others (card_out)
 
276
                       (if (nth *ATMv2/take* current_input)
 
277
                           "init"
 
278
                           "card_out")))
 
279
                )
 
280
               "error")))
 
281
 
 
282
;    + Definition of the function that gives the start_op output signal
 
283
  (local (defun ATMv2-start_op (current_input current_state)
 
284
           (if (and (ATMv2-Sp current_state)
 
285
                    (true-listp current_input)
 
286
                    (booleanp (nth 0 current_input)) ; reset
 
287
                    (booleanp (nth 1 current_input)) ; done_op
 
288
                    (equal (len current_input) 2))
 
289
               (or (and (equal (nth *ATMv2/c_state* current_state)
 
290
                               "test_code")
 
291
                        (equal (ATMv2-code_reg-out_value nil 
 
292
                                (nth *ATMv2/code_register* current_state))
 
293
                               (ATMv2-ok_reg-out_value nil
 
294
                                (nth *ATMv2/ok_register* current_state)))
 
295
                        (not (or (ATMv2-n_reg-e_detect nil
 
296
                                  (nth *ATMv2/n_register* current_state))
 
297
                                 (ATMv2-ok_reg-e_detect nil
 
298
                                  (nth *ATMv2/ok_register* current_state))
 
299
                                 (ATMv2-code_reg-e_detect nil
 
300
                                  (nth *ATMv2/code_register* current_state)))))
 
301
                   (and (equal (nth *ATMv2/c_state* current_state)
 
302
                               "code_ok")
 
303
                        (not (nth 0 current_input))
 
304
                        (not (nth 1 current_input))
 
305
                        (not (or (ATMv2-n_reg-e_detect nil
 
306
                                  (nth *ATMv2/n_register* current_state))
 
307
                                 (ATMv2-ok_reg-e_detect nil
 
308
                                  (nth *ATMv2/ok_register* current_state))
 
309
                                 (ATMv2-code_reg-e_detect nil
 
310
                                  (nth *ATMv2/code_register* current_state))))))
 
311
               "error")))
 
312
 
 
313
;    + Definition of the function that gives the keep output signal
 
314
  (local (defun ATMv2-keep (current_input current_state)
 
315
           (if (and (ATMv2-Sp current_state)
 
316
                    (true-listp current_input)
 
317
                    (equal (len current_input) 0))
 
318
               (and (equal (nth *ATMv2/c_state* current_state)
 
319
                           "test_code")
 
320
                    (not (equal (ATMv2-code_reg-out_value nil
 
321
                                 (nth *ATMv2/code_register* current_state))
 
322
                                (ATMv2-ok_reg-out_value nil
 
323
                                 (nth *ATMv2/ok_register* current_state))))
 
324
                    (>= (ATMv2-n_reg-out_value nil 
 
325
                         (nth *ATMv2/n_register* current_state))
 
326
                        *ATMv2/max_try*)
 
327
                    (not (or (ATMv2-n_reg-e_detect nil
 
328
                              (nth *ATMv2/n_register* current_state))
 
329
                             (ATMv2-ok_reg-e_detect nil
 
330
                              (nth *ATMv2/ok_register* current_state))
 
331
                             (ATMv2-code_reg-e_detect nil
 
332
                              (nth *ATMv2/code_register* current_state)))))
 
333
               "error")))
 
334
 
 
335
;    + Definition of the function that gives the outc output signal
 
336
  (local (defun ATMv2-outc (current_input current_state)
 
337
           (if (and (ATMv2-Sp current_state)
 
338
                    (true-listp current_input)
 
339
                    (booleanp (nth 0 current_input)) ; reset
 
340
                    (booleanp (nth 1 current_input)) ; done_op
 
341
                    (equal (len current_input) 2))
 
342
               (or (and (equal (nth *ATMv2/c_state* current_state)
 
343
                               "code_ok")
 
344
                        (or (nth 0 current_input)
 
345
                            (nth 1 current_input)
 
346
                            (or (ATMv2-n_reg-e_detect nil
 
347
                                 (nth *ATMv2/n_register* current_state))
 
348
                                (ATMv2-ok_reg-e_detect nil
 
349
                                 (nth *ATMv2/ok_register* current_state))
 
350
                                (ATMv2-code_reg-e_detect nil
 
351
                                 (nth *ATMv2/code_register* current_state)))))
 
352
                   (and (equal (nth *ATMv2/c_state* current_state)
 
353
                               "card_in")
 
354
                        (or (nth 0 current_input)
 
355
                            (or (ATMv2-n_reg-e_detect nil
 
356
                                 (nth *ATMv2/n_register* current_state))
 
357
                                (ATMv2-ok_reg-e_detect nil
 
358
                                 (nth *ATMv2/ok_register* current_state))
 
359
                                (ATMv2-code_reg-e_detect nil
 
360
                                 (nth *ATMv2/code_register* current_state)))))
 
361
                   (and (equal (nth *ATMv2/c_state* current_state)
 
362
                               "test_code")
 
363
                        (or (ATMv2-n_reg-e_detect nil
 
364
                             (nth *ATMv2/n_register* current_state))
 
365
                            (ATMv2-ok_reg-e_detect nil
 
366
                             (nth *ATMv2/ok_register* current_state))
 
367
                            (ATMv2-code_reg-e_detect nil
 
368
                             (nth *ATMv2/code_register* current_state)))))
 
369
               "error")))
 
370
 
 
371
;    + Definition of the function that gives the e_detect output signal
 
372
  (local (defun ATMv2-e_detect (current_input current_state)
 
373
           (if (and (ATMv2-Sp current_state)
 
374
                    (true-listp current_input)
 
375
                    (equal (len current_input) 0))
 
376
               (or (ATMv2-n_reg-e_detect nil
 
377
                    (nth *ATMv2/n_register* current_state))
 
378
                   (ATMv2-ok_reg-e_detect nil
 
379
                    (nth *ATMv2/ok_register* current_state))
 
380
                   (ATMv2-code_reg-e_detect nil
 
381
                    (nth *ATMv2/code_register* current_state)))
 
382
               "error")))
 
383
 
 
384
;    + Definition of ATM reachable states
 
385
  (local (defun ATMv2-reach_state (S)
 
386
           (and (ATMv2-Sp S)
 
387
                (ATMv2-n_reg-reach_state (nth *ATMv2/n_register* S))
 
388
                (ATMv2-ok_reg-reach_state (nth *ATMv2/ok_register* S))
 
389
                (ATMv2-code_reg-reach_state (nth *ATMv2/code_register* S)))))
 
390
 
 
391
;    + Definition of an error in a ATM FSM
 
392
;      * The error is located in register n
 
393
  (local (defun ATMv2-inject1 (x)
 
394
           (if (ATMv2-Sp x)
 
395
               (list (ATMv2-n_reg-error (nth *ATMv2/n_register* x))
 
396
                     (nth *ATMv2/ok_register*   x)
 
397
                     (nth *ATMv2/code_register* x)
 
398
                     (nth *ATMv2/c_state* x)
 
399
                     )
 
400
               "error")))
 
401
 
 
402
;      * Or the error is located in register ok
 
403
  (local (defun ATMv2-inject2 (x)
 
404
           (if (ATMv2-Sp x)
 
405
               (list (nth *ATMv2/n_register* x)
 
406
                     (ATMv2-ok_reg-error (nth *ATMv2/ok_register* x))
 
407
                     (nth *ATMv2/code_register* x)
 
408
                     (nth *ATMv2/c_state* x)
 
409
                     )
 
410
               "error")))
 
411
 
 
412
;      * Or the error is located in register code
 
413
  (local (defun ATMv2-inject3 (x)
 
414
           (if (ATMv2-Sp x)
 
415
               (list (nth *ATMv2/n_register* x)
 
416
                     (nth *ATMv2/ok_register* x)
 
417
                     (ATMv2-code_reg-error (nth *ATMv2/code_register* x))
 
418
                     (nth *ATMv2/c_state* x)
 
419
                     )
 
420
               "error")))
 
421
 
 
422
;      * Definition of the error model
 
423
  (local (encapsulate
 
424
          (((ATMv2-error *) => *))
 
425
          (local (defun ATMv2-error (x) (ATMv2-inject1 x)))
 
426
          (defthm ATMv2-error-type1
 
427
            (equal (ATMv2-Sp (ATMv2-error x))
 
428
                   (ATMv2-Sp x)))
 
429
          (defthm ATMv2-error-type2
 
430
            (implies (not (ATMv2-Sp x))
 
431
                     (equal (ATMv2-error x) "error")))
 
432
          (defthm ATMv2-error-def1
 
433
            (implies (ATMv2-Sp x)
 
434
                     (not (equal (ATMv2-error x) x))))
 
435
          (defthm ATMv2-error-def2   ; the error can be located in any of the 3 registers
 
436
            (or (equal (ATMv2-error x)
 
437
                       (ATMv2-inject1 x))
 
438
                (equal (ATMv2-error x)
 
439
                       (ATMv2-inject2 x))
 
440
                (equal (ATMv2-error x)
 
441
                       (ATMv2-inject3 x)))
 
442
            :hints (("Goal" :in-theory (disable ATMv2-Sp)))
 
443
            :rule-classes nil)))
 
444
 
 
445
; - Typing properties
 
446
; -------------------
 
447
 
 
448
;    + Sp is a predicate
 
449
  (defthm ATMv2-thm-Sp-type
 
450
    (booleanp (ATMv2-Sp S))
 
451
    :rule-classes ((:type-prescription :typed-term (ATMv2-Sp S))))
 
452
 
 
453
;    + "error" is not a Sp (speeds up proofs)
 
454
  (defthm ATMv2-thm-Sp-error
 
455
    (not (ATMv2-Sp "error"))
 
456
    :rule-classes :rewrite)
 
457
 
 
458
;    + Output of the transition function
 
459
  (defthm ATMv2-thm-next-type1
 
460
    (implies (ATMv2-Sp S)
 
461
             (equal (ATMv2-Sp (ATMv2-next I S))
 
462
                    (and (true-listp I)
 
463
                         (booleanp (nth *ATMv2/reset*   I))
 
464
                         (booleanp (nth *ATMv2/inc*     I))
 
465
                         (natp     (nth *ATMv2/cc*      I))
 
466
                         (natp     (nth *ATMv2/codin*   I))
 
467
                         (booleanp (nth *ATMv2/val*     I))
 
468
                         (booleanp (nth *ATMv2/done_op* I))
 
469
                         (booleanp (nth *ATMv2/take*    I))
 
470
                         (equal (len I) 7))))
 
471
    :rule-classes :rewrite)
 
472
 
 
473
;    + Input of the transition function
 
474
  (defthm ATMv2-thm-next-type2
 
475
    (implies (or (not (ATMv2-Sp S))
 
476
                 (not (true-listp I))
 
477
                 (not (booleanp (nth *ATMv2/reset*   I)))
 
478
                 (not (booleanp (nth *ATMv2/inc*     I)))
 
479
                 (not (natp     (nth *ATMv2/cc*      I)))
 
480
                 (not (natp     (nth *ATMv2/codin*   I)))
 
481
                 (not (booleanp (nth *ATMv2/val*     I)))
 
482
                 (not (booleanp (nth *ATMv2/done_op* I)))
 
483
                 (not (booleanp (nth *ATMv2/take*    I)))
 
484
                 (not (equal (len I) 7)))
 
485
             (equal (ATMv2-next I S)
 
486
                    "error"))
 
487
    :rule-classes :rewrite)
 
488
 
 
489
;    + Output of the function that gives the start_op output signal
 
490
  (defthm ATMv2-thm-start_op-type1
 
491
    (implies (ATMv2-Sp S)
 
492
             (equal (booleanp (ATMv2-start_op I S))
 
493
                    (and (true-listp I)
 
494
                         (booleanp (nth 0 I)) ; reset
 
495
                         (booleanp (nth 1 I)) ; done_op
 
496
                         (equal (len I) 2))))
 
497
    :rule-classes :rewrite)
 
498
 
 
499
;    + Input of the function that gives the start_op output signal
 
500
  (defthm ATMv2-thm-start_op-type2
 
501
    (implies (or (not (ATMv2-Sp S))
 
502
                 (not (true-listp I))
 
503
                 (not (booleanp (nth 0 I)))
 
504
                 (not (booleanp (nth 1 I)))
 
505
                 (not (equal (len I) 2)))
 
506
             (equal (ATMv2-start_op I S)
 
507
                    "error"))
 
508
    :rule-classes :rewrite)
 
509
 
 
510
;    + Output of the function that gives the keep output signal
 
511
  (defthm ATMv2-thm-keep-type1
 
512
    (implies (ATMv2-Sp S)
 
513
             (equal (booleanp (ATMv2-keep I S))
 
514
                    (and (true-listp I)
 
515
                         (equal (len I) 0))))
 
516
    :rule-classes :rewrite)
 
517
 
 
518
;    + Input of the function that gives the keep output signal
 
519
  (defthm ATMv2-thm-keep-type2
 
520
    (implies (or (not (ATMv2-Sp S))
 
521
                 (not (true-listp I))
 
522
                 (not (equal (len I) 0)))
 
523
             (equal (ATMv2-keep I S)
 
524
                    "error"))
 
525
    :rule-classes :rewrite)
 
526
 
 
527
;    + Output of the function that gives the outc output signal
 
528
  (defthm ATMv2-thm-outc-type1
 
529
    (implies (ATMv2-Sp S)
 
530
             (equal (booleanp (ATMv2-outc I S))
 
531
                    (and (true-listp I)
 
532
                         (booleanp (nth 0 I)) ; reset
 
533
                         (booleanp (nth 1 I)) ; done_op
 
534
                         (equal (len I) 2))))
 
535
    :rule-classes :rewrite)
 
536
 
 
537
;    + Input of the function that gives the outc output signal
 
538
  (defthm ATMv2-thm-outc-type2
 
539
    (implies (or (not (ATMv2-Sp S))
 
540
                 (not (true-listp I))
 
541
                 (not (booleanp (nth 0 I)))
 
542
                 (not (booleanp (nth 1 I)))
 
543
                 (not (equal (len I) 2)))
 
544
             (equal (ATMv2-outc I S)
 
545
                    "error"))
 
546
    :rule-classes :rewrite)
 
547
 
 
548
;    + Output of the function that gives the e_detect output signal
 
549
  (defthm ATMv2-thm-e_detect-type1
 
550
    (implies (ATMv2-Sp S)
 
551
             (equal (booleanp (ATMv2-e_detect I S))
 
552
                    (and (true-listp I)
 
553
                         (equal (len I) 0))))
 
554
    :rule-classes :rewrite)
 
555
 
 
556
;    + Input of the function that gives the e_detect output signal
 
557
  (defthm ATMv2-thm-e_detect-type2
 
558
    (implies (or (not (ATMv2-Sp S))
 
559
                 (not (true-listp I))
 
560
                 (not (equal (len I) 0)))
 
561
             (equal (ATMv2-e_detect I S)
 
562
                    "error"))
 
563
    :rule-classes :rewrite)
 
564
 
 
565
;    + reach_state is a predicate
 
566
  (defthm ATMv2-thm-reach_state-type
 
567
    (booleanp (ATMv2-reach_state S))
 
568
    :rule-classes ((:type-prescription :typed-term (ATMv2-reach_state S))))
 
569
 
 
570
;    + Output of error is a Sp
 
571
  (defthm ATMv2-thm-error-type1
 
572
    (equal (ATMv2-Sp (ATMv2-error S))
 
573
           (ATMv2-Sp S))
 
574
    :rule-classes :rewrite)
 
575
 
 
576
;    + Input of error is a Sp
 
577
  (defthm ATMv2-thm-error-type2
 
578
    (implies (not (ATMv2-Sp S))
 
579
             (equal (ATMv2-error S)
 
580
                    "error"))
 
581
    :rule-classes :rewrite)
 
582
 
 
583
;    + the transition function returns a reachable state
 
584
  (defthm ATMv2-thm-reach_state
 
585
    (implies (and (ATMv2-Sp S)
 
586
                  (ATMv2-reach_state S))
 
587
             (equal (ATMv2-reach_state (ATMv2-next I S))
 
588
                    (and (true-listp I)
 
589
                         (booleanp (nth *ATMv2/reset*   I))
 
590
                         (booleanp (nth *ATMv2/inc*     I))
 
591
                         (natp     (nth *ATMv2/cc*      I))
 
592
                         (natp     (nth *ATMv2/codin*   I))
 
593
                         (booleanp (nth *ATMv2/val*     I))
 
594
                         (booleanp (nth *ATMv2/done_op* I))
 
595
                         (booleanp (nth *ATMv2/take*    I))
 
596
                         (equal (len I) 7))))
 
597
    :rule-classes :rewrite)
 
598
 
 
599
; - Robustness-related properties
 
600
; -------------------------------
 
601
 
 
602
;    + fault-injection is actual
 
603
  (defthm ATMv2-thm-error
 
604
    (implies (ATMv2-Sp S)
 
605
             (not (equal (ATMv2-error S) S)))
 
606
    :rule-classes ((:forward-chaining :match-free :all
 
607
                                      :trigger-terms ((ATMv2-Sp S)))))
 
608
 
 
609
;    + an error does not change the symbolic state
 
610
  (local (defthm ATMv2-thm-symbolicstate-unchanged
 
611
    (implies (ATMv2-Sp S)
 
612
             (equal (nth *ATMv2/c_state* (ATMv2-error S))
 
613
                    (nth *ATMv2/c_state* S)))
 
614
    :hints (("Goal" :use (:instance ATMv2-error-def2 (x S))))
 
615
    :rule-classes :rewrite))
 
616
 
 
617
;    + an error is corrected after one clock tick
 
618
  (defthm ATMv2-thm-hardened-1
 
619
    (implies (and (ATMv2-Sp S)
 
620
                  (ATMv2-reach_state S)
 
621
                  (true-listp I)
 
622
                  (booleanp (nth *ATMv2/reset*   I))
 
623
                  (booleanp (nth *ATMv2/inc*     I))
 
624
                  (natp     (nth *ATMv2/cc*      I))
 
625
                  (natp     (nth *ATMv2/codin*   I))
 
626
                  (booleanp (nth *ATMv2/val*     I))
 
627
                  (booleanp (nth *ATMv2/done_op* I))
 
628
                  (booleanp (nth *ATMv2/take*    I))
 
629
                  (equal (len I) 7))
 
630
             (equal (ATMv2-next I (ATMv2-error S))
 
631
                    (ATMv2-next I S)))
 
632
    :hints (("Goal" :use (:instance ATMv2-error-def2 (x S))
 
633
                    :in-theory (disable booleanp)))
 
634
    :rule-classes :rewrite)
 
635
 
 
636
;    + the start_op output signal is unchanged when an error occurs
 
637
  (defthm ATMv2-thm-hardened-2    
 
638
    (implies (and (ATMv2-Sp S)
 
639
                  (true-listp I)
 
640
                  (booleanp (nth 0 I))
 
641
                  (booleanp (nth 1 I))
 
642
                  (equal (len I) 2)
 
643
                  (ATMv2-reach_state S))
 
644
             (equal (ATMv2-start_op I (ATMv2-error S))
 
645
                    (ATMv2-start_op I S)))
 
646
    :hints (("Goal" :use (:instance ATMv2-error-def2 (x S))))
 
647
    :rule-classes :rewrite)
 
648
 
 
649
;    + the keep output signal is unchanged when an error occurs
 
650
  (defthm ATMv2-thm-hardened-3
 
651
    (implies (and (ATMv2-Sp S)
 
652
                  (ATMv2-reach_state S))
 
653
             (equal (ATMv2-keep nil (ATMv2-error S))
 
654
                    (ATMv2-keep nil S)))
 
655
    :hints (("Goal" :use (:instance ATMv2-error-def2 (x S))))
 
656
    :rule-classes :rewrite)
 
657
 
 
658
;    + the outc output signal is unchanged when an error occurs
 
659
  (defthm ATMv2-thm-hardened-4
 
660
    (implies (and (ATMv2-Sp S)
 
661
                  (true-listp I)
 
662
                  (booleanp (nth 0 I))
 
663
                  (booleanp (nth 1 I))
 
664
                  (equal (len I) 2)
 
665
                  (ATMv2-reach_state S))
 
666
             (equal (ATMv2-outc I (ATMv2-error S))
 
667
                    (ATMv2-outc I S)))
 
668
    :hints (("Goal" :use (:instance ATMv2-error-def2 (x S))))
 
669
    :rule-classes :rewrite)
 
670
)
 
671
 
 
672
; -------------------------------------------------
 
673
; Then, robustness-related properties over n cycles
 
674
; -------------------------------------------------
 
675
 
 
676
; Definition of a well-formed trace
 
677
(defun SPEC-ATMv2-Ip (x)
 
678
  (and (true-listp x)
 
679
       (booleanp (nth *ATMv2/reset*   x))
 
680
       (booleanp (nth *ATMv2/inc*     x))
 
681
       (natp     (nth *ATMv2/cc*      x))
 
682
       (natp     (nth *ATMv2/codin*   x))
 
683
       (booleanp (nth *ATMv2/val*     x))
 
684
       (booleanp (nth *ATMv2/done_op* x))
 
685
       (booleanp (nth *ATMv2/take*    x))
 
686
       (equal (len x) 7)))
 
687
; - An input trace is a list of inputs
 
688
(defun SPEC-ATMv2-Trace-Ip (x)
 
689
  (and (true-listp x)
 
690
       (or (null x)
 
691
           (and (SPEC-ATMv2-Ip (car x))
 
692
                (SPEC-ATMv2-Trace-Ip (cdr x))))))
 
693
 
 
694
; - Definition of the recursive application of the transition function
 
695
(defun SPEC-ATMv2-rec-next (input_trace initial_state)
 
696
  (if (and (ATMv2-Sp initial_state)
 
697
           (SPEC-ATMv2-Trace-Ip input_trace))
 
698
      (if (null input_trace)
 
699
          initial_state
 
700
          (ATMv2-next (car input_trace)
 
701
                      (SPEC-ATMv2-rec-next (cdr input_trace)
 
702
                                           initial_state)))
 
703
      "error"))
 
704
 
 
705
; Typing properties
 
706
; -----------------
 
707
 
 
708
; - Output of SPEC-ATMv2-rec-next is a Sp
 
709
(defthm SPEC-ATMv2-thm-rec-next-type1
 
710
  (implies (ATMv2-Sp initial_state)
 
711
           (equal (ATMv2-Sp (SPEC-ATMv2-rec-next input_trace initial_state))
 
712
                  (SPEC-ATMv2-Trace-Ip input_trace)))
 
713
  :rule-classes :rewrite)
 
714
 
 
715
; Output of SPEC-ATMv2-rec-next is a reach_state
 
716
(defthm SPEC-ATMv2-thm-rec-next-reach_state
 
717
  (implies (and (ATMv2-Sp initial_state) ; for all state
 
718
                (ATMv2-reach_state initial_state) ; being a reachable state
 
719
                (SPEC-ATMv2-Trace-Ip input_trace)) ; and all input trace
 
720
           (ATMv2-reach_state (SPEC-ATMv2-rec-next input_trace initial_state)))
 
721
  :rule-classes :rewrite)
 
722
 
 
723
; Input of SPEC-ATMv2-rec-next
 
724
(defthm SPEC-ATMv2-thm-rec-next-type2
 
725
  (implies (or (not (ATMv2-Sp S))
 
726
               (not (SPEC-ATMv2-Trace-Ip I)))
 
727
           (equal (SPEC-ATMv2-rec-next I S)
 
728
                  "error"))
 
729
  :rule-classes :rewrite)
 
730
 
 
731
; Robustness-related props
 
732
; ------------------------
 
733
 
 
734
; - If an error is injected in a ATMv2 FSM after n clock ticks,
 
735
;   it will be corrected one clock cycle later
 
736
(defthm SPEC-ATMv2-test1
 
737
  (implies
 
738
   (and (ATMv2-Sp initial_state) ; for all state
 
739
        (ATMv2-reach_state initial_state) ; being a reachable state
 
740
        (SPEC-ATMv2-Trace-Ip input_trace) ; and all input trace
 
741
        (SPEC-ATMv2-Ip last_input)) ; and all last input
 
742
   (equal (ATMv2-next last_input
 
743
                      (ATMv2-error (SPEC-ATMv2-rec-next input_trace
 
744
                                                        initial_state)))
 
745
          (ATMv2-next last_input
 
746
                                   (SPEC-ATMv2-rec-next input_trace
 
747
                                                        initial_state))))
 
748
  :rule-classes nil) 
 
749
 
 
750
; - If an error is injected in a ATMv2 FSM after n clock ticks, 
 
751
; the start_op output signal keeps its value on the next clock tick
 
752
(defthm SPEC-ATMv2-test2
 
753
  (implies
 
754
   (and (ATMv2-Sp initial_state) ; for all state
 
755
        (ATMv2-reach_state initial_state) ; being a reachable state
 
756
        (SPEC-ATMv2-Trace-Ip input_trace) ; and all input trace
 
757
        (true-listp last_input) ; and all last start_op input
 
758
        (booleanp (nth 0 last_input))
 
759
        (booleanp (nth 1 last_input))
 
760
        (equal (len last_input) 2)) 
 
761
   (equal (ATMv2-start_op last_input
 
762
                          (ATMv2-error (SPEC-ATMv2-rec-next input_trace
 
763
                                                            initial_state)))
 
764
          (ATMv2-start_op last_input
 
765
                                       (SPEC-ATMv2-rec-next input_trace
 
766
                                                            initial_state))))
 
767
  :rule-classes nil) 
 
768
 
 
769
; - If an error is injected in a ATMv2 FSM after n clock ticks,
 
770
; the keep output signal keeps its value on the next clock tick
 
771
(defthm SPEC-ATMv2-test3
 
772
  (implies
 
773
   (and (ATMv2-Sp initial_state) ; for all state
 
774
        (ATMv2-reach_state initial_state) ; being a reachable state
 
775
        (SPEC-ATMv2-Trace-Ip input_trace)) ; and all input trace
 
776
   (equal (ATMv2-keep nil
 
777
                      (ATMv2-error (SPEC-ATMv2-rec-next input_trace
 
778
                                                        initial_state)))
 
779
          (ATMv2-keep nil
 
780
                                   (SPEC-ATMv2-rec-next input_trace
 
781
                                                        initial_state))))
 
782
  :rule-classes nil) 
 
783
 
 
784
; - If an error is injected in a ATMv2 FSM after n clock ticks,
 
785
; the outc output signal keeps its value on the next clock tick
 
786
(defthm SPEC-ATMv2-test4
 
787
  (implies
 
788
   (and (ATMv2-Sp initial_state) ; for all state
 
789
        (ATMv2-reach_state initial_state) ; being a reachable state
 
790
        (SPEC-ATMv2-Trace-Ip input_trace) ; and all input trace
 
791
        (true-listp last_input) ; and all last input
 
792
        (booleanp (nth 0 last_input))
 
793
        (booleanp (nth 1 last_input))
 
794
        (equal (len last_input) 2)) 
 
795
   (equal (ATMv2-outc last_input
 
796
                      (ATMv2-error (SPEC-ATMv2-rec-next input_trace
 
797
                                                        initial_state)))
 
798
          (ATMv2-outc last_input
 
799
                                   (SPEC-ATMv2-rec-next input_trace
 
800
                                                        initial_state))))
 
801
  :rule-classes nil)