From: Cosimo Oliboni Date: Wed, 29 Jul 2009 16:30:44 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3597 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=842e243be954d67360788d08701289f3237c2699;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma index 5bfd406b5..766be3772 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma @@ -116,11 +116,11 @@ ndefinition RS08_memory_filter_read_bit ≝ ndefinition memory_filter_read ≝ λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → option byte8 with [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16. - mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr + mem_read t (mem_desc ? t s) (chk_desc ? t s) addr | HC08 ⇒ λs:any_status HC08 t.λaddr:word16. - mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr + mem_read t (mem_desc ? t s) (chk_desc ? t s) addr | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16. - mem_read t (get_mem_desc ? t s) (get_chk_desc ? t s) addr + mem_read t (mem_desc ? t s) (chk_desc ? t s) addr | RS08 ⇒ λs:any_status RS08 t.λaddr:word16. RS08_memory_filter_read t s addr ]. @@ -128,11 +128,11 @@ ndefinition memory_filter_read ≝ ndefinition memory_filter_read_bit ≝ λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → option bool with [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct. - mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub + mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct. - mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub + mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct. - mem_read_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub + mem_read_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct. RS08_memory_filter_read_bit t s addr sub ]. @@ -217,13 +217,13 @@ ndefinition memory_filter_write ≝ λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → byte8 → option (any_status m t) with [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λval:byte8. - opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val) + opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val) (λmem.Some ? (set_mem_desc ? t s mem)) | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λval:byte8. - opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val) + opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val) (λmem.Some ? (set_mem_desc ? t s mem)) | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λval:byte8. - opt_map ?? (mem_update t (get_mem_desc ? t s) (get_chk_desc ? t s) addr val) + opt_map ?? (mem_update t (mem_desc ? t s) (chk_desc ? t s) addr val) (λmem.Some ? (set_mem_desc ? t s mem)) | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λval:byte8. RS08_memory_filter_write t s addr val @@ -233,13 +233,13 @@ ndefinition memory_filter_write_bit ≝ λm:mcu_type.λt:memory_impl.match m return λm:mcu_type.any_status m t → word16 → oct → bool → option (any_status m t) with [ HC05 ⇒ λs:any_status HC05 t.λaddr:word16.λsub:oct.λval:bool. - opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val) + opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val) (λmem.Some ? (set_mem_desc ? t s mem)) | HC08 ⇒ λs:any_status HC08 t.λaddr:word16.λsub:oct.λval:bool. - opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val) + opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val) (λmem.Some ? (set_mem_desc ? t s mem)) | HCS08 ⇒ λs:any_status HCS08 t.λaddr:word16.λsub:oct.λval:bool. - opt_map ?? (mem_update_bit t (get_mem_desc ? t s) (get_chk_desc ? t s) addr sub val) + opt_map ?? (mem_update_bit t (mem_desc ? t s) (chk_desc ? t s) addr sub val) (λmem.Some ? (set_mem_desc ? t s mem)) | RS08 ⇒ λs:any_status RS08 t.λaddr:word16.λsub:oct.λval:bool. RS08_memory_filter_write_bit t s addr sub val diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma index fc374d9ab..e0277386c 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma @@ -1268,7 +1268,7 @@ ndefinition tick_execute ≝ ndefinition tick ≝ λm:mcu_type.λt:memory_impl.λs:any_status m t. - let opt_info ≝ get_clk_desc m t s in + let opt_info ≝ clk_desc m t s in match opt_info with (* e' il momento del fetch *) [ None ⇒ match fetch m t s with diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma index e6d42deed..6a0f81887 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma @@ -165,7 +165,6 @@ nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝ clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16) }. - (* 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 }. @@ -362,20 +361,6 @@ ndefinition get_irq_flag ≝ | 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 *) (* ***************************** *) @@ -397,23 +382,23 @@ ndefinition aux_set_typing_opt ≝ λx:Type.λm:mcu_type.option (* 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 *)