Theory Sparc_Types

(*
 * Copyright 2016, NTU
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * Author: Zhe Hou, David Sanan. 
 *)

section ‹SPARC V8 architecture CPU model›
theory Sparc_Types    
imports Main "../lib/WordDecl" "Word_Lib.Bit_Shifts_Infix_Syntax"
begin

text ‹The following type definitions are taken from David Sanan's 
definitions for SPARC machines.›

type_synonym machine_word = word32
type_synonym byte = word8
type_synonym phys_address = word36

type_synonym virtua_address = word32
type_synonym page_address = word24
type_synonym offset = word12

type_synonym table_entry = word8

definition page_size :: "word32" where "page_size ≡ 4096"

type_synonym virtua_page_address = word20
type_synonym context_type = word8

type_synonym word_length_t1 = word_length8
type_synonym word_length_t2 = word_length6
type_synonym word_length_t3 = word_length6
type_synonym word_length_offset = word_length12
type_synonym word_length_page = word_length24
type_synonym word_length_phys_address = word_length36
type_synonym word_length_virtua_address = word_length32
type_synonym word_length_entry_type = word_length2
type_synonym word_length_machine_word = word_length32

definition length_machine_word :: "nat" 
 where "length_machine_word ≡ LENGTH(word_length_machine_word)"

text_raw ‹\newpage›

section ‹CPU Register Definitions›

text‹
 The definitions below come from the SPARC Architecture Manual, Version 8.
 The LEON3 processor has been certified SPARC V8 conformant (2005).
›

definition leon3khz ::"word32"
where
"leon3khz ≡ 33000"

text ‹The following type definitions for MMU is taken from 
David Sanan's definitions for MMU.›

text‹
  The definitions below come from the UT699 LEON 3FT/SPARC V8 Microprocessor Functional Manual, 
   Aeroflex, June 20, 2012, p35.
›
datatype MMU_register
 = CR    ― ‹Control Register›
 | CTP   ― ‹ConText Pointer register›
 | CNR   ― ‹Context Register›
 | FTSR   ― ‹Fault Status Register›
 | FAR   ― ‹Fault Address Register›

lemma MMU_register_induct: 
  "P CR ⟹ P CTP ⟹ P CNR ⟹ P FTSR ⟹ P FAR 
   ⟹ P x"
  by (cases x) auto

lemma UNIV_MMU_register [no_atp]: "UNIV = {CR, CTP, CNR, FTSR, FAR}"
   apply (safe)
   apply (case_tac x)
   apply (auto intro:MMU_register_induct)
  done


instantiation MMU_register :: enum begin

definition "enum_MMU_register = [ CR, CTP, CNR, FTSR, FAR ]"

definition
  "enum_all_MMU_register P ⟷ P CR ∧ P CTP ∧ P CNR ∧ P FTSR ∧ P FAR "
definition
  "enum_ex_MMU_register P ⟷ P CR ∨ P CTP ∨ P CNR ∨ P FTSR ∨ P FAR"

 instance proof
  qed (simp_all only: enum_MMU_register_def enum_all_MMU_register_def 
                      enum_ex_MMU_register_def UNIV_MMU_register, simp_all)
end
type_synonym MMU_context = "MMU_register ⇒ machine_word"

text ‹‹PTE_flags› is the last 8 bits of a PTE. See page 242 of SPARCv8 manual.
▪ C - bit 7
▪ M - bit 6,
▪ R - bit 5
▪ ACC - bit 4~2
▪ ET - bit 1~0.›

type_synonym PTE_flags = word8

text ‹
  @{term CPU_register} datatype is an enumeration with the CPU registers defined in the SPARC V8 
  architecture.
›
datatype CPU_register = 
   PSR   ― ‹Processor State Register›
 | WIM   ― ‹Window Invalid Mask›
 | TBR   ― ‹Trap Base Register›
 | Y     ― ‹Multiply/Divide Register›
 | PC    ― ‹Program Counter›
 | nPC   ― ‹next Program Counter›
 | DTQ   ― ‹Deferred-Trap Queue›
 | FSR   ― ‹Floating-Point State Register›
 | FQ    ― ‹Floating-Point Deferred-Trap Queue›
 | CSR   ― ‹Coprocessor State Register›
 | CQ    ― ‹Coprocessor Deferred-Trap Queue›
 (*| CCR   --   "Cache Control Register"*)
 | ASR "word5"  ― ‹Ancillary State Register›

