(* ********************************************************************** *)
(* 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) *)
irq_flag_HC05 : bool
}.
-ndefinition alu_HC05_ind :
- ΠP:alu_HC05 → Prop.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
-λP:alu_HC05 → Prop.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
- match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
-
-ndefinition alu_HC05_rec :
- ΠP:alu_HC05 → Set.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
-λP:alu_HC05 → Set.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
- match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
-
-ndefinition alu_HC05_rect :
- ΠP:alu_HC05 → Type.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝
-λP:alu_HC05 → Type.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05.
- match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ].
-
-ndefinition acc_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 x _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition indX_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition sp_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition sp_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition sp_fix_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition pc_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ].
-ndefinition pc_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ].
-ndefinition h_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ].
-ndefinition i_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ].
-ndefinition n_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ].
-ndefinition z_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
-ndefinition c_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
-ndefinition irq_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
-
notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
non associative with precedence 80 for
@{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }.
irq_flag_HC08 : bool
}.
-ndefinition alu_HC08_ind :
- ΠP:alu_HC08 → Prop.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
-λP:alu_HC08 → Prop.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
- match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
-
-ndefinition alu_HC08_rec :
- ΠP:alu_HC08 → Set.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
-λP:alu_HC08 → Set.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
- match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
-
-ndefinition alu_HC08_rect :
- ΠP:alu_HC08 → Type.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝
-λP:alu_HC08 → Type.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08.
- match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ].
-
-ndefinition acc_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition indX_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition indX_high_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition sp_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ].
-ndefinition pc_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ].
-ndefinition v_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ].
-ndefinition h_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ].
-ndefinition i_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ].
-ndefinition n_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ].
-ndefinition z_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ].
-ndefinition c_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ].
-ndefinition irq_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ].
-
notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}"
non associative with precedence 80 for
@{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }.
c_flag_RS08 : bool
}.
-ndefinition alu_RS08_ind :
- ΠP:alu_RS08 → Prop.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
-λP:alu_RS08 → Prop.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
- match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
-
-ndefinition alu_RS08_rec :
- ΠP:alu_RS08 → Set.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
-λP:alu_RS08 → Set.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
- match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
-
-ndefinition alu_RS08_rect :
- ΠP:alu_RS08 → Type.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝
-λP:alu_RS08 → Type.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08.
- match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ].
-
-ndefinition acc_low_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 x _ _ _ _ _ _ _ ⇒ x ].
-ndefinition pc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ x _ _ _ _ _ _ ⇒ x ].
-ndefinition pc_mask_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ x _ _ _ _ _ ⇒ x ].
-ndefinition spc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ x _ _ _ _ ⇒ x ].
-ndefinition x_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ x _ _ _ ⇒ x ].
-ndefinition ps_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ x _ _ ⇒ x ].
-ndefinition z_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ x _ ⇒ x ].
-ndefinition c_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ _ x ⇒ x ].
-
notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}"
non associative with precedence 80 for
@{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }.
clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
}.
-ndefinition any_status_ind :
- Πmcu.Πt.ΠP:any_status mcu t → Prop.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Prop.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rec :
- Πmcu.Πt.ΠP:any_status mcu t → Set.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Set.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rect :
- Πmcu.Πt.ΠP:any_status mcu t → Type.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Type.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition alu ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status (x:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]) _ _ _ ⇒ x ].
-ndefinition mem_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ x _ _ ⇒ x ].
-ndefinition chk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ x _ ⇒ x ].
-ndefinition clk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ _ x ⇒ x ].
-
(* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80
for @{ 'mk_any_status $alu $mem $chk $clk }.
| RS08 ⇒ λalu.None ? ]
(alu m t s).
-(* DESCRITTORI ESTERNI ALLA ALU *)
-
-(* getter della ALU, esiste sempre *)
-ndefinition get_alu ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.alu m t s.
-
-(* getter della memoria, esiste sempre *)
-ndefinition get_mem_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.mem_desc m t s.
-
-(* getter del descrittore, esiste sempre *)
-ndefinition get_chk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.chk_desc m t s.
-
-(* getter del clik, esiste sempre *)
-ndefinition get_clk_desc ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t.clk_desc m t s.
-
(* ***************************** *)
(* SETTER SPECIFICI FORTI/DEBOLI *)
(* ***************************** *)
(* setter forte della ALU *)
ndefinition set_alu ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λalu'.
- mk_any_status m t alu' (get_mem_desc m t s) (get_chk_desc m t s) (get_clk_desc m t s).
+ mk_any_status m t alu' (mem_desc m t s) (chk_desc m t s) (clk_desc m t s).
(* setter forte della memoria *)
ndefinition set_mem_desc ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λmem':aux_mem_type t.
- mk_any_status m t (get_alu m t s) mem' (get_chk_desc m t s) (get_clk_desc m t s).
+ mk_any_status m t (alu m t s) mem' (chk_desc m t s) (clk_desc m t s).
(* setter forte del descrittore *)
ndefinition set_chk_desc ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λchk':aux_chk_type t.
- mk_any_status m t (get_alu m t s) (get_mem_desc m t s) chk' (get_clk_desc m t s).
+ mk_any_status m t (alu m t s) (mem_desc m t s) chk' (clk_desc m t s).
(* setter forte del clik *)
ndefinition set_clk_desc ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.
λclk':option (Prod5T byte8 (any_opcode m) (instr_mode) byte8 word16).
- mk_any_status m t (get_alu m t s) (get_mem_desc m t s) (get_chk_desc m t s) clk'.
+ mk_any_status m t (alu m t s) (mem_desc m t s) (chk_desc m t s) clk'.
(* REGISTRO A *)
(* setter forte di X *)
ndefinition set_indX_8_low_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
[ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
| HC08 ⇒ Some ? set_indX_8_low_reg_HC08
| HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
(* setter forte di H *)
ndefinition set_indX_8_high_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
[ HC05 ⇒ None ?
| HC08 ⇒ Some ? set_indX_8_high_reg_HC08
| HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
(* setter forte di H:X *)
ndefinition set_indX_16_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
- opt_map ?? (match m return aux_set_typing_opt word16 with
+ opt_map … (match m return aux_set_typing_opt word16 with
[ HC05 ⇒ None ?
| HC08 ⇒ Some ? set_indX_16_reg_HC08
| HCS08 ⇒ Some ? set_indX_16_reg_HC08
(* setter forte di SP *)
ndefinition set_sp_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
- opt_map ?? (match m return aux_set_typing_opt word16 with
+ opt_map … (match m return aux_set_typing_opt word16 with
[ HC05 ⇒ Some ? set_sp_reg_HC05
| HC08 ⇒ Some ? set_sp_reg_HC08
| HCS08 ⇒ Some ? set_sp_reg_HC08
(* setter forte di SPC *)
ndefinition set_spc_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
- opt_map ?? (match m return aux_set_typing_opt word16 with
+ opt_map … (match m return aux_set_typing_opt word16 with
[ HC05 ⇒ None ?
| HC08 ⇒ None ?
| HCS08 ⇒ None ?
(* setter forte di memory mapped X *)
ndefinition set_x_map ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λxm':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
[ HC05 ⇒ None ?
| HC08 ⇒ None ?
| HCS08 ⇒ None ?
(* setter forte di memory mapped PS *)
ndefinition set_ps_map ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
- opt_map ?? (match m return aux_set_typing_opt byte8 with
+ opt_map … (match m return aux_set_typing_opt byte8 with
[ HC05 ⇒ None ?
| HC08 ⇒ None ?
| HCS08 ⇒ None ?
(* setter forte di V *)
ndefinition set_v_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λvfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
[ HC05 ⇒ None ?
| HC08 ⇒ Some ? set_v_flag_HC08
| HCS08 ⇒ Some ? set_v_flag_HC08
(* setter forte di H *)
ndefinition set_h_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
[ HC05 ⇒ Some ? set_h_flag_HC05
| HC08 ⇒ Some ? set_h_flag_HC08
| HCS08 ⇒ Some ? set_h_flag_HC08
(* setter forte di I *)
ndefinition set_i_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
[ HC05 ⇒ Some ? set_i_flag_HC05
| HC08 ⇒ Some ? set_i_flag_HC08
| HCS08 ⇒ Some ? set_i_flag_HC08
(* setter forte di N *)
ndefinition set_n_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
[ HC05 ⇒ Some ? set_n_flag_HC05
| HC08 ⇒ Some ? set_n_flag_HC08
| HCS08 ⇒ Some ? set_n_flag_HC08
(* setter forte di IRQ *)
ndefinition set_irq_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
- opt_map ?? (match m return aux_set_typing_opt bool with
+ opt_map … (match m return aux_set_typing_opt bool with
[ HC05 ⇒ Some ? set_irq_flag_HC05
| HC08 ⇒ Some ? set_irq_flag_HC08
| HCS08 ⇒ Some ? set_irq_flag_HC08
(* ***************** *)
(* 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 ⇒
[ None ⇒ match c2 with
[ None ⇒ true | Some _ ⇒ false ]
| 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_b8 (frth5T ????? c1') (frth5T ????? c2')) ⊗
- (eq_w16 (ffth5T ????? c1') (ffth5T ????? c2')) ]
+ [ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
+ (eq_anyop m (snd5T … c1') (snd5T … 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] *)
projects / helm.git / blobdiff