+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(* Progetto FreeScale *)
-(* *)
-(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Sviluppo: 2008-2010 *)
-(* *)
-(* ********************************************************************** *)
-
-include "num/bool.ma".
-
-(* ********************************************** *)
-(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
-(* ********************************************** *)
-
-(* enumerazione delle istruzioni *)
-ninductive IP2022_opcode: Type ≝
- ADD : IP2022_opcode (* add *)
-| ADDC : IP2022_opcode (* add with carry *)
-| AND : IP2022_opcode (* and *)
-| BREAK : IP2022_opcode (* enter break mode *)
-| BREAKX : IP2022_opcode (* enter break mode, after skip *)
-| CALL : IP2022_opcode (* subroutine call *)
-| CLR : IP2022_opcode (* clear *)
-| CLRB : IP2022_opcode (* clear bit *)
-| CMP : IP2022_opcode (* set flags according to sub *)
-| CSE : IP2022_opcode (* confront & skip if equal *)
-| CSNE : IP2022_opcode (* confront & skip if not equal *)
-| CWDT : IP2022_opcode (* clear watch dog -- not impl. ERR *)
-| DEC : IP2022_opcode (* decrement *)
-| DECSNZ : IP2022_opcode (* decrement & skip if not zero *)
-| DECSZ : IP2022_opcode (* decrement & skip if zero *)
-| FERASE : IP2022_opcode (* flash erase -- not impl. ERR *)
-| FREAD : IP2022_opcode (* flash read -- not impl. ERR *)
-| FWRITE : IP2022_opcode (* flash write -- not impl. ERR *)
-| INC : IP2022_opcode (* increment *)
-| INCSNZ : IP2022_opcode (* increment & skip if not zero *)
-| INCSZ : IP2022_opcode (* increment & skip if zero *)
-| INT : IP2022_opcode (* interrupt -- not impl. ERR *)
-| IREAD : IP2022_opcode (* memory read *)
-| IREADI : IP2022_opcode (* memory read & inc *)
-| IWRITE : IP2022_opcode (* memory write *)
-| IWRITEI : IP2022_opcode (* memory write & inc *)
-| JMP : IP2022_opcode (* jump *)
-| LOADH : IP2022_opcode (* load Data Pointer High *)
-| LOADL : IP2022_opcode (* load Data Pointer Low *)
-| MOV : IP2022_opcode (* move *)
-| MULS : IP2022_opcode (* signed mul *)
-| MULU : IP2022_opcode (* unsigned mul *)
-| NOP : IP2022_opcode (* nop *)
-| NOT : IP2022_opcode (* not *)
-| OR : IP2022_opcode (* or *)
-| PAGE : IP2022_opcode (* set Page Register *)
-| POP : IP2022_opcode (* pop *)
-| PUSH : IP2022_opcode (* push *)
-| RET : IP2022_opcode (* subroutine ret *)
-| RETI : IP2022_opcode (* interrupt ret -- not impl. ERR *)
-| RETNP : IP2022_opcode (* subroutine ret & don't restore Page Register *)
-| RETW : IP2022_opcode (* subroutine ret & load W Register *)
-| RL : IP2022_opcode (* rotate left *)
-| RR : IP2022_opcode (* rotate right *)
-| SB : IP2022_opcode (* skip if bit set *)
-| SETB : IP2022_opcode (* set bit *)
-| SNB : IP2022_opcode (* skip if bit not set *)
-| SPEED : IP2022_opcode (* set Speed Register *)
-| SUB : IP2022_opcode (* sub *)
-| SUBC : IP2022_opcode (* sub with carry *)
-| SWAP : IP2022_opcode (* swap xxxxyyyy → yyyyxxxx *)
-| TEST : IP2022_opcode (* set flags according to zero test *)
-| XOR : IP2022_opcode (* xor *)
-.
-
-ndefinition eq_IP2022_op ≝
-λop1,op2:IP2022_opcode.
- match op1 with
- [ ADD ⇒ match op2 with [ ADD ⇒ true | _ ⇒ false ] | ADDC ⇒ match op2 with [ ADDC ⇒ true | _ ⇒ false ]
- | AND ⇒ match op2 with [ AND ⇒ true | _ ⇒ false ] | BREAK ⇒ match op2 with [ BREAK ⇒ true | _ ⇒ false ]
- | BREAKX ⇒ match op2 with [ BREAKX ⇒ true | _ ⇒ false ] | CALL ⇒ match op2 with [ CALL ⇒ true | _ ⇒ false ]
- | CLR ⇒ match op2 with [ CLR ⇒ true | _ ⇒ false ] | CLRB ⇒ match op2 with [ CLRB ⇒ true | _ ⇒ false ]
- | CMP ⇒ match op2 with [ CMP ⇒ true | _ ⇒ false ] | CSE ⇒ match op2 with [ CSE ⇒ true | _ ⇒ false ]
- | CSNE ⇒ match op2 with [ CSNE ⇒ true | _ ⇒ false ] | CWDT ⇒ match op2 with [ CWDT ⇒ true | _ ⇒ false ]
- | DEC ⇒ match op2 with [ DEC ⇒ true | _ ⇒ false ] | DECSNZ ⇒ match op2 with [ DECSNZ ⇒ true | _ ⇒ false ]
- | DECSZ ⇒ match op2 with [ DECSZ ⇒ true | _ ⇒ false ] | FERASE ⇒ match op2 with [ FERASE ⇒ true | _ ⇒ false ]
- | FREAD ⇒ match op2 with [ FREAD ⇒ true | _ ⇒ false ] | FWRITE ⇒ match op2 with [ FWRITE ⇒ true | _ ⇒ false ]
- | INC ⇒ match op2 with [ INC ⇒ true | _ ⇒ false ] | INCSNZ ⇒ match op2 with [ INCSNZ ⇒ true | _ ⇒ false ]
- | INCSZ ⇒ match op2 with [ INCSZ ⇒ true | _ ⇒ false ] | INT ⇒ match op2 with [ INT ⇒ true | _ ⇒ false ]
- | IREAD ⇒ match op2 with [ IREAD ⇒ true | _ ⇒ false ] | IREADI ⇒ match op2 with [ IREADI ⇒ true | _ ⇒ false ]
- | IWRITE ⇒ match op2 with [ IWRITE ⇒ true | _ ⇒ false ] | IWRITEI ⇒ match op2 with [ IWRITEI ⇒ true | _ ⇒ false ]
- | JMP ⇒ match op2 with [ JMP ⇒ true | _ ⇒ false ] | LOADH ⇒ match op2 with [ LOADH ⇒ true | _ ⇒ false ]
- | LOADL ⇒ match op2 with [ LOADL ⇒ true | _ ⇒ false ] | MOV ⇒ match op2 with [ MOV ⇒ true | _ ⇒ false ]
- | MULS ⇒ match op2 with [ MULS ⇒ true | _ ⇒ false ] | MULU ⇒ match op2 with [ MULU ⇒ true | _ ⇒ false ]
- | NOP ⇒ match op2 with [ NOP ⇒ true | _ ⇒ false ] | NOT ⇒ match op2 with [ NOT ⇒ true | _ ⇒ false ]
- | OR ⇒ match op2 with [ OR ⇒ true | _ ⇒ false ] | PAGE ⇒ match op2 with [ PAGE ⇒ true | _ ⇒ false ]
- | POP ⇒ match op2 with [ POP ⇒ true | _ ⇒ false ] | PUSH ⇒ match op2 with [ PUSH ⇒ true | _ ⇒ false ]
- | RET ⇒ match op2 with [ RET ⇒ true | _ ⇒ false ] | RETI ⇒ match op2 with [ RETI ⇒ true | _ ⇒ false ]
- | RETNP ⇒ match op2 with [ RETNP ⇒ true | _ ⇒ false ] | RETW ⇒ match op2 with [ RETW ⇒ true | _ ⇒ false ]
- | RL ⇒ match op2 with [ RL ⇒ true | _ ⇒ false ] | RR ⇒ match op2 with [ RR ⇒ true | _ ⇒ false ]
- | SB ⇒ match op2 with [ SB ⇒ true | _ ⇒ false ] | SETB ⇒ match op2 with [ SETB ⇒ true | _ ⇒ false ]
- | SNB ⇒ match op2 with [ SNB ⇒ true | _ ⇒ false ] | SPEED ⇒ match op2 with [ SPEED ⇒ true | _ ⇒ false ]
- | SUB ⇒ match op2 with [ SUB ⇒ true | _ ⇒ false ] | SUBC ⇒ match op2 with [ SUBC ⇒ true | _ ⇒ false ]
- | SWAP ⇒ match op2 with [ SWAP ⇒ true | _ ⇒ false ] | TEST ⇒ match op2 with [ TEST ⇒ true | _ ⇒ false ]
- | XOR ⇒ match op2 with [ XOR ⇒ true | _ ⇒ false ]
- ].
-
-(* iteratore sugli opcode *)
-ndefinition forall_IP2022_op ≝ λP:IP2022_opcode → bool.
- P ADD ⊗ P ADDC ⊗ P AND ⊗ P BREAK ⊗ P BREAKX ⊗ P CALL ⊗ P CLR ⊗ P CLRB ⊗
- P CMP ⊗ P CSE ⊗ P CSNE ⊗ P CWDT ⊗ P DEC ⊗ P DECSNZ ⊗ P DECSZ ⊗ P FERASE ⊗
- P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IREADI ⊗
- P IWRITE ⊗ P IWRITEI ⊗ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗
- P NOP ⊗ P NOT ⊗ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗
- P RETNP ⊗ P RETW ⊗ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗
- P SUB ⊗ P SUBC ⊗ P SWAP ⊗ P TEST ⊗ P XOR.
projects / helm.git / blobdiff