text ‹The following two functions are dummies since we will not use 
        ASRs. Future formalisation may add more details to this.›

context
  includes bit_operations_syntax
begin

definition privileged_ASR :: "word5 ⇒ bool"
where
"privileged_ASR r ≡ False
"

definition illegal_instruction_ASR :: "word5 ⇒ bool"
where
"illegal_instruction_ASR r ≡ False
"

definition get_tt :: "word32 ⇒ word8"
where
"get_tt tbr ≡
  ucast (((AND) tbr 0b00000000000000000000111111110000) >> 4)
"

text ‹Write the tt field of the TBR register. 
        Return the new value of TBR.›
definition write_tt :: "word8 ⇒ word32 ⇒ word32"
where
"write_tt new_tt_val tbr_val ≡
  let tmp = (AND) tbr_val 0b111111111111111111111000000001111 in
      (OR) tmp (((ucast new_tt_val)::word32) << 4)
"

text ‹Get the nth bit of WIM. This equals ((AND) WIM $2^n$). 
        N.B. the first bit of WIM is the 0th bit.›
definition get_WIM_bit :: "nat ⇒ word32 ⇒ word1"
where
"get_WIM_bit n wim ≡
  let mask = ((ucast (0b1::word1))::word32) << n in
  ucast (((AND) mask wim) >> n)
"

definition get_CWP :: "word32 ⇒ word5"
where
"get_CWP psr ≡ 
  ucast ((AND) psr 0b00000000000000000000000000011111) 
"

definition get_ET :: "word32 ⇒ word1"
where
"get_ET psr ≡ 
  ucast (((AND) psr 0b00000000000000000000000000100000) >> 5) 
"

definition get_PIL :: "word32 ⇒ word4"
where
"get_PIL psr ≡ 
  ucast (((AND) psr 0b00000000000000000000111100000000) >> 8) 
"

definition get_PS :: "word32 ⇒ word1"
where
"get_PS psr ≡ 
  ucast (((AND) psr 0b00000000000000000000000001000000) >> 6) 
"

definition get_S :: "word32 ⇒ word1"
where
"get_S psr ≡ 
  ⌦‹ucast (((AND) psr 0b00000000000000000000000010000000) >> 7)›
  if ((AND) psr (0b00000000000000000000000010000000::word32)) = 0 then 0
  else 1
"

definition get_icc_N :: "word32 ⇒ word1"
where
"get_icc_N psr ≡
  ucast (((AND) psr 0b00000000100000000000000000000000) >> 23)
"

definition get_icc_Z :: "word32 ⇒ word1"
where
"get_icc_Z psr ≡
  ucast (((AND) psr 0b00000000010000000000000000000000) >> 22)
"

definition get_icc_V :: "word32 ⇒ word1"
where
"get_icc_V psr ≡
  ucast (((AND) psr 0b00000000001000000000000000000000) >> 21)
"

definition get_icc_C :: "word32 ⇒ word1"
where
"get_icc_C psr ≡
  ucast (((AND) psr 0b00000000000100000000000000000000) >> 20)
"

definition update_S :: "word1 ⇒ word32 ⇒ word32"
where
"update_S s_val psr_val ≡
  let tmp0 = (AND) psr_val 0b11111111111111111111111101111111 in
  (OR) tmp0 (((ucast s_val)::word32) << 7)
"

text ‹Update the CWP field of PSR. 
        Return the new value of PSR.›
definition update_CWP :: "word5 ⇒ word32 ⇒ word32"
where
"update_CWP cwp_val psr_val ≡
  let tmp0 = (AND) psr_val (0b11111111111111111111111111100000::word32);
      s_val = ((ucast (get_S psr_val))::word1)
  in
  if s_val = 0 then  
    (AND) ((OR) tmp0 ((ucast cwp_val)::word32)) (0b11111111111111111111111101111111::word32)
  else
    (OR) ((OR) tmp0 ((ucast cwp_val)::word32)) (0b00000000000000000000000010000000::word32)
"

