Context Navigation

Status.ma @ 358

Last change on this file since 358 was 357, checked in by sacerdot, 10 years ago
stupid bug fixed in BitVectorTrie? dependencies minimized, dead code removed
File size: 38.3 KB

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

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

Download in other formats:

Original Format