(* 0x3800-0x3FFF *) ; triple … 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x3,x8〉:〈x0,x0〉〉〉 〈〈x0,x8〉:〈x0,x0〉〉 MEM_READ_ONLY (* 2048B FLASH *) ]
].
-(*
- 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_RS08 ≝
λmcu:RS08_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_RS08 ≝
λt:memory_impl.λs:any_status RS08 t.
(mk_any_status RS08 t