(* etc... *)
].
-(*
- parametrizzati i non deterministici rispetto a tutti i valori casuali
+(* parametrizzati i non deterministici rispetto a tutti i valori casuali
che verranno dati dall'esterno di tipo byte8 (ndby1-2) e bool (ndbo1-5).
l'ACCENSIONE e' totalmente equivalente ad un reset causato da calo di tensione
- (reset V-low), la memoria ed il check possono essere passati
-*)
+ (reset V-low), la memoria ed il check possono essere passati *)
ndefinition start_of_model_HCS08 ≝
λmcu:HCS08_model.λt:memory_impl.
λmem:aux_mem_type t.λchk:aux_chk_type t.
(* chk *) chk
(* clk: reset *) (None ?).
-(*
- cio' che non viene resettato mantiene il valore precedente: nella documentazione
+(* cio' che non viene resettato mantiene il valore precedente: nella documentazione
viene riportato come "unaffected"/"indeterminate"/"unpredictable"
- il soft RESET e' diverso da un calo di tensione e la ram non variera'
-*)
+ il soft RESET e' diverso da un calo di tensione e la ram non variera' *)
ndefinition reset_of_model_HCS08 ≝
λt:memory_impl.λs:any_status HCS08 t.
(mk_any_status HCS08 t