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/multivm/multivm_base.ma".
24 include "emulator/read_write/load_write.ma".
26 (* ************************************************ *)
27 (* LOGICHE AUSILIARE CHE ACCOMUNANO PIU' OPERAZIONI *)
28 (* ************************************************ *)
30 (* **************** *)
31 (* LOGICA DELLA ALU *)
32 (* **************** *)
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).
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 *)
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
102 (* istruzioni speciali per skip *)
103 ndefinition IP2022_check_skip ≝
104 λps:IP2022_pseudo.match ps with
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 ].