(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
include "freescale/memory_abs.ma".
include "freescale/opcode_base.ma".
-include "freescale/prod.ma".
(* *********************************** *)
(* STATUS INTERNO DEL PROCESSORE (ALU) *)
(* ***************** *)
(* confronto registro per registro dell'HC05 *)
-ndefinition eq_alu_HC05 ≝
+ndefinition eq_aluHC05 ≝
λalu1,alu2:alu_HC05.
match alu1 with
[ mk_alu_HC05 acclow1 indxlow1 sp1 spm1 spf1 pc1 pcm1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
(eq_bool irqfl1 irqfl2) ]].
(* confronto registro per registro dell'HC08 *)
-ndefinition eq_alu_HC08 ≝
+ndefinition eq_aluHC08 ≝
λalu1,alu2:alu_HC08.
match alu1 with
[ mk_alu_HC08 acclow1 indxlow1 indxhigh1 sp1 pc1 vfl1 hfl1 ifl1 nfl1 zfl1 cfl1 irqfl1 ⇒
(eq_bool irqfl1 irqfl2) ]].
(* confronto registro per registro dell'RS08 *)
-ndefinition eq_alu_RS08 ≝
+ndefinition eq_aluRS08 ≝
λalu1,alu2:alu_RS08.
match alu1 with
[ mk_alu_RS08 acclow1 pc1 pcm1 spc1 xm1 psm1 zfl1 cfl1 ⇒
| Some c1' ⇒ match c2 with
[ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
(eq_anyop m (snd5T … c1') (snd5T … c2')) ⊗
- (eq_instrmode (thd5T … c1') (thd5T … c2')) ⊗
+ (eq_im (thd5T … c1') (thd5T … c2')) ⊗
(eq_b8 (frth5T … c1') (frth5T … c2')) ⊗
(eq_w16 (ffth5T … c1') (ffth5T … c2')) ]
].
(* generalizzazione del confronto fra stati *)
-ndefinition eq_status ≝
+ndefinition eq_anystatus ≝
λm:mcu_type.λt:memory_impl.λs1,s2:any_status m t.λaddrl:list word16.
match s1 with [ mk_any_status alu1 mem1 chk1 clk1 ⇒
match s2 with [ mk_any_status alu2 mem2 chk2 clk2 ⇒
match m with
[ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
bool with
- [ HC05 ⇒ eq_alu_HC05 | HC08 ⇒ eq_alu_HC08 | HCS08 ⇒ eq_alu_HC08 | RS08 ⇒ eq_alu_RS08 ]
+ [ HC05 ⇒ eq_aluHC05 | HC08 ⇒ eq_aluHC08 | HCS08 ⇒ eq_aluHC08 | RS08 ⇒ eq_aluRS08 ]
alu1 alu2) ⊗
(* 2) confronto della memoria in [inf,inf+n] *)