text ‹Update the the ET, CWP, and S fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_rett :: "word5 ⇒ word1 ⇒ word1 ⇒ word32 ⇒ word32"
where
"update_PSR_rett cwp_val et_val s_val psr_val ≡
  let tmp0 = (AND) psr_val 0b11111111111111111111111101000000;
      tmp1 = (OR) tmp0 ((ucast cwp_val)::word32);
      tmp2 = (OR) tmp1 (((ucast et_val)::word32) << 5); 
      tmp3 = (OR) tmp2 (((ucast s_val)::word32) << 7)
  in  
  tmp3
"

definition update_PSR_exe_trap :: "word5 ⇒ word1 ⇒ word1 ⇒ word32 ⇒ word32"
where
"update_PSR_exe_trap cwp_val et_val ps_val psr_val ≡
  let tmp0 = (AND) psr_val 0b11111111111111111111111110000000;
      tmp1 = (OR) tmp0 ((ucast cwp_val)::word32);
      tmp2 = (OR) tmp1 (((ucast et_val)::word32) << 5); 
      tmp3 = (OR) tmp2 (((ucast ps_val)::word32) << 6)
  in  
  tmp3
"

text ‹Update the N, Z, V, C fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_icc :: "word1 ⇒ word1 ⇒ word1 ⇒ word1 ⇒ word32 ⇒ word32"
where
"update_PSR_icc n_val z_val v_val c_val psr_val ≡
  let
      n_val_32 = if n_val = 0 then 0 
                 else       (0b00000000100000000000000000000000::word32); 
      z_val_32 = if z_val = 0 then 0 
                 else       (0b00000000010000000000000000000000::word32); 
      v_val_32 = if v_val = 0 then 0 
                 else       (0b00000000001000000000000000000000::word32);
      c_val_32 = if c_val = 0 then 0 
                 else       (0b00000000000100000000000000000000::word32);
      tmp0 = (AND) psr_val (0b11111111000011111111111111111111::word32);
      tmp1 = (OR) tmp0 n_val_32;
      tmp2 = (OR) tmp1 z_val_32;
      tmp3 = (OR) tmp2 v_val_32;
      tmp4 = (OR) tmp3 c_val_32
  in
  tmp4
"

text ‹Update the ET, PIL fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_et_pil :: "word1 ⇒ word4 ⇒ word32 ⇒ word32"
where
"update_PSR_et_pil et pil psr_val ≡
  let tmp0 = (AND) psr_val 0b111111111111111111111000011011111;
      tmp1 = (OR) tmp0 (((ucast et)::word32) << 5);
      tmp2 = (OR) tmp1 (((ucast pil)::word32) << 8)
  in
  tmp2
"

end

text ‹
   SPARC V8 architecture is organized in windows of 32 user registers.
   The data stored in a register is defined as a 32 bits word @{term reg_type}:
›
type_synonym reg_type = "word32"

text ‹
  The access to the value of a CPU register of type @{term CPU_register} is
  defined by a total function @{term cpu_context}
›

type_synonym cpu_context = "CPU_register ⇒ reg_type"

text ‹
  User registers are defined with the type @{term user_reg} represented by a 5 bits word.
›

type_synonym user_reg_type = "word5"

definition PSR_S ::"reg_type"
where "PSR_S ≡ 6"
text ‹
  Each window context is defined by a total function @{term window_context} from @{term user_register} 
  to @{term reg_type} (32 bits word storing the actual value of the register).
›

type_synonym window_context = "user_reg_type ⇒ reg_type"
text ‹
  The number of windows is implementation dependent. 
  The LEON architecture is composed of 16 different windows (a 4 bits word).
›

definition NWINDOWS :: "int"
where "NWINDOWS ≡ 8"

