1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "emulator/status/status.ma".
25 (* *********************************** *)
26 (* IMPOSTAZIONI SPECIFICHE DEI MODELLI *)
27 (* *********************************** *)
29 (* modelli di IP2022 *)
30 ninductive IP2022_model : Type ≝
33 (* memoria degli IP2022 *)
34 ndefinition memory_type_of_FamilyIP2022 ≝
35 λm:IP2022_model.match m with
38 (* mappato nel segmento 0 *)
39 (* 0x00000002-0x0000007F *) quadruple … o0 〈〈x0,x0〉:〈x0,x2〉〉 〈〈x0,x0〉:〈x7,xE〉〉 MEM_READ_ONLY (* 126B SystemMemoryReg *)
40 (* 0x00000080-0x00000FFF *) ; quadruple … o0 〈〈x0,x0〉:〈x8,x0〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 UserMemoryReg+RAM+STACK *)
41 (* tutto mappato nel segmento 1 *)
42 (* 0x02000000-0x02003FFF *) ; quadruple … o1 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_WRITE (* 16384B PROGRAM RAM *)
43 (* tutto mappato nel segmento 2 *)
44 (* 0x02010000-0x02013FFF *) ; quadruple … o2 〈〈x0,x0〉:〈x0,x0〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
45 (* 0x02014000-0x02017FFF *) ; quadruple … o2 〈〈x4,x0〉:〈x0,x0〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
46 (* 0x02018000-0x0201BFFF *) ; quadruple … o2 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
47 (* 0x0201C000-0x0201FFFF *) ; quadruple … o2 〈〈xC,x0〉:〈x0,x0〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *) ]
51 (* punto di riferimento per accessi $FR, ($IP) ($DP) ($SP) *)
52 ndefinition IP2022_gpr_base ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉.
53 (* punto di riferimento per accessi ($PC) ($ADDR) *)
54 ndefinition IP2022_ram_base ≝ 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉.
56 (* parametrizzati i non deterministici rispetto a tutti i valori casuali
57 che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
58 l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
59 (reset V-low), la memoria ed il check possono essere passati *)
60 ndefinition start_of_model_IP2022 ≝
61 λmcu:IP2022_model.λt:memory_impl.
62 λmem:aux_mem_type t.λchk:aux_chk_type t.
63 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
64 (mk_any_status IP2022 t
66 (* acc_low: reset *) 〈x0,x0〉
67 (* mulh: reset *) 〈x0,x0〉
68 (* addrsel: reset *) 〈x0,x0〉
69 (* addr: reset *) new_addrarray
70 (* call: reset *) new_callstack
71 (* ip: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
72 (* dp: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
73 (* data: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
74 (* sp: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
75 (* pc: reset *) 〈〈xF,xF〉:〈xF,x0〉〉
81 (* skip mode: reset *) false)
84 (* clk: reset *) (None ?)).
86 (* cio' che non viene resettato mantiene il valore precedente: nella documentazione
87 viene riportato come "unaffected"/"indeterminate"/"unpredictable"
88 il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
89 ndefinition reset_of_model_IP2022 ≝
90 λt:memory_impl.λs:any_status IP2022 t.
91 (mk_any_status IP2022 t
93 (* acc_low: reset *) 〈x0,x0〉
94 (* mulh: reset *) 〈x0,x0〉
95 (* addrsel: reset *) 〈x0,x0〉
96 (* addr: reset *) new_addrarray
97 (* call: reset *) new_callstack
98 (* ip: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
99 (* dp: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
100 (* data: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
101 (* sp: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
102 (* pc: reset *) 〈〈xF,xF〉:〈xF,x0〉〉
103 (* speed: reset *) x3
108 (* skip mode: reset *) false)
109 (* mem: inv. *) (mem_desc ? t s)
110 (* chk: inv. *) (chk_desc ? t s)
111 (* clk: reset *) (None ?)).