1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(in-package "ACL2")
(set-case-split-limitations 'nil)
(include-book "refinement-sfm06-with-hazards")
;:trans1
(generate-full-system isa-step isa-p ma-step ma-p
ma-to-isa good-ma ma-rank)
(include-book "acl2s/cgen/top" :dir :system :ttags :all)
;----------Data definitions----------------------------------
(defdata reg acl2s::nat)
(defdata pc-type acl2s::nat)
(defdata data integer)
(defdata register (map reg data))
(defun boolp (x)
(declare (xargs :guard t))
(booleanp x))
(defun bool-enum (x)
(if (> x 100) t nil))
(acl2s::register-type bool :predicate boolp :enumerator bool-enum)
(defdata dmemory (map acl2s::nat data))
(defdata operation-code (oneof 'add 'sub 'mul 'load 'loadi 'store 'bez 'jump))
(defdata inst (record (opcode . operation-code)
(rc . reg)
(ra . reg)
(rb . reg)))
(defdata imemory (map pc-type inst))
(defdata ISA-type 'ISA)
(defdata ISA-testing (record
(type . ISA-type)
(pc . pc-type)
(regs . register)
(imem . imemory)
(dmem . dmemory)))
(acl2s::register-type ISA :enumerator nth-ISA-testing :predicate ISA-p)
(defdata latch1-type 'latch1)
(defdata latch1-testing (record (type . latch1-type)
(validp . bool)
(op . operation-code)
(rc . reg)
(ra . reg)
(rb . reg)
(pch . pc-type)))
;(acl2s::register-type latch1 :enumerator nth-latch1-testing :predicate latch1p)
(defdata latch2-type 'latch2)
(defdata latch2-testing (record (type . latch2-type)
(validp . bool)
(op . operation-code)
(rc . reg)
(ra-val . data)
(rb-val . data)
(pch . pc-type)))
;(acl2s::register-type latch2 :enumerator nth-latch2-testing :predicate latch2p)
(defdata MA-type 'MA)
(defdata MA-testing (record (type . MA-type)
(pc . pc-type)
(regs . register)
(imem . imemory)
(dmem . dmemory)
(latch1 . latch1-testing)
(latch2 . latch2-testing)))
(acl2s::register-type MA :enumerator nth-MA-testing :predicate MA-p)
(in-theory (disable pc-typep regp))
:set-ignore-ok t
(acl2s-defaults :set num-witnesses 0)
(acl2s-defaults :set num-counterexamples 1)
(acl2s-defaults :set testing-enabled T)
(acl2s-defaults :set search-strategy :incremental)
(acl2s-defaults :set use-fixers nil)
(in-theory (disable operation-codep ACL2::NON-NIL-IF-MGET-NON-NIL))
(acl2s-defaults :set sampling-method :random)
(acl2s-defaults :set backtrack-limit 1)
(in-theory (disable boolp))
(acl2s-defaults :set verbosity-level 2)
(acl2s-defaults :set num-trials 50)
(acl2s-defaults :set cgen-local-timeout 2)
(defthm cgen-support
(implies (and (registerp r)
(regp a1)
(regp a2))
(equal (mget a1 (mset a2 v r))
(if (not (equal a1 a2))
(mget a1 r)
v))))
(set-inhibit-warnings "invariant-risk")
(thm ;B-IS-A-WF-BISIM-CORE
(LET ((U (ISA-STEP S)) (V (MA-STEP W)))
(IMPLIES (AND
(ISA-P S)
(MA-P W)
(MA-testingp W)
(ISA-P U)
(MA-P V)
(WF-REL S W))
(OR (WF-REL U V)
(WF-REL S V)))))
|
