Context Navigation

Status.ma @ 317

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

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

Download in other formats:

Original Format