-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathInstance.v
168 lines (141 loc) · 4.38 KB
/
Instance.v
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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
(*
This script contains the extraction command used to translate the
RISC-V processor core model into Haskell, which is the first step
in generating the model's Verilog.
*)
Require Import Kami.All Kami.Compiler.Compiler Kami.Compiler.Rtl Kami.Compiler.UnverifiedIncompleteCompiler.
Require Import ProcKami.FU.
Require Import ProcKami.Pipeline.ProcessorCore.
Require Import ProcKami.MemOps.
Require Import List.
Import ListNotations.
Require Import ProcKami.ModelParams.
Require Import PeanoNat.
Import Nat.
Require Import StdLibKami.RegStruct.
Require Import Kami.Compiler.Test.
Require Import Kami.Simulator.NativeTest.
Require Import Kami.Simulator.CoqSim.Simulator.
Require Import Kami.Simulator.CoqSim.HaskellTypes.
Require Import Kami.Simulator.CoqSim.RegisterFile.
Require Import Kami.Simulator.CoqSim.Eval.
Require Import Kami.WfActionT.
Require Import Kami.SignatureMatch.
Require Import ProcKami.Devices.Uart.
Definition supportedExts
: list SupportedExt
:= [
Build_SupportedExt "I" true true ;
Build_SupportedExt "M" true true ;
Build_SupportedExt "A" true true ;
Build_SupportedExt "F" true true ;
Build_SupportedExt "D" true true ;
Build_SupportedExt "C" true true ;
Build_SupportedExt "S" true true ;
Build_SupportedExt "U" true true ;
Build_SupportedExt "Zicsr" true false ;
Build_SupportedExt "Zifencei" true false
].
Definition allow_misaligned := false.
Definition allow_inst_misaligned := true.
Definition misaligned_access := false.
Definition core (xlens : list nat) : Mod
:= generateCore
xlens
supportedExts
allow_misaligned
allow_inst_misaligned
misaligned_access
(_ 'h"1000").
Definition model (xlens : list nat) : Mod
:= generateModel
xlens
supportedExts
allow_misaligned
allow_inst_misaligned
misaligned_access
(_ 'h"1000").
Definition modelParams (xlens : list nat) : ProcParams
:= modelProcParams
xlens
supportedExts
allow_misaligned
allow_inst_misaligned
misaligned_access
(_ 'h"1000").
Definition core32 : Mod := core [Xlen32].
Definition core64 : Mod := core [Xlen32; Xlen64].
Definition model32 : Mod := model [Xlen32].
Definition model64 : Mod := model [Xlen32; Xlen64].
Definition model32Params := modelParams [Xlen32].
Definition model64Params := modelParams [Xlen32; Xlen64].
(* verify that the 32 bit model is compatible with TileLink. *)
Goal Nat.log2_up (length (@memOps model32Params)) <= (@TlFullSz model32Params).
Proof. cbv; lia. Qed.
(* verify that the 64 bit model is compatible with TileLink. *)
Goal Nat.log2_up (length (@memOps model64Params)) <= (@TlFullSz model64Params).
Proof. cbv; lia. Qed.
(** vm_compute should take ~40s *)
Lemma model64_wf : WfMod_unit model64 = [].
Proof.
vm_compute.
reflexivity.
Qed.
Lemma model32_wf : WfMod_unit model32 = [].
Proof.
vm_compute.
reflexivity.
Qed.
Lemma model64_sf : SigMatch_Mod model64 = [].
Proof.
vm_compute.
reflexivity.
Qed.
Lemma model32_sf : SigMatch_Mod model32 = [].
Proof.
vm_compute.
reflexivity.
Qed.
Axiom cheat : forall {X},X.
Definition basemod32 := let '(_,(_,basemod)) := separateModRemove model32 in basemod.
Definition basemod64 := let '(_,(_,basemod)) := separateModRemove model64 in basemod.
Definition rules_32 : list (evaluated_Rule (getRegisters basemod32)) := map (fun r => eval_Rule r cheat) (getRules basemod32).
Definition rules_64 : list (evaluated_Rule (getRegisters basemod64)) := map (fun r => eval_Rule r cheat) (getRules basemod64).
Separate Extraction
predPack
orKind
predPackOr
createWriteRq
createWriteRqMask
pointwiseIntersectionNoMask
pointwiseIntersectionMask
pointwiseIntersection
pointwiseBypass
getDefaultConstFullKind
CAS_RulesRf
Fin_to_list
getCallsWithSignPerMod
RtlExpr'
getRtl
CompActionSimple
RmeSimple
RtlModule
getRules
separateModRemove
separateModHidesNoInline
core32
core64
model32
model64
rules_32
rules_64
testReg
testAsync
testSyncIsAddr
testSyncNotIsAddr
testNative
print_Val2
init_state
sim_step
initialize_files_zero
.