]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly2/emulator/multivm/IP2022_multivm.ma
freescale porting
[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / multivm / IP2022_multivm.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "emulator/multivm/multivm_base.ma".
24 include "emulator/read_write/load_write.ma".
25
26 (* ************************************************ *)
27 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
28 (* ************************************************ *)
29
30 (* **************** *)
31 (* LOGICA DELLA ALU *)
32 (* **************** *)
33
34 ndefinition execute_NO ≝
35 λm:mcu_type.λt:memory_impl.λs:any_status m t.λcur_pc:word16.λi:aux_im_type m.
36  None (ProdT (any_status m t) word16).
37
38 (* raccordo *)
39 ndefinition IP2022_execute_any ≝
40 λps:IP2022_pseudo.match ps with
41   [ ADD    ⇒ execute_NO (* add *)
42   | ADDC   ⇒ execute_NO (* add with carry *)
43   | AND    ⇒ execute_NO (* and *)
44   | BREAK  ⇒ execute_NO (* enter break mode *)
45   | BREAKX ⇒ execute_NO (* enter break mode, after skip *)
46   | CALL   ⇒ execute_NO (* subroutine call *)
47   | CLR    ⇒ execute_NO (* clear *)
48   | CLRB   ⇒ execute_NO (* clear bit *)
49   | CMP    ⇒ execute_NO (* set flags according to sub *)
50   | CSE    ⇒ execute_NO (* confront & skip if equal *)
51   | CSNE   ⇒ execute_NO (* confront & skip if not equal *)
52   | CWDT   ⇒ execute_NO (* clear watch dog -- not impl. ERR *)
53   | DEC    ⇒ execute_NO (* decrement *)
54   | DECSNZ ⇒ execute_NO (* decrement & skip if not zero *)
55   | DECSZ  ⇒ execute_NO (* decrement & skip if zero *)
56   | FERASE ⇒ execute_NO (* flash erase -- not impl. ERR *)
57   | FREAD  ⇒ execute_NO (* flash read -- not impl. ERR *)
58   | FWRITE ⇒ execute_NO (* flash write -- not impl. ERR *)
59   | INC    ⇒ execute_NO (* increment *)
60   | INCSNZ ⇒ execute_NO (* increment & skip if not zero *)
61   | INCSZ  ⇒ execute_NO (* increment & skip if zero *)
62   | INT    ⇒ execute_NO (* interrupt -- not impl. ERR *)
63   | IREAD  ⇒ execute_NO (* memory read *)
64   | IWRITE ⇒ execute_NO (* memory write *)
65   | JMP    ⇒ execute_NO (* jump *)
66   | LOADH  ⇒ execute_NO (* load Data Pointer High *)
67   | LOADL  ⇒ execute_NO (* load Data Pointer Low *)
68   | MOV    ⇒ execute_NO (* move *)
69   | MULS   ⇒ execute_NO (* signed mul *)
70   | MULU   ⇒ execute_NO (* unsigned mul *)
71   | NOP    ⇒ execute_NO (* nop *)
72   | NOT    ⇒ execute_NO (* not *)
73   | OR     ⇒ execute_NO (* or *)
74   | PAGE   ⇒ execute_NO (* set Page Register *)
75   | POP    ⇒ execute_NO (* pop *)
76   | PUSH   ⇒ execute_NO (* push *)
77   | RET    ⇒ execute_NO (* subroutine ret *)
78   | RETI   ⇒ execute_NO (* interrupt ret -- not impl. ERR *)
79   | RETNP  ⇒ execute_NO (* subroutine ret & don't restore Page Register *)
80   | RETW   ⇒ execute_NO (* subroutine ret & load W Register *)
81   | RL     ⇒ execute_NO (* rotate left *)
82   | RR     ⇒ execute_NO (* rotate right *)
83   | SB     ⇒ execute_NO (* skip if bit set *)
84   | SETB   ⇒ execute_NO (* set bit *)
85   | SNB    ⇒ execute_NO (* skip if bit not set *)
86   | SPEED  ⇒ execute_NO (* set Speed Register *)
87   | SUB    ⇒ execute_NO (* sub *)
88   | SUBC   ⇒ execute_NO (* sub with carry *)
89   | SWAP   ⇒ execute_NO (* swap xxxxyyyy → yyyyxxxx *)
90   | TEST   ⇒ execute_NO (* set flags according to zero test *)
91   | XOR    ⇒ execute_NO (* xor *)
92   ].
93
94 (* stati speciali di esecuzione *)
95 ndefinition IP2022_check_susp ≝
96 λps:IP2022_pseudo.match ps with
97  [ BREAK ⇒ Some ? BGND_MODE
98  | BREAKX ⇒ Some ? BGND_MODE
99  | _ ⇒ None ?
100  ].
101
102 (* istruzioni speciali per skip *)
103 ndefinition IP2022_check_skip ≝
104 λps:IP2022_pseudo.match ps with
105  [ LOADH ⇒ true
106  | LOADL ⇒ true
107  | PAGE ⇒ true
108  | _ ⇒ false
109  ].
110
111 (* motiplicatore del ciclo di durata *)
112 ndefinition IP2022_clk_mult ≝
113 λt.λs:any_status IP2022 t.
114  (* divisore del clock, 0 = stop *)
115  match speed_reg_IP2022 … (alu … s) with
116   [ x0 ⇒ nat1  | x1 ⇒ nat2  | x2 ⇒ nat3   | x3 ⇒ nat4
117   | x4 ⇒ nat5  | x5 ⇒ nat6  | x6 ⇒ nat8   | x7 ⇒ nat10
118   | x8 ⇒ nat12 | x9 ⇒ nat16 | xA ⇒ nat24  | xB ⇒ nat32
119   | xC ⇒ nat48 | xD ⇒ nat64 | xE ⇒ nat128 | xF ⇒ O ] *
120  (* FLASH clock 120MHz, RAM clock 40MHz *)
121  match IP2022_pc_flashtest (get_pc_reg … s) with
122   [ true ⇒ nat3 | false ⇒ nat1 ].