text ‹Maximum number of windows is 32 in SPARCv8.›
type_synonym ('a) window_size = "'a word"

text ‹
Finally the user context is defined by another total function @{term user_context} from 
@{term window_size} to @{term window_context}. That is, the user context is a function taking as
argument a register set window and a register within that window, and it returns the value stored
in that user register.
›
type_synonym ('a) user_context = "('a) window_size ⇒ window_context"

datatype sys_reg = 
         CCR    ― ‹Cache control register›
        |ICCR   ― ‹Instruction cache configuration register›
        |DCCR   ― ‹Data cache configuration register›

type_synonym sys_context = "sys_reg ⇒ reg_type"

text‹
The memory model is defined by a total function from 32 bits words to 8 bits words
›
type_synonym asi_type = "word8"

text ‹
 The memory is defined as a function from page address to page, which is also defined
  as a function from physical address to @{term "machine_word"}
›

type_synonym mem_val_type = "word8"
type_synonym mem_context = "asi_type ⇒ phys_address ⇒ mem_val_type option"

type_synonym cache_tag = "word20"
type_synonym cache_line_size = "word12"
type_synonym cache_type = "(cache_tag × cache_line_size)"
type_synonym cache_context = "cache_type ⇒ mem_val_type option"

text ‹The delayed-write pool generated from write state register instructions.›
type_synonym delayed_write_pool = "(int × reg_type × CPU_register) list"

definition DELAYNUM :: "int"
where "DELAYNUM ≡ 0"

text ‹Convert a set to a list.›
definition list_of_set :: "'a set ⇒ 'a list"
  where "list_of_set s = (SOME l. set l = s)"

lemma set_list_of_set: "finite s ⟹ set (list_of_set s) = s"
unfolding list_of_set_def 
by (metis (mono_tags) finite_list some_eq_ex)

type_synonym ANNUL = "bool"
type_synonym RESET_TRAP = "bool"
type_synonym EXECUTE_MODE = "bool"
type_synonym RESET_MODE = "bool"
type_synonym ERROR_MODE = "bool"
type_synonym TICC_TRAP_TYPE = "word7"
type_synonym INTERRUPT_LEVEL = "word3"
type_synonym STORE_BARRIER_PENDING = "bool"

text ‹The processor asserts this signal to ensure that the
memory system will not process another SWAP or
LDSTUB operation to the same memory byte.›
type_synonym pb_block_ldst_byte = "virtua_address ⇒ bool"

text‹The processor asserts this signal to ensure that the
memory system will not process another SWAP or
LDSTUB operation to the same memory word.›
type_synonym pb_block_ldst_word = "virtua_address ⇒ bool"

record sparc_state_var =
annul:: ANNUL
resett:: RESET_TRAP
exe:: EXECUTE_MODE
reset:: RESET_MODE
err:: ERROR_MODE
ticc:: TICC_TRAP_TYPE
itrpt_lvl:: INTERRUPT_LEVEL
st_bar:: STORE_BARRIER_PENDING
atm_ldst_byte:: pb_block_ldst_byte
atm_ldst_word:: pb_block_ldst_word

definition get_annul :: "sparc_state_var ⇒ bool"
where "get_annul v ≡ annul v"

definition get_reset_trap :: "sparc_state_var ⇒ bool"
where "get_reset_trap v ≡ resett v"

definition get_exe_mode :: "sparc_state_var ⇒ bool"
where "get_exe_mode v ≡ exe v"

definition get_reset_mode :: "sparc_state_var ⇒ bool"
where "get_reset_mode v ≡ reset v"

definition get_err_mode :: "sparc_state_var ⇒ bool"
where "get_err_mode v ≡ err v"

definition get_ticc_trap_type :: "sparc_state_var ⇒ word7"
where "get_ticc_trap_type v ≡ ticc v"

definition get_interrupt_level :: "sparc_state_var ⇒ word3"
where "get_interrupt_level v ≡ itrpt_lvl v"

definition get_store_barrier_pending :: "sparc_state_var ⇒ bool"
where "get_store_barrier_pending v ≡ st_bar v"

definition write_annul :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_annul b v ≡ v⦇annul := b⦈"

definition write_reset_trap :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_reset_trap b v ≡ v⦇resett := b⦈"

definition write_exe_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_exe_mode b v ≡ v⦇exe := b⦈"

definition write_reset_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_reset_mode b v ≡ v⦇reset := b⦈"

definition write_err_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_err_mode b v ≡ v⦇err := b⦈"

definition write_ticc_trap_type :: "word7 ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_ticc_trap_type w v ≡ v⦇ticc := w⦈"

definition write_interrupt_level :: "word3 ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_interrupt_level w v ≡ v⦇itrpt_lvl := w⦈"

definition write_store_barrier_pending :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_store_barrier_pending b v ≡ v⦇st_bar := b⦈"

context
  includes bit_operations_syntax
begin

text ‹Given a word7 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext7::"word7 ⇒ word32"
where
"sign_ext7 w ≡ 
  let highest_bit = ((AND) w 0b1000000) >> 6 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111111111110000000
"

definition zero_ext8 :: "word8 ⇒ word32"
where
"zero_ext8 w ≡ (ucast w)::word32
"

text ‹Given a word8 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext8::"word8 ⇒ word32"
where
"sign_ext8 w ≡ 
  let highest_bit = ((AND) w 0b10000000) >> 7 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111111111100000000
"

text ‹Given a word13 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext13::"word13 ⇒ word32"
where
"sign_ext13 w ≡ 
  let highest_bit = ((AND) w 0b1000000000000) >> 12 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111110000000000000
"

definition zero_ext16 :: "word16 ⇒ word32"
where
"zero_ext16 w ≡ (ucast w)::word32
"

text ‹Given a word16 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext16::"word16 ⇒ word32"
where
"sign_ext16 w ≡ 
  let highest_bit = ((AND) w 0b1000000000000000) >> 15 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111110000000000000000
"

text ‹Given a word22 value, find the highest bit,
        and fill the left bits to tbe the highest bit.›
definition sign_ext22::"word22 ⇒ word32"
where
"sign_ext22 w ≡
  let highest_bit = ((AND) w 0b1000000000000000000000) >> 21 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111110000000000000000000000
"

text ‹Given a word24 value, find the highest bit,
        and fill the left bits to tbe the highest bit.›
definition sign_ext24::"word24 ⇒ word32"
where
"sign_ext24 w ≡
  let highest_bit = ((AND) w 0b100000000000000000000000) >> 23 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111000000000000000000000000
"

text‹
Operations to be defined.
The SPARC V8 architecture is composed of the following set of instructions:
  ▪ Load Integer Instructions
  ▪ Load Floating-point Instructions
  ▪ Load Coprocessor Instructions
  ▪ Store Integer Instructions
  ▪ Store Floating-point Instructions
  ▪ Store Coprocessor Instructions
  ▪ Atomic Load-Store Unsigned Byte Instructions
  ▪ SWAP Register With Memory Instruction
  ▪ SETHI Instructions
  ▪ NOP Instruction
  ▪ Logical Instructions
  ▪ Shift Instructions
  ▪ Add Instructions
  ▪ Tagged Add Instructions
  ▪ Subtract Instructions
  ▪ Tagged Subtract Instructions
  ▪ Multiply Step Instruction
  ▪ Multiply Instructions
  ▪ Divide Instructions
  ▪ SAVE and RESTORE Instructions
  ▪ Branch on Integer Condition Codes Instructions
  ▪ Branch on Floating-point Condition Codes Instructions
  ▪ Branch on Coprocessor Condition Codes Instructions
  ▪ Call and Link Instruction
  ▪ Jump and Link Instruction
  ▪ Return from Trap Instruction
  ▪ Trap on Integer Condition Codes Instructions
  ▪ Read State Register Instructions
  ▪ Write State Register Instructions
  ▪ STBAR Instruction
  ▪ Unimplemented Instruction
  ▪ Flush Instruction Memory
  ▪ Floating-point Operate (FPop) Instructions
  ▪ Convert Integer to Floating point Instructions
  ▪ Convert Floating point to Integer Instructions
  ▪ Convert Between Floating-point Formats Instructions
  ▪ Floating-point Move Instructions
  ▪ Floating-point Square Root Instructions
  ▪ Floating-point Add and Subtract Instructions
  ▪ Floating-point Multiply and Divide Instructions
  ▪ Floating-point Compare Instructions
  ▪ Coprocessor Operate Instructions
›

text ‹The CALL instruction.›
datatype call_type = CALL ― ‹Call and Link›

text ‹The SETHI instruction.›
datatype sethi_type = SETHI    ― ‹Set High 22 bits of r Register›

text ‹The NOP instruction.›
datatype nop_type = NOP      ― ‹No Operation›

text ‹The Branch on integer condition codes instructions.› 
datatype bicc_type = 
  BE       ― ‹Branch on Equal›
 | BNE      ― ‹Branch on Not Equal›
 | BGU      ― ‹Branch on Greater Unsigned›
 | BLE      ― ‹Branch on Less or Equal›
 | BL       ― ‹Branch on Less›
 | BGE      ― ‹Branch on Greater or Equal›
 | BNEG     ― ‹Branch on Negative›
 | BG       ― ‹Branch on Greater›
 | BCS      ― ‹Branch on Carry Set (Less than, Unsigned)›
 | BLEU     ― ‹Branch on Less or Equal Unsigned›
 | BCC      ― ‹Branch on Carry Clear (Greater than or Equal, Unsigned)›
 | BA       ― ‹Branch Always›
 | BN       ― ‹Branch Never› ― ‹Added for unconditional branches›
 | BPOS     ― ‹Branch on Positive›
 | BVC      ― ‹Branch on Overflow Clear›
 | BVS      ― ‹Branch on Overflow Set›

text ‹Memory instructions. That is, load and store.›
datatype load_store_type =
  LDSB     ― ‹Load Signed Byte›
 | LDUB     ― ‹Load Unsigned Byte›
 | LDUBA    ― ‹Load Unsigned Byte from Alternate space›
 | LDUH     ― ‹Load Unsigned Halfword›
 | LD       ― ‹Load Word›
 | LDA      ― ‹Load Word from Alternate space›
 | LDD      ― ‹Load Doubleword›
 | STB      ― ‹Store Byte›
 | STH      ― ‹Store Halfword›
 | ST       ― ‹Store Word›
 | STA      ― ‹Store Word into Alternate space›
 | STD      ― ‹Store Doubleword›
 | LDSBA    ― ‹Load Signed Byte from Alternate space›
 | LDSH     ― ‹Load Signed Halfword›
 | LDSHA    ― ‹Load Signed Halfword from Alternate space›
 | LDUHA    ― ‹Load Unsigned Halfword from Alternate space›
 | LDDA     ― ‹Load Doubleword from Alternate space›
 | STBA     ― ‹Store Byte into Alternate space›
 | STHA     ― ‹Store Halfword into Alternate space›
 | STDA     ― ‹Store Doubleword into Alternate space›
 | LDSTUB   ― ‹Atomic Load Store Unsigned Byte›
 | LDSTUBA  ― ‹Atomic Load Store Unsinged Byte in Alternate space›
 | SWAP     ― ‹Swap r Register with Mmemory›
 | SWAPA    ― ‹Swap r Register with Mmemory in Alternate space›
 | FLUSH    ― ‹Flush Instruction Memory›
 | STBAR    ― ‹Store Barrier›

text ‹Arithmetic instructions.›
datatype arith_type =
  ADD      ― ‹Add›
 | ADDcc    ― ‹Add and modify icc›
 | ADDX     ― ‹Add with Carry›
 | SUB      ― ‹Subtract›
 | SUBcc    ― ‹Subtract and modify icc›
 | SUBX     ― ‹Subtract with Carry›
 | UMUL     ― ‹Unsigned Integer Multiply›
 | SMUL     ― ‹Signed Integer Multiply›
 | SMULcc   ― ‹Signed Integer Multiply and modify icc›
 | UDIV     ― ‹Unsigned Integer Divide›
 | UDIVcc   ― ‹Unsigned Integer Divide and modify icc›
 | SDIV     ― ‹Signed Integer Divide› 
 | ADDXcc   ― ‹Add with Carry and modify icc›
 | TADDcc   ― ‹Tagged Add and modify icc›
 | TADDccTV ― ‹Tagged Add and modify icc and Trap on overflow›
 | SUBXcc   ― ‹Subtract with Carry and modify icc›
 | TSUBcc   ― ‹Tagged Subtract and modify icc›
 | TSUBccTV ― ‹Tagged Subtract and modify icc and Trap on overflow›
 | MULScc   ― ‹Multiply Step and modify icc›
 | UMULcc   ― ‹Unsigned Integer Multiply and modify icc›
 | SDIVcc   ― ‹Signed Integer Divide and modify icc›

text ‹Logical instructions.›
datatype logic_type =
  ANDs      ― ‹And›
 | ANDcc    ― ‹And and modify icc›
 | ANDN     ― ‹And Not›
 | ANDNcc   ― ‹And Not and modify icc›
 | ORs       ― ‹Inclusive-Or›
 | ORcc     ― ‹Inclusive-Or and modify icc›
 | ORN      ― ‹Inclusive Or Not›
 | XORs      ― ‹Exclusive-Or›
 | XNOR     ― ‹Exclusive-Nor›
 | ORNcc    ― ‹Inclusive-Or Not and modify icc›
 | XORcc    ― ‹Exclusive-Or and modify icc›
 | XNORcc   ― ‹Exclusive-Nor and modify icc›
 
text ‹Shift instructions.›
datatype shift_type =
  SLL      ― ‹Shift Left Logical›
 | SRL      ― ‹Shift Right Logical›
 | SRA      ― ‹Shift Right Arithmetic› 

text ‹Other Control-transfer instructions.›
datatype ctrl_type = 
  JMPL     ― ‹Jump and Link›
 | RETT     ― ‹Return from Trap›
 | SAVE     ― ‹Save caller's window›
 | RESTORE  ― ‹Restore caller's window› 

text ‹Access state registers instructions.›
datatype sreg_type =
  RDASR    ― ‹Read Ancillary State Register›
 | RDY      ― ‹Read Y Register›
 | RDPSR    ― ‹Read Processor State Register›
 | RDWIM    ― ‹Read Window Invalid Mask Register›
 | RDTBR    ― ‹Read Trap Base Regiser›
 | WRASR    ― ‹Write Ancillary State Register›
 | WRY      ― ‹Write Y Register›
 | WRPSR    ― ‹Write Processor State Register›
 | WRWIM    ― ‹Write Window Invalid Mask Register›
 | WRTBR    ― ‹Write Trap Base Register› 

text ‹Unimplemented instruction.›
datatype uimp_type = UNIMP    ― ‹Unimplemented› 

text ‹Trap on integer condition code instructions.›
datatype ticc_type =
 TA       ― ‹Trap Always›
 | TN       ― ‹Trap Never›
 | TNE      ― ‹Trap on Not Equal›
 | TE       ― ‹Trap on Equal›
 | TG       ― ‹Trap on Greater›
 | TLE      ― ‹Trap on Less or Equal›
 | TGE      ― ‹Trap on Greater or Equal›
 | TL       ― ‹Trap on Less›
 | TGU      ― ‹Trap on Greater Unsigned›
 | TLEU     ― ‹Trap on Less or Equal Unsigned›
 | TCC      ― ‹Trap on Carry Clear (Greater than or Equal, Unsigned)›
 | TCS      ― ‹Trap on Carry Set (Less Than, Unsigned)›
 | TPOS     ― ‹Trap on Postive›
 | TNEG     ― ‹Trap on Negative›
 | TVC      ― ‹Trap on Overflow Clear›
 | TVS      ― ‹Trap on Overflow Set›

datatype sparc_operation =
  call_type call_type
 | sethi_type sethi_type
 | nop_type nop_type
 | bicc_type bicc_type
 | load_store_type load_store_type
 | arith_type arith_type
 | logic_type logic_type
 | shift_type shift_type
 | ctrl_type ctrl_type
 | sreg_type sreg_type
 | uimp_type uimp_type
 | ticc_type ticc_type

datatype Trap = 
reset 
|data_store_error
|instruction_access_MMU_miss
|instruction_access_error
|r_register_access_error
|instruction_access_exception
|privileged_instruction
|illegal_instruction
|unimplemented_FLUSH
|watchpoint_detected
|fp_disabled
|cp_disabled
|window_overflow
|window_underflow
|mem_address_not_aligned
|fp_exception
|cp_exception
|data_access_error
|data_access_MMU_miss
|data_access_exception
|tag_overflow
|division_by_zero
|trap_instruction
|interrupt_level_n

datatype Exception =
― ‹The following are processor states that are not in the instruction model,›
― ‹but we MAY want to deal with these from hardware perspective.›
⌦‹|execute_mode›
⌦‹|reset_mode›
⌦‹|error_mode›
― ‹The following are self-defined exceptions.›
invalid_cond_f2
|invalid_op2_f2
|illegal_instruction2 ― ‹when ‹i = 0› for load/store not from alternate space›
|invalid_op3_f3_op11
|case_impossible
|invalid_op3_f3_op10
|invalid_op_f3
|unsupported_instruction
|fetch_instruction_error
|invalid_trap_cond

end

end