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 (* 0x00000080-0x00000FFF *) triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x8,x0〉〉〉 〈〈x0,xF〉:〈x8,x0〉〉 MEM_READ_WRITE (* 3968 GPR+RAM+STACK *)
39 (* 0x02000000-0x02003FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_WRITE (* 16384B PROGRAM RAM *)
40 (* 0x02010000-0x02013FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
41 (* 0x02014000-0x02017FFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x4,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
42 (* 0x02018000-0x0201BFFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈x8,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *)
43 (* 0x0201C000-0x0201FFFF *) ; triple … 〈〈〈x0,x2〉:〈x0,x1〉〉.〈〈xC,x0〉:〈x0,x0〉〉〉 〈〈x4,x0〉:〈x0,x0〉〉 MEM_READ_ONLY (* 16384B PROGRAM FLASH *) ]
47 (* punto di riferimento per accessi $FR, ($IP) ($DP) ($SP) *)
48 ndefinition IP2022_gpr_base ≝ 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉.
49 (* punto di riferimento per accessi ($PC) ($ADDR) *)
50 ndefinition IP2022_ram_base ≝ 〈〈〈x0,x2〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x0〉〉〉.
53 parametrizzati i non deterministici rispetto a tutti i valori casuali
54 che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
55 l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
56 (reset V-low), la memoria ed il check possono essere passati
58 ndefinition start_of_model_IP2022 ≝
59 λmcu:IP2022_model.λt:memory_impl.
60 λmem:aux_mem_type t.λchk:aux_chk_type t.
61 λndby1,ndby2:byte8.λirqfl,ndbo1,ndbo2,ndbo3,ndbo4,ndbo5:bool.
62 (mk_any_status IP2022 t
64 (* acc_low: reset *) 〈x0,x0〉
65 (* mulh: reset *) 〈x0,x0〉
66 (* addrsel: reset *) 〈x0,x0〉
67 (* addr: reset *) new_addrarray
68 (* call: reset *) new_callstack
69 (* ip: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
70 (* dp: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
71 (* data: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
72 (* sp: reset *) 〈〈x0,x0〉:〈x0,x0〉〉
73 (* pc: reset *) 〈〈xF,xF〉:〈xF,x0〉〉
79 (* skip mode: reset *) false)
82 (* clk: reset *) (None ?)).
85 cio' che non viene resettato mantiene il valore precedente: nella documentazione
86 viene riportato come "unaffected"/"indeterminate"/"unpredictable"
87 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 ?)).