(* *)
(* ********************************************************************** *)
-include "emulator/opcodes/opcode.ma".
+include "emulator/opcodes/pseudo.ma".
include "emulator/opcodes/HCS08_table.ma".
(* ****************** *)
;〈xA,xC〉
].
-(* test bytecode non implementati *)
nlemma ok_byte_table_HCS08 : forall_b8 (λb.
(test_not_impl_byte b HCS08_not_impl_byte ⊙ eq_w16 (get_byte_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
(⊖ (test_not_impl_byte b HCS08_not_impl_byte) ⊙ eq_w16 (get_byte_count HCS08 b 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
;〈xF,x0〉;〈xF,x1〉;〈xF,x2〉;〈xF,x4〉;〈xF,x5〉;〈xF,x6〉;〈xF,x7〉;〈xF,x8〉;〈xF,x9〉;〈xF,xA〉;〈xF,xB〉;〈xF,xC〉;〈xF,xD〉
].
-(* test bytecode non implementati *)
nlemma ok_word_table_HCS08 : forall_b8 (λb.
(test_not_impl_byte b HCS08_not_impl_word ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉) ⊗
(⊖ (test_not_impl_byte b HCS08_not_impl_word) ⊙ eq_w16 (get_word_count HCS08 〈〈x9,xE〉:b〉 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
napply refl_eq.
nqed.
-(* tutti op implementati *)
-nlemma ok_pseudo_table_HCS08 :
- forall_op HCS08 (λo.
- le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) = true.
+(* HCS08: pseudocodici non implementati come da manuale *)
+ndefinition HCS08_not_impl_pseudo ≝
+ [ SHA ; SLA ].
+
+nlemma ok_pseudo_table_HCS08 : forall_Freescale_pseudo (λo.
+ (test_not_impl_pseudo HCS08 o HCS08_not_impl_pseudo ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) ⊗
+ (⊖ (test_not_impl_pseudo HCS08 o HCS08_not_impl_pseudo) ⊙ eq_w16 (get_pseudo_count HCS08 o 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
+ = true.
napply refl_eq.
nqed.
-(* tutte im implementate *)
-nlemma ok_mode_table_HCS08 :
- forall_im HCS08 (λi.
- le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HCS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) = true.
+(* HCS08: modalita' non implementate come da manuale *)
+ndefinition HCS08_not_impl_mode ≝
+ [ MODE_TNY x0 ; MODE_TNY x1 ; MODE_TNY x2 ; MODE_TNY x3
+ ; MODE_TNY x4 ; MODE_TNY x5 ; MODE_TNY x6 ; MODE_TNY x7
+ ; MODE_TNY x8 ; MODE_TNY x9 ; MODE_TNY xA ; MODE_TNY xB
+ ; MODE_TNY xC ; MODE_TNY xD ; MODE_TNY xE ; MODE_TNY xF
+ ; MODE_SRT t00 ; MODE_SRT t01 ; MODE_SRT t02 ; MODE_SRT t03
+ ; MODE_SRT t04 ; MODE_SRT t05 ; MODE_SRT t06 ; MODE_SRT t07
+ ; MODE_SRT t08 ; MODE_SRT t09 ; MODE_SRT t0A ; MODE_SRT t0B
+ ; MODE_SRT t0C ; MODE_SRT t0D ; MODE_SRT t0E ; MODE_SRT t0F
+ ; MODE_SRT t10 ; MODE_SRT t11 ; MODE_SRT t12 ; MODE_SRT t13
+ ; MODE_SRT t14 ; MODE_SRT t15 ; MODE_SRT t16 ; MODE_SRT t17
+ ; MODE_SRT t18 ; MODE_SRT t19 ; MODE_SRT t1A ; MODE_SRT t1B
+ ; MODE_SRT t1C ; MODE_SRT t1D ; MODE_SRT t1E ; MODE_SRT t1F ].
+
+nlemma ok_mode_table_HCS08 : forall_Freescale_im (λi.
+ (test_not_impl_mode HCS08 i HCS08_not_impl_mode ⊙ le_w16 〈〈x0,x0〉:〈x0,x1〉〉 (get_mode_count HCS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08)) ⊗
+ (⊖ (test_not_impl_mode HCS08 i HCS08_not_impl_mode) ⊙ eq_w16 (get_mode_count HCS08 i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x0〉〉))
+ = true.
napply refl_eq.
nqed.
-(* nessuna ripetizione di combinazione op + imm *)
-nlemma ok_OpIm_table_HCS08 :
- forall_im HCS08 (λi.
- forall_op HCS08 (λo.
- le_w16 (get_OpIm_count HCS08 o i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true.
+nlemma ok_PsIm_table_HCS08 :
+ forall_Freescale_im (λi:Freescale_instr_mode.
+ forall_Freescale_pseudo (λps:Freescale_pseudo.
+ le_w16 (get_PsIm_count HCS08 ps i 〈〈x0,x0〉:〈x0,x0〉〉 opcode_table_HCS08) 〈〈x0,x0〉:〈x0,x1〉〉)) = true.
napply refl_eq.
nqed.