Context Navigation

Status.ma @ 330

Last change on this file since 330 was 329, checked in by mulligan, 10 years ago
Commit to restore deleted file.
File size: 38.2 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	naxiom sfr8051_index_nineteen:
106	∀i: SFR8051.
107	sfr_8051_index i < nineteen.
108
109	naxiom sfr8052_index_five:
110	∀i: SFR8052.
111	sfr_8052_index i < five.
112
113	ndefinition set_clock ≝
114	λs: Status.
115	λt: Time.
116	let old_code_memory ≝ code_memory s in
117	let old_low_internal_ram ≝ low_internal_ram s in
118	let old_high_internal_ram ≝ high_internal_ram s in
119	let old_external_ram ≝ external_ram s in
120	let old_program_counter ≝ program_counter s in
121	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
122	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
123	let old_p1_latch ≝ p1_latch s in
124	let old_p3_latch ≝ p3_latch s in
125	mk_Status old_code_memory
126	old_low_internal_ram
127	old_high_internal_ram
128	old_external_ram
129	old_program_counter
130	old_special_function_registers_8051
131	old_special_function_registers_8052
132	old_p1_latch
133	old_p3_latch
134	t.
135
136	ndefinition set_p1_latch ≝
137	λs: Status.
138	λb: Byte.
139	let old_code_memory ≝ code_memory s in
140	let old_low_internal_ram ≝ low_internal_ram s in
141	let old_high_internal_ram ≝ high_internal_ram s in
142	let old_external_ram ≝ external_ram s in
143	let old_program_counter ≝ program_counter s in
144	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
145	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
146	let old_p3_latch ≝ p3_latch s in
147	let old_clock ≝ clock s in
148	mk_Status old_code_memory
149	old_low_internal_ram
150	old_high_internal_ram
151	old_external_ram
152	old_program_counter
153	old_special_function_registers_8051
154	old_special_function_registers_8052
155	b
156	old_p3_latch
157	old_clock.
158
159	ndefinition set_p3_latch ≝
160	λs: Status.
161	λb: Byte.
162	let old_code_memory ≝ code_memory s in
163	let old_low_internal_ram ≝ low_internal_ram s in
164	let old_high_internal_ram ≝ high_internal_ram s in
165	let old_external_ram ≝ external_ram s in
166	let old_program_counter ≝ program_counter s in
167	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
168	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
169	let old_p1_latch ≝ p1_latch s in
170	let old_clock ≝ clock s in
171	mk_Status old_code_memory
172	old_low_internal_ram
173	old_high_internal_ram
174	old_external_ram
175	old_program_counter
176	old_special_function_registers_8051
177	old_special_function_registers_8052
178	old_p1_latch
179	b
180	old_clock.
181
182	ndefinition get_8051_sfr ≝
183	λs: Status.
184	λi: SFR8051.
185	let sfr ≝ special_function_registers_8051 s in
186	let index ≝ sfr_8051_index i in
187	get_index … sfr index ?.
188	napply (sfr8051_index_nineteen i).
189	nqed.
190
191	ndefinition get_8052_sfr ≝
192	λs: Status.
193	λi: SFR8052.
194	let sfr ≝ special_function_registers_8052 s in
195	let index ≝ sfr_8052_index i in
196	get_index … sfr index ?.
197	napply (sfr8052_index_five i).
198	nqed.
199
200	ndefinition set_8051_sfr ≝
201	λs: Status.
202	λi: SFR8051.
203	λb: Byte.
204	let index ≝ sfr_8051_index i in
205	let old_code_memory ≝ code_memory s in
206	let old_low_internal_ram ≝ low_internal_ram s in
207	let old_high_internal_ram ≝ high_internal_ram s in
208	let old_external_ram ≝ external_ram s in
209	let old_program_counter ≝ program_counter s in
210	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
211	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
212	let new_special_function_registers_8051 ≝
213	cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte nineteen old_special_function_registers_8051 index b ? in
214	let old_p1_latch ≝ p1_latch s in
215	let old_p3_latch ≝ p3_latch s in
216	let old_clock ≝ clock s in
217	mk_Status old_code_memory
218	old_low_internal_ram
219	old_high_internal_ram
220	old_external_ram
221	old_program_counter
222	new_special_function_registers_8051
223	old_special_function_registers_8052
224	old_p1_latch
225	old_p3_latch
226	old_clock.
227	napply (sfr8051_index_nineteen i).
228	nqed.
229
230	ndefinition set_8052_sfr ≝
231	λs: Status.
232	λi: SFR8052.
233	λb: Byte.
234	let index ≝ sfr_8052_index i in
235	let old_code_memory ≝ code_memory s in
236	let old_low_internal_ram ≝ low_internal_ram s in
237	let old_high_internal_ram ≝ high_internal_ram s in
238	let old_external_ram ≝ external_ram s in
239	let old_program_counter ≝ program_counter s in
240	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
241	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
242	let new_special_function_registers_8052 ≝
243	cic:/matita/ng/Vector/set_index.fix(0,3,2) Byte five old_special_function_registers_8052 index b ? in
244	let old_p1_latch ≝ p1_latch s in
245	let old_p3_latch ≝ p3_latch s in
246	let old_clock ≝ clock s in
247	mk_Status old_code_memory
248	old_low_internal_ram
249	old_high_internal_ram
250	old_external_ram
251	old_program_counter
252	old_special_function_registers_8051
253	new_special_function_registers_8052
254	old_p1_latch
255	old_p3_latch
256	old_clock.
257	napply (sfr8052_index_five i).
258	nqed.
259
260	ndefinition set_program_counter ≝
261	λs: Status.
262	λw: Word.
263	let old_code_memory ≝ code_memory s in
264	let old_low_internal_ram ≝ low_internal_ram s in
265	let old_high_internal_ram ≝ high_internal_ram s in
266	let old_external_ram ≝ external_ram s in
267	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
268	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
269	let old_p1_latch ≝ p1_latch s in
270	let old_p3_latch ≝ p3_latch s in
271	let old_clock ≝ clock s in
272	mk_Status old_code_memory
273	old_low_internal_ram
274	old_high_internal_ram
275	old_external_ram
276	w
277	old_special_function_registers_8051
278	old_special_function_registers_8052
279	old_p1_latch
280	old_p3_latch
281	old_clock.
282
283	ndefinition set_code_memory ≝
284	λs: Status.
285	λr: BitVectorTrie Byte sixteen.
286	let old_low_internal_ram ≝ low_internal_ram s in
287	let old_high_internal_ram ≝ high_internal_ram s in
288	let old_external_ram ≝ external_ram s in
289	let old_program_counter ≝ program_counter s in
290	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
291	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
292	let old_p1_latch ≝ p1_latch s in
293	let old_p3_latch ≝ p3_latch s in
294	let old_clock ≝ clock s in
295	mk_Status r
296	old_low_internal_ram
297	old_high_internal_ram
298	old_external_ram
299	old_program_counter
300	old_special_function_registers_8051
301	old_special_function_registers_8052
302	old_p1_latch
303	old_p3_latch
304	old_clock.
305
306	ndefinition set_low_internal_ram ≝
307	λs: Status.
308	λr: BitVectorTrie Byte seven.
309	let old_code_memory ≝ code_memory s in
310	let old_high_internal_ram ≝ high_internal_ram s in
311	let old_external_ram ≝ external_ram s in
312	let old_program_counter ≝ program_counter s in
313	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
314	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
315	let old_p1_latch ≝ p1_latch s in
316	let old_p3_latch ≝ p3_latch s in
317	let old_clock ≝ clock s in
318	mk_Status old_code_memory
319	r
320	old_high_internal_ram
321	old_external_ram
322	old_program_counter
323	old_special_function_registers_8051
324	old_special_function_registers_8052
325	old_p1_latch
326	old_p3_latch
327	old_clock.
328
329	ndefinition set_high_internal_ram ≝
330	λs: Status.
331	λr: BitVectorTrie Byte seven.
332	let old_code_memory ≝ code_memory s in
333	let old_low_internal_ram ≝ low_internal_ram s in
334	let old_high_internal_ram ≝ high_internal_ram s in
335	let old_external_ram ≝ external_ram s in
336	let old_program_counter ≝ program_counter s in
337	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
338	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
339	let old_p1_latch ≝ p1_latch s in
340	let old_p3_latch ≝ p3_latch s in
341	let old_clock ≝ clock s in
342	mk_Status old_code_memory
343	old_low_internal_ram
344	r
345	old_external_ram
346	old_program_counter
347	old_special_function_registers_8051
348	old_special_function_registers_8052
349	old_p1_latch
350	old_p3_latch
351	old_clock.
352
353	ndefinition set_external_ram ≝
354	λs: Status.
355	λr: BitVectorTrie Byte sixteen.
356	let old_code_memory ≝ code_memory s in
357	let old_low_internal_ram ≝ low_internal_ram s in
358	let old_high_internal_ram ≝ high_internal_ram s in
359	let old_program_counter ≝ program_counter s in
360	let old_special_function_registers_8051 ≝ special_function_registers_8051 s in
361	let old_special_function_registers_8052 ≝ special_function_registers_8052 s in
362	let old_p1_latch ≝ p1_latch s in
363	let old_p3_latch ≝ p3_latch s in
364	let old_clock ≝ clock s in
365	mk_Status old_code_memory
366	old_low_internal_ram
367	old_high_internal_ram
368	r
369	old_program_counter
370	old_special_function_registers_8051
371	old_special_function_registers_8052
372	old_p1_latch
373	old_p3_latch
374	old_clock.
375
376	naxiom less_than_or_equal_monotone:
377	∀m, n: Nat.
378	m ≤ n → S m ≤ S n.
379
380	alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
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_program_counter status (bitvector_of_nat sixteen seven).
516
517	naxiom not_implemented: False.
518
519	include "Arithmetic.ma".
520
521	ndefinition get_bit_addressable_sfr ≝
522	λs: Status.
523	λn: Nat.
524	λb: BitVector n.
525	λl: Bool.
526	let address ≝ nat_of_bitvector … b in
527	if (decidable_equality address one_hundred_and_twenty_eight) then
528	?
529	else if (decidable_equality address one_hundred_and_forty_four) then
530	if l then
531	(p1_latch s)
532	else
533	(get_8051_sfr s SFR_P1)
534	else if (decidable_equality address one_hundred_and_sixty) then
535	?
536	else if (decidable_equality address one_hundred_and_seventy_six) then
537	if l then
538	(p3_latch s)
539	else
540	(get_8051_sfr s SFR_P3)
541	else if (decidable_equality address one_hundred_and_fifty_three) then
542	get_8051_sfr s SFR_SBUF
543	else if (decidable_equality address one_hundred_and_thirty_eight) then
544	get_8051_sfr s SFR_TL0
545	else if (decidable_equality address one_hundred_and_thirty_nine) then
546	get_8051_sfr s SFR_TL1
547	else if (decidable_equality address one_hundred_and_forty) then
548	get_8051_sfr s SFR_TH0
549	else if (decidable_equality address one_hundred_and_forty_one) then
550	get_8051_sfr s SFR_TH1
551	else if (decidable_equality address two_hundred) then
552	get_8052_sfr s SFR_T2CON
553	else if (decidable_equality address two_hundred_and_two) then
554	get_8052_sfr s SFR_RCAP2L
555	else if (decidable_equality address two_hundred_and_three) then
556	get_8052_sfr s SFR_RCAP2H
557	else if (decidable_equality address two_hundred_and_four) then
558	get_8052_sfr s SFR_TL2
559	else if (decidable_equality address two_hundred_and_five) then
560	get_8052_sfr s SFR_TH2
561	else if (decidable_equality address one_hundred_and_thirty_five) then
562	get_8051_sfr s SFR_PCON
563	else if (decidable_equality address one_hundred_and_thirty_six) then
564	get_8051_sfr s SFR_TCON
565	else if (decidable_equality address one_hundred_and_thirty_seven) then
566	get_8051_sfr s SFR_TMOD
567	else if (decidable_equality address one_hundred_and_fifty_two) then
568	get_8051_sfr s SFR_SCON
569	else if (decidable_equality address one_hundred_and_sixty_eight) then
570	get_8051_sfr s SFR_IE
571	else if (decidable_equality address one_hundred_and_eighty_four) then
572	get_8051_sfr s SFR_IP
573	else if (decidable_equality address one_hundred_and_twenty_nine) then
574	get_8051_sfr s SFR_SP
575	else if (decidable_equality address one_hundred_and_thirty) then
576	get_8051_sfr s SFR_DPL
577	else if (decidable_equality address one_hundred_and_thirty_one) then
578	get_8051_sfr s SFR_DPH
579	else if (decidable_equality address two_hundred_and_eight) then
580	get_8051_sfr s SFR_PSW
581	else if (decidable_equality address two_hundred_and_twenty_four) then
582	get_8051_sfr s SFR_ACC_A
583	else if (decidable_equality address two_hundred_and_forty) then
584	get_8051_sfr s SFR_ACC_B
585	else
586	?.
587	ncases not_implemented.
588	nqed.
589
590	ndefinition set_bit_addressable_sfr ≝
591	λs: Status.
592	λb: Byte.
593	λv: Byte.
594	let address ≝ nat_of_bitvector … b in
595	if (decidable_equality address one_hundred_and_twenty_eight) then
596	?
597	else if (decidable_equality address one_hundred_and_forty_four) then
598	let status_1 ≝ set_8051_sfr s SFR_P1 v in
599	let status_2 ≝ set_p1_latch s v in
600	status_2
601	else if (decidable_equality address one_hundred_and_sixty) then
602	?
603	else if (decidable_equality address one_hundred_and_seventy_six) then
604	let status_1 ≝ set_8051_sfr s SFR_P3 v in
605	let status_2 ≝ set_p3_latch s v in
606	status_2
607	else if (decidable_equality address one_hundred_and_fifty_three) then
608	set_8051_sfr s SFR_SBUF v
609	else if (decidable_equality address one_hundred_and_thirty_eight) then
610	set_8051_sfr s SFR_TL0 v
611	else if (decidable_equality address one_hundred_and_thirty_nine) then
612	set_8051_sfr s SFR_TL1 v
613	else if (decidable_equality address one_hundred_and_forty) then
614	set_8051_sfr s SFR_TH0 v
615	else if (decidable_equality address one_hundred_and_forty_one) then
616	set_8051_sfr s SFR_TH1 v
617	else if (decidable_equality address two_hundred) then
618	set_8052_sfr s SFR_T2CON v
619	else if (decidable_equality address two_hundred_and_two) then
620	set_8052_sfr s SFR_RCAP2L v
621	else if (decidable_equality address two_hundred_and_three) then
622	set_8052_sfr s SFR_RCAP2H v
623	else if (decidable_equality address two_hundred_and_four) then
624	set_8052_sfr s SFR_TL2 v
625	else if (decidable_equality address two_hundred_and_five) then
626	set_8052_sfr s SFR_TH2 v
627	else if (decidable_equality address one_hundred_and_thirty_five) then
628	set_8051_sfr s SFR_PCON v
629	else if (decidable_equality address one_hundred_and_thirty_six) then
630	set_8051_sfr s SFR_TCON v
631	else if (decidable_equality address one_hundred_and_thirty_seven) then
632	set_8051_sfr s SFR_TMOD v
633	else if (decidable_equality address one_hundred_and_fifty_two) then
634	set_8051_sfr s SFR_SCON v
635	else if (decidable_equality address one_hundred_and_sixty_eight) then
636	set_8051_sfr s SFR_IE v
637	else if (decidable_equality address one_hundred_and_eighty_four) then
638	set_8051_sfr s SFR_IP v
639	else if (decidable_equality address one_hundred_and_twenty_nine) then
640	set_8051_sfr s SFR_SP v
641	else if (decidable_equality address one_hundred_and_thirty) then
642	set_8051_sfr s SFR_DPL v
643	else if (decidable_equality address one_hundred_and_thirty_one) then
644	set_8051_sfr s SFR_DPH v
645	else if (decidable_equality address two_hundred_and_eight) then
646	set_8051_sfr s SFR_PSW v
647	else if (decidable_equality address two_hundred_and_twenty_four) then
648	set_8051_sfr s SFR_ACC_A v
649	else if (decidable_equality address two_hundred_and_forty) then
650	set_8051_sfr s SFR_ACC_B v
651	else
652	?.
653	ncases not_implemented.
654	nqed.
655
656	ndefinition bit_address_of_register ≝
657	λs: Status.
658	λr: BitVector three.
659	let b ≝ get_index ? r Z ? in
660	let c ≝ get_index ? r one ? in
661	let d ≝ get_index ? r two ? in
662	let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
663	let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
664	let offset ≝
665	if conjunction (negation r1) (negation r0) then
666	Z
667	else if conjunction (negation r1) r0 then
668	eight
669	else if conjunction r1 r0 then
670	twenty_four
671	else
672	sixteen
673	in
674	bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
675	##[##1,2,3,4,5:
676	nnormalize;
677	nrepeat (napply less_than_or_equal_monotone);
678	napply less_than_or_equal_zero;
679	##]
680	nqed.
681
682	ndefinition get_register ≝
683	λs: Status.
684	λr: BitVector three.
685	let address ≝ bit_address_of_register s r in
686	lookup … address (low_internal_ram s) (zero eight).
687
688	ndefinition set_register ≝
689	λs: Status.
690	λr: BitVector three.
691	λv: Byte.
692	let address ≝ bit_address_of_register s r in
693	let old_low_internal_ram ≝ low_internal_ram s in
694	let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
695	set_low_internal_ram s new_low_internal_ram.
696
697	alias id "get_index" = "cic:/matita/ng/BitVector/get_index.def(3)".
698	ndefinition read_at_stack_pointer ≝
699	λs: Status.
700	let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
701	let m ≝ get_index … nu Z ? in
702	let r1 ≝ get_index … nu one ? in
703	let r2 ≝ get_index … nu two ? in
704	let r3 ≝ get_index … nu three ? in
705	let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
706	let memory ≝
707	if m then
708	(low_internal_ram s)
709	else
710	(high_internal_ram s)
711	in
712	lookup … address memory (zero eight).
713	##[##1,2,3,4:
714	nnormalize;
715	nrepeat (napply less_than_or_equal_monotone);
716	napply less_than_or_equal_zero;
717	##]
718	nqed.
719
720	ndefinition write_at_stack_pointer ≝
721	λs: Status.
722	λv: Byte.
723	let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
724	let bit_zero ≝ get_index … nu Z ? in
725	let bit_one ≝ get_index … nu one ? in
726	let bit_two ≝ get_index … nu two ? in
727	let bit_three ≝ get_index … nu three ? in
728	if bit_zero then
729	let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
730	v (low_internal_ram s) in
731	set_low_internal_ram s memory
732	else
733	let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
734	v (high_internal_ram s) in
735	set_high_internal_ram s memory.
736	##[##1,2,3,4:
737	nnormalize;
738	nrepeat (napply less_than_or_equal_monotone);
739	napply less_than_or_equal_zero;
740	##]
741	nqed.
742
743	ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
744	λs,v,a.
745	match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
746	[ DPTR ⇒ λ_:True.
747	let 〈 bu, bl 〉 ≝ split … eight eight v in
748	let status ≝ set_8051_sfr s SFR_DPH bu in
749	let status ≝ set_8051_sfr status SFR_DPL bl in
750	status
751	\| _ ⇒ λK.
752	match K in False with
753	[
754	]
755	] (subaddressing_modein … a).
756
757	ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝
758	λs, a.
759	match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
760	[ DATA16 d ⇒ λ_:True. d
761	\| _ ⇒ λK.
762	match K in False with
763	[
764	]
765	] (subaddressing_modein … a).
766
767	ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;
768	acc_a ; acc_b ; data ; acc_dptr ;
769	acc_pc ; ext_indirect ;
770	ext_indirect_dptr ]] → Byte ≝
771	λs, l, a.
772	match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
773	acc_a ; acc_b ; data ; acc_dptr ;
774	acc_pc ; ext_indirect ;
775	ext_indirect_dptr ]] x) → ? with
776	[ ACC_A ⇒ λacc_a: True. get_8051_sfr s SFR_ACC_A
777	\| ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
778	\| DATA d ⇒ λdata: True. d
779	\| REGISTER r ⇒ λregister: True. get_register s r
780	\| EXT_INDIRECT_DPTR ⇒
781	λext_indirect_dptr: True.
782	let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
783	lookup … sixteen address (external_ram s) (zero eight)
784	\| EXT_INDIRECT e ⇒
785	λext_indirect: True.
786	let address ≝ get_register s [[ false; false; e ]] in
787	let padded_address ≝ pad eight eight address in
788	lookup … sixteen padded_address (external_ram s) (zero eight)
789	\| ACC_DPTR ⇒
790	λacc_dptr: True.
791	let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
792	let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
793	let 〈 carry, address 〉 ≝ half_add sixteen dptr padded_acc in
794	lookup … sixteen address (external_ram s) (zero eight)
795	\| ACC_PC ⇒
796	λacc_pc: True.
797	let padded_acc ≝ pad eight eight (get_8051_sfr s SFR_ACC_A) in
798	let 〈 carry, address 〉 ≝ half_add sixteen (program_counter s) padded_acc in
799	lookup … sixteen address (external_ram s) (zero eight)
800	\| DIRECT d ⇒
801	λdirect: True.
802	let 〈 nu, nl 〉 ≝ split … four four d in
803	let bit_one ≝ get_index … nu one ? in
804	match bit_one with
805	[ true ⇒
806	let 〈 bit_one, three_bits 〉 ≝ split ? one three nu in
807	let address ≝ three_bits @@ nl in
808	lookup ? seven address (low_internal_ram s) (zero eight)
809	\| false ⇒ get_bit_addressable_sfr s eight d l
810	]
811	\| INDIRECT i ⇒
812	λindirect: True.
813	let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in
814	let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
815	let bit_one ≝ get_index … bit_one_v Z ? in
816	match bit_one with
817	[ true ⇒
818	lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)
819	\| false ⇒
820	lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)
821	]
822	\| _ ⇒ λother.
823	match other in False with [ ]
824	] (subaddressing_modein … a).
825	##[##1,2:
826	nnormalize;
827	nrepeat (napply less_than_or_equal_monotone);
828	napply less_than_or_equal_zero;
829	##]
830	nqed.
831
832	ndefinition set_arg_8: Status → [[ direct ; indirect ; register ;
833	acc_a ; acc_b ; ext_indirect ;
834	ext_indirect_dptr ]] → Byte → Status ≝
835	λs, a, v.
836	match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
837	acc_a ; acc_b ; ext_indirect ;
838	ext_indirect_dptr ]] x) → ? with
839	[ DIRECT d ⇒
840	λdirect: True.
841	let 〈 nu, nl 〉 ≝ split … four four d in
842	let bit_one ≝ get_index … nu one ? in
843	let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
844	match bit_one with
845	[ true ⇒ set_bit_addressable_sfr s d v
846	\| false ⇒
847	let memory ≝ insert ? seven (three_bits @@ nl) v (low_internal_ram s) in
848	set_low_internal_ram s memory
849	]
850	\| INDIRECT i ⇒
851	λindirect: True.
852	let register ≝ get_register s [[ false; false; i ]] in
853	let 〈 nu, nl 〉 ≝ split ? four four register in
854	let bit_one ≝ get_index ? nu one ? in
855	let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
856	match bit_one with
857	[ true ⇒
858	let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in
859	set_low_internal_ram s memory
860	\| false ⇒
861	let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram s) in
862	set_high_internal_ram s memory
863	]
864	\| REGISTER r ⇒ λregister: True. set_register s r v
865	\| ACC_A ⇒ λacc_a: True. set_8051_sfr s SFR_ACC_A v
866	\| ACC_B ⇒ λacc_b: True. set_8051_sfr s SFR_ACC_B v
867	\| EXT_INDIRECT e ⇒
868	λext_indirect: True.
869	let address ≝ get_register s [[ false; false; e ]] in
870	let padded_address ≝ pad eight eight address in
871	let memory ≝ insert ? sixteen padded_address v (external_ram s) in
872	set_external_ram s memory
873	\| EXT_INDIRECT_DPTR ⇒
874	λext_indirect_dptr: True.
875	let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in
876	let memory ≝ insert ? sixteen address v (external_ram s) in
877	set_external_ram s memory
878	\| _ ⇒
879	λother: False.
880	match other in False with [ ]
881	] (subaddressing_modein … a).
882	##[##1,2:
883	nnormalize;
884	nrepeat (napply less_than_or_equal_monotone);
885	napply less_than_or_equal_zero
886	##]
887	nqed.
888
889	naxiom modulus_less_than:
890	∀m,n: Nat.
891	(m mod n) < n.
892
893	ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] →
894	Bool → Bool ≝
895	λs, a, l.
896	match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;
897	n_bit_addr ;
898	carry ]] x) → ? with
899	[ BIT_ADDR b ⇒
900	λbit_addr: True.
901	let 〈 nu, nl 〉 ≝ split … four four b in
902	let bit_one ≝ get_index … nu one ? in
903	let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
904	match bit_one with
905	[ true ⇒
906	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
907	let d ≝ address ÷ eight in
908	let m ≝ address mod eight in
909	let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
910	let sfr ≝ get_bit_addressable_sfr s ? trans l in
911	get_index ? sfr m ?
912	\| false ⇒
913	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
914	let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
915	let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
916	get_index ? t (modulus address eight) ?
917	]
918	\| N_BIT_ADDR n ⇒
919	λn_bit_addr: True.
920	let 〈 nu, nl 〉 ≝ split … four four n in
921	let bit_one ≝ get_index … nu one ? in
922	let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in
923	match bit_one with
924	[ true ⇒
925	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
926	let d ≝ address ÷ eight in
927	let m ≝ address mod eight in
928	let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
929	let sfr ≝ get_bit_addressable_sfr s ? trans l in
930	negation (get_index ? sfr m ?)
931	\| false ⇒
932	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
933	let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
934	let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
935	negation (get_index ? trans (modulus address eight) ?)
936	]
937	\| CARRY ⇒ λcarry: True. get_cy_flag s
938	\| _ ⇒ λother.
939	match other in False with [ ]
940	] (subaddressing_modein … a).
941	##[##3,6:
942	nnormalize;
943	nrepeat (napply less_than_or_equal_monotone);
944	napply less_than_or_equal_zero;
945	##\|##1,2,4,5:
946	napply modulus_less_than;
947	##]
948	nqed.
949
950	ndefinition set_arg_1: Status → [[ bit_addr ; carry ]] →
951	Bit → Status ≝
952	λs, a, v.
953	match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with
954	[ BIT_ADDR b ⇒ λbit_addr: True.
955	let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
956	let bit_one ≝ get_index ? nu one ? in
957	let 〈 ignore, three_bits 〉 ≝ split ? one three nu in
958	match bit_one with
959	[ true ⇒
960	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
961	let d ≝ address ÷ eight in
962	let m ≝ address mod eight in
963	let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in
964	let sfr ≝ get_bit_addressable_sfr s ? t true in
965	let new_sfr ≝ set_index … sfr m v ? in
966	set_bit_addressable_sfr s new_sfr t
967	\| false ⇒
968	let address ≝ nat_of_bitvector … (three_bits @@ nl) in
969	let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in
970	let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in
971	let n_bit ≝ set_index … t (modulus address eight) v ? in
972	let memory ≝ insert ? seven address' n_bit (low_internal_ram s) in
973	set_low_internal_ram s memory
974	]
975	\| CARRY ⇒
976	λcarry: True.
977	let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
978	let bit_one ≝ get_index … nu one ? in
979	let bit_two ≝ get_index … nu two ? in
980	let bit_three ≝ get_index … nu three ? in
981	let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in
982	set_8051_sfr s SFR_PSW new_psw
983	\| _ ⇒
984	λother: False.
985	match other in False with
986	[ ]
987	] (subaddressing_modein … a).
988	##[##1,2,3,6:
989	nnormalize;
990	nrepeat (napply less_than_or_equal_monotone);
991	napply less_than_or_equal_zero;
992	##\|##4,5:
993	napply (modulus_less_than address eight);
994	##]
995	nqed.

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

Download in other formats:

Original Format