Context Navigation

Status.ma @ 724

Last change on this file since 724 was 705, checked in by sacerdot, 10 years ago
Ported to new library (notation).
File size: 34.4 KB

Line
1	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2	(* Interpret.ma: Operational semantics for the 8051/8052 processor. *)
3	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5	include "ASM/ASM.ma".
6	include "ASM/Arithmetic.ma".
7	include "ASM/BitVectorTrie.ma".
8
9	definition Time ≝ nat.
10
11	inductive SerialBufferType: Type[0] ≝
12	Eight: Byte → SerialBufferType
13	\| Nine: Bit → Byte → SerialBufferType.
14
15	inductive LineType: Type[0] ≝
16	P1: Byte → LineType
17	\| P3: Byte → LineType
18	\| SerialBuffer: SerialBufferType → LineType.
19
20	(* What is a continuation, now? *)
21
22	inductive SFR8051: Type[0] ≝
23	SFR_SP: SFR8051
24	\| SFR_DPL: SFR8051
25	\| SFR_DPH: SFR8051
26	\| SFR_PCON: SFR8051
27	\| SFR_TCON: SFR8051
28	\| SFR_TMOD: SFR8051
29	\| SFR_TL0: SFR8051
30	\| SFR_TL1: SFR8051
31	\| SFR_TH0: SFR8051
32	\| SFR_TH1: SFR8051
33	\| SFR_P1: SFR8051
34	\| SFR_SCON: SFR8051
35	\| SFR_SBUF: SFR8051
36	\| SFR_IE: SFR8051
37	\| SFR_P3: SFR8051
38	\| SFR_IP: SFR8051
39	\| SFR_PSW: SFR8051
40	\| SFR_ACC_A: SFR8051
41	\| SFR_ACC_B: SFR8051.
42
43	definition sfr_8051_index ≝
44	λs: SFR8051.
45	match s with
46	[ SFR_SP ⇒ O
47	\| SFR_DPL ⇒ 1
48	\| SFR_DPH ⇒ 2
49	\| SFR_PCON ⇒ 3
50	\| SFR_TCON ⇒ 4
51	\| SFR_TMOD ⇒ 5
52	\| SFR_TL0 ⇒ 6
53	\| SFR_TL1 ⇒ 7
54	\| SFR_TH0 ⇒ 8
55	\| SFR_TH1 ⇒ 9
56	\| SFR_P1 ⇒ 10
57	\| SFR_SCON ⇒ 11
58	\| SFR_SBUF ⇒ 12
59	\| SFR_IE ⇒ 13
60	\| SFR_P3 ⇒ 14
61	\| SFR_IP ⇒ 15
62	\| SFR_PSW ⇒ 16
63	\| SFR_ACC_A ⇒ 17
64	\| SFR_ACC_B ⇒ 18
65	].
66
67	inductive SFR8052: Type[0] ≝
68	SFR_T2CON: SFR8052
69	\| SFR_RCAP2L: SFR8052
70	\| SFR_RCAP2H: SFR8052
71	\| SFR_TL2: SFR8052
72	\| SFR_TH2: SFR8052.
73
74	definition sfr_8052_index ≝
75	λs: SFR8052.
76	match s with
77	[ SFR_T2CON ⇒ O
78	\| SFR_RCAP2L ⇒ 1
79	\| SFR_RCAP2H ⇒ 2
80	\| SFR_TL2 ⇒ 3
81	\| SFR_TH2 ⇒ 4
82	].
83
84	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
85	(* Processor status. *)
86	(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
87	record Status: Type[0] ≝
88	{
89	code_memory: BitVectorTrie Byte 16;
90	low_internal_ram: BitVectorTrie Byte 7;
91	high_internal_ram: BitVectorTrie Byte 7;
92	external_ram: BitVectorTrie Byte 16;
93
94	program_counter: Word;
95
96	special_function_registers_8051: Vector Byte 19;
97	special_function_registers_8052: Vector Byte 5;
98
99	p1_latch: Byte;
100	p3_latch: Byte;
101
102	clock: Time
103	}.
104
105	lemma sfr8051_index_19:
106	∀i: SFR8051.
107	sfr_8051_index i < 19.
108	# i
109	cases i
110	normalize
111	repeat (@ le_S_S)
112	@ le_O_n
113	qed.
114
115	lemma sfr8052_index_5:
116	∀i: SFR8052.
117	sfr_8052_index i < 5.
118	# i
119	cases i
120	normalize
121	repeat (@ le_S_S)
122	@ le_O_n
123	qed.
124
125	definition set_clock ≝
126	λs: Status.
127	λt: Time.
128	let old_code_memory ≝ code_memory s in
129	let old_low_internal_ram ≝ low_internal_ram s in
130	let old_high_internal_ram ≝ high_internal_ram s in
131	let old_external_ram ≝ external_ram s in
132	let old_program_counter ≝ program_counter s in
133	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
134	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
135	let old_p1_latch ≝ p1_latch s in
136	let old_p3_latch ≝ p3_latch s in
137	mk_Status old_code_memory
138	old_low_internal_ram
139	old_high_internal_ram
140	old_external_ram
141	old_program_counter
142	old_special_function_registers_8051
143	old_special_function_registers_8052
144	old_p1_latch
145	old_p3_latch
146	t.
147
148	definition set_p1_latch ≝
149	λs: Status.
150	λb: Byte.
151	let old_code_memory ≝ code_memory s in
152	let old_low_internal_ram ≝ low_internal_ram s in
153	let old_high_internal_ram ≝ high_internal_ram s in
154	let old_external_ram ≝ external_ram s in
155	let old_program_counter ≝ program_counter s in
156	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
157	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
158	let old_p3_latch ≝ p3_latch s in
159	let old_clock ≝ clock s in
160	mk_Status old_code_memory
161	old_low_internal_ram
162	old_high_internal_ram
163	old_external_ram
164	old_program_counter
165	old_special_function_registers_8051
166	old_special_function_registers_8052
167	b
168	old_p3_latch
169	old_clock.
170
171	definition set_p3_latch ≝
172	λs: Status.
173	λb: Byte.
174	let old_code_memory ≝ code_memory s in
175	let old_low_internal_ram ≝ low_internal_ram s in
176	let old_high_internal_ram ≝ high_internal_ram s in
177	let old_external_ram ≝ external_ram s in
178	let old_program_counter ≝ program_counter s in
179	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
180	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
181	let old_p1_latch ≝ p1_latch s in
182	let old_clock ≝ clock s in
183	mk_Status old_code_memory
184	old_low_internal_ram
185	old_high_internal_ram
186	old_external_ram
187	old_program_counter
188	old_special_function_registers_8051
189	old_special_function_registers_8052
190	old_p1_latch
191	b
192	old_clock.
193
194	definition get_8051_sfr ≝
195	λs: Status.
196	λi: SFR8051.
197	let sfr ≝ special_function_registers_8051 s in
198	let index ≝ sfr_8051_index i in
199	get_index_v … sfr index ?.
200	@ sfr8051_index_19
201	qed.
202
203	definition get_8052_sfr ≝
204	λs: Status.
205	λi: SFR8052.
206	let sfr ≝ special_function_registers_8052 s in
207	let index ≝ sfr_8052_index i in
208	get_index_v … sfr index ?.
209	@ sfr8052_index_5
210	qed.
211
212	definition set_8051_sfr ≝
213	λs: Status.
214	λi: SFR8051.
215	λb: Byte.
216	let index ≝ sfr_8051_index i in
217	let old_code_memory ≝ code_memory s in
218	let old_low_internal_ram ≝ low_internal_ram s in
219	let old_high_internal_ram ≝ high_internal_ram s in
220	let old_external_ram ≝ external_ram s in
221	let old_program_counter ≝ program_counter s in
222	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
223	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
224	let new_special_function_registers_8051 ≝
225	set_index Byte 19 old_special_function_registers_8051 index b ? in
226	let old_p1_latch ≝ p1_latch s in
227	let old_p3_latch ≝ p3_latch s in
228	let old_clock ≝ clock s in
229	mk_Status old_code_memory
230	old_low_internal_ram
231	old_high_internal_ram
232	old_external_ram
233	old_program_counter
234	new_special_function_registers_8051
235	old_special_function_registers_8052
236	old_p1_latch
237	old_p3_latch
238	old_clock.
239	@ (sfr8051_index_19 i)
240	qed.
241
242	definition set_8052_sfr ≝
243	λs: Status.
244	λi: SFR8052.
245	λb: Byte.
246	let index ≝ sfr_8052_index i in
247	let old_code_memory ≝ code_memory s in
248	let old_low_internal_ram ≝ low_internal_ram s in
249	let old_high_internal_ram ≝ high_internal_ram s in
250	let old_external_ram ≝ external_ram s in
251	let old_program_counter ≝ program_counter s in
252	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
253	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
254	let new_special_function_registers_8052 ≝
255	set_index Byte 5 old_special_function_registers_8052 index b ? in
256	let old_p1_latch ≝ p1_latch s in
257	let old_p3_latch ≝ p3_latch s in
258	let old_clock ≝ clock s in
259	mk_Status old_code_memory
260	old_low_internal_ram
261	old_high_internal_ram
262	old_external_ram
263	old_program_counter
264	old_special_function_registers_8051
265	new_special_function_registers_8052
266	old_p1_latch
267	old_p3_latch
268	old_clock.
269	@ (sfr8052_index_5 i)
270	qed.
271
272	definition set_program_counter ≝
273	λs: Status.
274	λw: Word.
275	let old_code_memory ≝ code_memory s in
276	let old_low_internal_ram ≝ low_internal_ram s in
277	let old_high_internal_ram ≝ high_internal_ram s in
278	let old_external_ram ≝ external_ram s in
279	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
280	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
281	let old_p1_latch ≝ p1_latch s in
282	let old_p3_latch ≝ p3_latch s in
283	let old_clock ≝ clock s in
284	mk_Status old_code_memory
285	old_low_internal_ram
286	old_high_internal_ram
287	old_external_ram
288	w
289	old_special_function_registers_8051
290	old_special_function_registers_8052
291	old_p1_latch
292	old_p3_latch
293	old_clock.
294
295	definition set_code_memory ≝
296	λs: Status.
297	λr: BitVectorTrie Byte 16.
298	let old_low_internal_ram ≝ low_internal_ram s in
299	let old_high_internal_ram ≝ high_internal_ram s in
300	let old_external_ram ≝ external_ram s in
301	let old_program_counter ≝ program_counter s in
302	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
303	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
304	let old_p1_latch ≝ p1_latch s in
305	let old_p3_latch ≝ p3_latch s in
306	let old_clock ≝ clock s in
307	mk_Status r
308	old_low_internal_ram
309	old_high_internal_ram
310	old_external_ram
311	old_program_counter
312	old_special_function_registers_8051
313	old_special_function_registers_8052
314	old_p1_latch
315	old_p3_latch
316	old_clock.
317
318	definition set_low_internal_ram ≝
319	λs: Status.
320	λr: BitVectorTrie Byte 7.
321	let old_code_memory ≝ code_memory s in
322	let old_high_internal_ram ≝ high_internal_ram s in
323	let old_external_ram ≝ external_ram s in
324	let old_program_counter ≝ program_counter s in
325	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
326	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
327	let old_p1_latch ≝ p1_latch s in
328	let old_p3_latch ≝ p3_latch s in
329	let old_clock ≝ clock s in
330	mk_Status old_code_memory
331	r
332	old_high_internal_ram
333	old_external_ram
334	old_program_counter
335	old_special_function_registers_8051
336	old_special_function_registers_8052
337	old_p1_latch
338	old_p3_latch
339	old_clock.
340
341	definition set_high_internal_ram ≝
342	λs: Status.
343	λr: BitVectorTrie Byte 7.
344	let old_code_memory ≝ code_memory s in
345	let old_low_internal_ram ≝ low_internal_ram s in
346	let old_high_internal_ram ≝ high_internal_ram s in
347	let old_external_ram ≝ external_ram s in
348	let old_program_counter ≝ program_counter s in
349	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
350	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
351	let old_p1_latch ≝ p1_latch s in
352	let old_p3_latch ≝ p3_latch s in
353	let old_clock ≝ clock s in
354	mk_Status old_code_memory
355	old_low_internal_ram
356	r
357	old_external_ram
358	old_program_counter
359	old_special_function_registers_8051
360	old_special_function_registers_8052
361	old_p1_latch
362	old_p3_latch
363	old_clock.
364
365	definition set_external_ram ≝
366	λs: Status.
367	λr: BitVectorTrie Byte 16.
368	let old_code_memory ≝ code_memory s in
369	let old_low_internal_ram ≝ low_internal_ram s in
370	let old_high_internal_ram ≝ high_internal_ram s in
371	let old_program_counter ≝ program_counter s in
372	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
373	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
374	let old_p1_latch ≝ p1_latch s in
375	let old_p3_latch ≝ p3_latch s in
376	let old_clock ≝ clock s in
377	mk_Status old_code_memory
378	old_low_internal_ram
379	old_high_internal_ram
380	r
381	old_program_counter
382	old_special_function_registers_8051
383	old_special_function_registers_8052
384	old_p1_latch
385	old_p3_latch
386	old_clock.
387
388	definition get_cy_flag ≝
389	λs: Status.
390	let sfr ≝ special_function_registers_8051 s in
391	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
392	get_index_v bool 8 psw O ?.
393	normalize
394	@ (le_S_S ? ?)
395	[ @ le_O_n
396	\| repeat (@ (le_S_S));
397	//
398	]
399	qed.
400
401	definition get_ac_flag ≝
402	λs: Status.
403	let sfr ≝ special_function_registers_8051 s in
404	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
405	get_index_v bool 8 psw (S O) ?.
406	normalize
407	repeat (@ (le_S_S ? ?))
408	@ le_O_n
409	qed.
410
411	definition get_fo_flag ≝
412	λs: Status.
413	let sfr ≝ special_function_registers_8051 s in
414	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
415	get_index_v bool 8 psw 2 ?.
416	normalize
417	repeat (@ (le_S_S ? ?))
418	@ le_O_n
419	qed.
420
421	definition get_rs1_flag ≝
422	λs: Status.
423	let sfr ≝ special_function_registers_8051 s in
424	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
425	get_index_v bool 8 psw 3 ?.
426	normalize
427	repeat (@ (le_S_S ? ?))
428	@ le_O_n
429	qed.
430
431	definition get_rs0_flag ≝
432	λs: Status.
433	let sfr ≝ special_function_registers_8051 s in
434	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
435	get_index_v bool 8 psw 4 ?.
436	normalize
437	repeat (@ (le_S_S ? ?))
438	@ le_O_n
439	qed.
440
441	definition get_ov_flag ≝
442	λs: Status.
443	let sfr ≝ special_function_registers_8051 s in
444	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
445	get_index_v bool 8 psw 5 ?.
446	normalize
447	repeat (@ (le_S_S ? ?))
448	@ le_O_n
449	qed.
450
451	definition get_ud_flag ≝
452	λs: Status.
453	let sfr ≝ special_function_registers_8051 s in
454	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
455	get_index_v bool 8 psw 6 ?.
456	normalize
457	repeat (@ (le_S_S ? ?))
458	@ le_O_n
459	qed.
460
461	definition get_p_flag ≝
462	λs: Status.
463	let sfr ≝ special_function_registers_8051 s in
464	let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
465	get_index_v bool 8 psw 7 ?.
466	normalize
467	repeat (@ (le_S_S ? ?))
468	@ le_O_n
469	qed.
470
471	definition set_flags ≝
472	λs: Status.
473	λcy: Bit.
474	λac: option Bit.
475	λov: Bit.
476	let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_PSW) in
477	let old_cy ≝ get_index_v… nu O ? in
478	let old_ac ≝ get_index_v… nu 1 ? in
479	let old_fo ≝ get_index_v… nu 2 ? in
480	let old_rs1 ≝ get_index_v… nu 3 ? in
481	let old_rs0 ≝ get_index_v… nl O ? in
482	let old_ov ≝ get_index_v… nl 1 ? in
483	let old_ud ≝ get_index_v… nl 2 ? in
484	let old_p ≝ get_index_v… nl 3 ? in
485	let new_ac ≝ match ac with [ None ⇒ old_ac \| Some j ⇒ j ] in
486	let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
487	old_rs0 ; old_ov ; old_ud ; old_p ]] in
488	set_8051_sfr s SFR_PSW new_psw.
489	[1,2,3,4,5,6,7,8:
490	normalize
491	repeat (@ le_S_S)
492	@ le_O_n
493	]
494	qed.
495
496	definition initialise_status ≝
497	let status ≝ mk_Status (Stub Byte 16) (* Code mem. *)
498	(Stub Byte 7) (* Low mem. *)
499	(Stub Byte 7) (* High mem. *)
500	(Stub Byte 16) (* Ext mem. *)
501	(zero 16) (* PC. *)
502	(replicate Byte 19 (zero 8)) (* 8051 SFR. *)
503	(replicate Byte 5 (zero 8)) (* 8052 SFR. *)
504	(zero 8) (* P1 latch. *)
505	(zero 8) (* P3 latch. *)
506	O (* Clock. *)
507	in
508	set_8051_sfr status SFR_SP (bitvector_of_nat 8 7).
509
510	axiom not_implemented: False.
511
512	definition get_bit_addressable_sfr ≝
513	λs: Status.
514	λn: nat.
515	λb: BitVector n.
516	λl: bool.
517	let address ≝ nat_of_bitvector … b in
518	if (eqb address 128) then
519	?
520	else if (eqb address 144) then
521	if l then
522	(p1_latch s)
523	else
524	(get_8051_sfr s SFR_P1)
525	else if (eqb address 160) then
526	?
527	else if (eqb address 176) then
528	if l then
529	(p3_latch s)
530	else
531	(get_8051_sfr s SFR_P3)
532	else if (eqb address 153) then
533	get_8051_sfr s SFR_SBUF
534	else if (eqb address 138) then
535	get_8051_sfr s SFR_TL0
536	else if (eqb address 139) then
537	get_8051_sfr s SFR_TL1
538	else if (eqb address 140) then
539	get_8051_sfr s SFR_TH0
540	else if (eqb address 141) then
541	get_8051_sfr s SFR_TH1
542	else if (eqb address 200) then
543	get_8052_sfr s SFR_T2CON
544	else if (eqb address 202) then
545	get_8052_sfr s SFR_RCAP2L
546	else if (eqb address 203) then
547	get_8052_sfr s SFR_RCAP2H
548	else if (eqb address 204) then
549	get_8052_sfr s SFR_TL2
550	else if (eqb address 205) then
551	get_8052_sfr s SFR_TH2
552	else if (eqb address 135) then
553	get_8051_sfr s SFR_PCON
554	else if (eqb address 136) then
555	get_8051_sfr s SFR_TCON
556	else if (eqb address 137) then
557	get_8051_sfr s SFR_TMOD
558	else if (eqb address 152) then
559	get_8051_sfr s SFR_SCON
560	else if (eqb address 168) then
561	get_8051_sfr s SFR_IE
562	else if (eqb address 184) then
563	get_8051_sfr s SFR_IP
564	else if (eqb address 129) then
565	get_8051_sfr s SFR_SP
566	else if (eqb address 130) then
567	get_8051_sfr s SFR_DPL
568	else if (eqb address 131) then
569	get_8051_sfr s SFR_DPH
570	else if (eqb address 208) then
571	get_8051_sfr s SFR_PSW
572	else if (eqb address 224) then
573	get_8051_sfr s SFR_ACC_A
574	else if (eqb address 240) then
575	get_8051_sfr s SFR_ACC_B
576	else
577	?.
578	cases not_implemented
579	qed.
580
581	definition set_bit_addressable_sfr ≝
582	λs: Status.
583	λb: Byte.
584	λv: Byte.
585	let address ≝ nat_of_bitvector … b in
586	if (eqb address 128) then
587	?
588	else if (eqb address 144) then
589	let status_1 ≝ set_8051_sfr s SFR_P1 v in
590	let status_2 ≝ set_p1_latch s v in
591	status_2
592	else if (eqb address 160) then
593	?
594	else if (eqb address 176) then
595	let status_1 ≝ set_8051_sfr s SFR_P3 v in
596	let status_2 ≝ set_p3_latch s v in
597	status_2
598	else if (eqb address 153) then
599	set_8051_sfr s SFR_SBUF v
600	else if (eqb address 138) then
601	set_8051_sfr s SFR_TL0 v
602	else if (eqb address 139) then
603	set_8051_sfr s SFR_TL1 v
604	else if (eqb address 140) then
605	set_8051_sfr s SFR_TH0 v
606	else if (eqb address 141) then
607	set_8051_sfr s SFR_TH1 v
608	else if (eqb address 200) then
609	set_8052_sfr s SFR_T2CON v
610	else if (eqb address 202) then
611	set_8052_sfr s SFR_RCAP2L v
612	else if (eqb address 203) then
613	set_8052_sfr s SFR_RCAP2H v
614	else if (eqb address 204) then
615	set_8052_sfr s SFR_TL2 v
616	else if (eqb address 205) then
617	set_8052_sfr s SFR_TH2 v
618	else if (eqb address 135) then
619	set_8051_sfr s SFR_PCON v
620	else if (eqb address 136) then
621	set_8051_sfr s SFR_TCON v
622	else if (eqb address 137) then
623	set_8051_sfr s SFR_TMOD v
624	else if (eqb address 152) then
625	set_8051_sfr s SFR_SCON v
626	else if (eqb address 168) then
627	set_8051_sfr s SFR_IE v
628	else if (eqb address 184) then
629	set_8051_sfr s SFR_IP v
630	else if (eqb address 129) then
631	set_8051_sfr s SFR_SP v
632	else if (eqb address 130) then
633	set_8051_sfr s SFR_DPL v
634	else if (eqb address 131) then
635	set_8051_sfr s SFR_DPH v
636	else if (eqb address 208) then
637	set_8051_sfr s SFR_PSW v
638	else if (eqb address 224) then
639	set_8051_sfr s SFR_ACC_A v
640	else if (eqb address 240) then
641	set_8051_sfr s SFR_ACC_B v
642	else
643	?.
644	cases not_implemented
645	qed.
646
647	definition bit_address_of_register ≝
648	λs: Status.
649	λr: BitVector 3.
650	let b ≝ get_index_v … r O ? in
651	let c ≝ get_index_v … r 1 ? in
652	let d ≝ get_index_v … r 2 ? in
653	let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
654	let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in
655	let offset ≝
656	if ¬r1 ∧ ¬r0 then
657	O
658	else if ¬r1 ∧ r0 then
659	8
660	else if r1 ∧ r0 then
661	24
662	else
663	16
664	in
665	bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
666	[1,2,3,4,5:
667	normalize
668	repeat (@ le_S_S)
669	@ le_O_n;
670	]
671	qed.
672
673	definition get_register ≝
674	λs: Status.
675	λr: BitVector 3.
676	let address ≝ bit_address_of_register s r in
677	lookup … address (low_internal_ram s) (zero 8).
678
679	definition set_register ≝
680	λs: Status.
681	λr: BitVector 3.
682	λv: Byte.
683	let address ≝ bit_address_of_register s r in
684	let old_low_internal_ram ≝ low_internal_ram s in
685	let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
686	set_low_internal_ram s new_low_internal_ram.
687
688	definition read_at_stack_pointer ≝
689	λs: Status.
690	let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
691	let m ≝ get_index_v … nu O ? in
692	let r1 ≝ get_index_v … nu 1 ? in
693	let r2 ≝ get_index_v … nu 2 ? in
694	let r3 ≝ get_index_v … nu 3 ? in
695	let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
696	let memory ≝
697	if m then
698	(low_internal_ram s)
699	else
700	(high_internal_ram s)
701	in
702	lookup … address memory (zero 8).
703	[1,2,3,4:
704	normalize
705	repeat (@ le_S_S)
706	@ le_O_n
707	]
708	qed.
709
710	definition write_at_stack_pointer ≝
711	λs: Status.
712	λv: Byte.
713	let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in
714	let bit_zero ≝ get_index_v… nu O ? in
715	let bit_1 ≝ get_index_v… nu 1 ? in
716	let bit_2 ≝ get_index_v… nu 2 ? in
717	let bit_3 ≝ get_index_v… nu 3 ? in
718	if bit_zero then
719	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
720	v (low_internal_ram s) in
721	set_low_internal_ram s memory
722	else
723	let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl)
724	v (high_internal_ram s) in
725	set_high_internal_ram s memory.
726	[1,2,3,4:
727	normalize
728	repeat (@ le_S_S)
729	@ le_O_n
730	]
731	qed.
732
733	definition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
734	λs,v,a.
735	match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
736	[ DPTR ⇒ λ_:True.
737	let 〈 bu, bl 〉 ≝ split … 8 8 v in
738	let status ≝ set_8051_sfr s SFR_DPH bu in
739	let status ≝ set_8051_sfr status SFR_DPL bl in
740	status
741	\| _ ⇒ λK.
742	match K in False with
743	[
744	]
745	] (subaddressing_modein … a).
746
747	definition get_arg_16: Status → [[ data16 ]] → Word ≝
748	λs, a.
749	match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
750	[ DATA16 d ⇒ λ_:True. d
751	\| _ ⇒ λK.
752	match K in False with
753	[
754	]
755	] (subaddressing_modein … a).
756
757	definition get_arg_8: Status → bool → [[ direct ; indirect ; register ;
758	acc_a ; acc_b ; data ; acc_dptr ;
759	acc_pc ; ext_indirect ;
760	ext_indirect_dptr ]] → Byte ≝
761	λs, l, a.
762	match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
763	acc_a ; acc_b ; data ; acc_dptr ;
764	acc_pc ; ext_indirect ;
765	ext_indirect_dptr ]] x) → ? with
766	[ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
767	\| ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
768	\| DATA d ⇒ λdata: True. d
769	\| REGISTER r ⇒ λregister: True. get_register s r
770	\| EXT_INDIRECT_DPTR ⇒
771	λext_indirect_dptr: True.
772	let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
773	lookup … 16 address (external_ram s) (zero 8)
774	\| EXT_INDIRECT e ⇒
775	λext_indirect: True.
776	let address ≝ get_register s [[ false; false; e ]] in
777	let padded_address ≝ pad 8 8 address in
778	lookup … 16 padded_address (external_ram s) (zero 8)
779	\| ACC_DPTR ⇒
780	λacc_dptr: True.
781	let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
782	let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
783	let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in
784	lookup … 16 address (external_ram s) (zero 8)
785	\| ACC_PC ⇒
786	λacc_pc: True.
787	let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in
788	let 〈 carry, address 〉 ≝ half_add 16 (program_counter s) padded_acc in
789	lookup … 16 address (external_ram s) (zero 8)
790	\| DIRECT d ⇒
791	λdirect: True.
792	let 〈 nu, nl 〉 ≝ split … 4 4 d in
793	let bit_1 ≝ get_index_v … nu 1 ? in
794	match bit_1 with
795	[ true ⇒
796	let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in
797	let address ≝ three_bits @@ nl in
798	lookup ? 7 address (low_internal_ram s) (zero 8)
799	\| false ⇒ get_bit_addressable_sfr s 8 d l
800	]
801	\| INDIRECT i ⇒
802	λindirect: True.
803	let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register s [[ false; false; i]]) in
804	let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
805	let bit_1 ≝ get_index_v … bit_one_v O ? in
806	match bit_1 with
807	[ true ⇒
808	lookup ? 7 (three_bits @@ nl) (low_internal_ram s) (zero 8)
809	\| false ⇒
810	lookup ? 7 (three_bits @@ nl) (high_internal_ram s) (zero 8)
811	]
812	\| _ ⇒ λother.
813	match other in False with [ ]
814	] (subaddressing_modein … a).
815	[1,2:
816	normalize
817	repeat (@ le_S_S)
818	@ le_O_n
819	]
820	qed.
821
822	definition set_arg_8: Status → [[ direct ; indirect ; register ;
823	acc_a ; acc_b ; ext_indirect ;
824	ext_indirect_dptr ]] → Byte → Status ≝
825	λs, a, v.
826	match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
827	acc_a ; acc_b ; ext_indirect ;
828	ext_indirect_dptr ]] x) → ? with
829	[ DIRECT d ⇒
830	λdirect: True.
831	let 〈 nu, nl 〉 ≝ split … 4 4 d in
832	let bit_1 ≝ get_index_v … nu 1 ? in
833	let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
834	match bit_1 with
835	[ true ⇒ set_bit_addressable_sfr s d v
836	\| false ⇒
837	let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in
838	set_low_internal_ram s memory
839	]
840	\| INDIRECT i ⇒
841	λindirect: True.
842	let register ≝ get_register s [[ false; false; i ]] in
843	let 〈nu, nl〉 ≝ split ? 4 4 register in
844	let bit_1 ≝ get_index_v … nu 1 ? in
845	let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
846	match bit_1 with
847	[ true ⇒
848	let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
849	set_low_internal_ram s memory
850	\| false ⇒
851	let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
852	set_high_internal_ram s memory
853	]
854	\| REGISTER r ⇒ λregister: True. set_register s r v
855	\| ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
856	\| ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
857	\| EXT_INDIRECT e ⇒
858	λext_indirect: True.
859	let address ≝ get_register s [[ false; false; e ]] in
860	let padded_address ≝ pad 8 8 address in
861	let memory ≝ insert ? 16 padded_address v (external_ram s) in
862	set_external_ram s memory
863	\| EXT_INDIRECT_DPTR ⇒
864	λext_indirect_dptr: True.
865	let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
866	let memory ≝ insert ? 16 address v (external_ram s) in
867	set_external_ram s memory
868	\| _ ⇒
869	λother: False.
870	match other in False with [ ]
871	] (subaddressing_modein … a).
872	[1,2,3,4:
873	normalize
874	repeat (@ le_S_S)
875	@ le_O_n
876	]
877	qed.
878
879	theorem modulus_less_than:
880	∀m,n: nat. (m mod (S n)) < S n.
881	#n #m
882	normalize
883	@ le_S_S
884	lapply (le_n n)
885	generalize in ⊢ (?%? → ?(??%?)?)
886	elim n in ⊢ (∀_:?. ??% → ?(?%??)?)
887	[ normalize
888	#n
889	@ (less_than_or_equal_b_elim n m)
890	normalize
891	[ //
892	\| #H #K
893	inversion K
894	[ # H1
895	< H1
896	//
897	\| #x #H1 #H2 #H3
898	destruct
899	]
900	]
901	\| normalize
902	# y # H1 # n # H2
903	@ (less_than_or_equal_b_elim n m)
904	normalize
905	[ //
906	\| # K
907	@ H1
908	cut (n ≤ S y → n - S m ≤ y)
909	/2/
910	cases n
911	normalize
912	//
913	# x # K1
914	lapply (le_S_S_to_le … K1)
915	generalize in match m
916	elim x
917	normalize
918	//
919	# w1 # H # m
920	cases m
921	normalize
922	//
923	# q # K2
924	apply H
925	/3/
926	]
927	]
928	qed.
929
930	definition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
931	bool → bool ≝
932	λs, a, l.
933	match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
934	n_bit_addr ;
935	carry ]] x) → ? with
936	[ BIT_ADDR b ⇒
937	λbit_addr: True.
938	let 〈 nu, nl 〉 ≝ split … 4 4 b in
939	let bit_1 ≝ get_index_v … nu 1 ? in
940	let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
941	match bit_1 with
942	[ true ⇒
943	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
944	let d ≝ address ÷ 8 in
945	let m ≝ address mod 8 in
946	let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
947	let sfr ≝ get_bit_addressable_sfr s ? trans l in
948	get_index_v … sfr m ?
949	\| false ⇒
950	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
951	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
952	let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
953	get_index_v … t (modulus address 8) ?
954	]
955	\| N_BIT_ADDR n ⇒
956	λn_bit_addr: True.
957	let 〈 nu, nl 〉 ≝ split … 4 4 n in
958	let bit_1 ≝ get_index_v … nu 1 ? in
959	let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
960	match bit_1 with
961	[ true ⇒
962	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
963	let d ≝ address ÷ 8 in
964	let m ≝ address mod 8 in
965	let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in
966	let sfr ≝ get_bit_addressable_sfr s ? trans l in
967	¬(get_index_v … sfr m ?)
968	\| false ⇒
969	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
970	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
971	let trans ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
972	¬(get_index_v … trans (modulus address 8) ?)
973	]
974	\| CARRY ⇒ λcarry: True. get_cy_flag s
975	\| _ ⇒ λother.
976	match other in False with [ ]
977	] (subaddressing_modein … a).
978	[3,6:
979	normalize
980	repeat (@ le_S_S)
981	@ le_O_n
982	\|1,2,4,5:
983	apply modulus_less_than
984	]
985	qed.
986
987	definition set_arg_1: Status → [[ bit_addr ; carry ]] →
988	Bit → Status ≝
989	λs, a, v.
990	match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
991	[ BIT_ADDR b ⇒ λbit_addr: True.
992	let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
993	let bit_1 ≝ get_index_v … nu 1 ? in
994	let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
995	match bit_1 with
996	[ true ⇒
997	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
998	let d ≝ address ÷ 8 in
999	let m ≝ address mod 8 in
1000	let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in
1001	let sfr ≝ get_bit_addressable_sfr s ? t true in
1002	let new_sfr ≝ set_index … sfr m v ? in
1003	set_bit_addressable_sfr s new_sfr t
1004	\| false ⇒
1005	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
1006	let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in
1007	let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in
1008	let n_bit ≝ set_index … t (modulus address 8) v ? in
1009	let memory ≝ insert ? 7 address' n_bit (low_internal_ram s) in
1010	set_low_internal_ram s memory
1011	]
1012	\| CARRY ⇒
1013	λcarry: True.
1014	let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in
1015	let bit_1 ≝ get_index_v… nu 1 ? in
1016	let bit_2 ≝ get_index_v… nu 2 ? in
1017	let bit_3 ≝ get_index_v… nu 3 ? in
1018	let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in
1019	set_8051_sfr s SFR_PSW new_psw
1020	\| _ ⇒
1021	λother: False.
1022	match other in False with
1023	[ ]
1024	] (subaddressing_modein … a).
1025	[1,2,3,6:
1026	normalize
1027	repeat (@ le_S_S)
1028	@ le_O_n
1029	\|4,5:
1030	@ modulus_less_than
1031	]
1032	qed.
1033
1034	definition load_code_memory ≝
1035	fold_left_i … (
1036	λi, mem, v.
1037	insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
1038
1039	definition load ≝
1040	λl, status.
1041	set_code_memory status (load_code_memory l).

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format