Context Navigation

Status.ma @ 294

Last change on this file since 294 was 294, checked in by mulligan, 10 years ago
get and set_arg_16 implemented.
File size: 25.1 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	naxiom less_than_or_equal_monotone:
313	∀m, n: Nat.
314	m ≤ n → S m ≤ S n.
315
316	alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
317
318	ndefinition get_cy_flag ≝
319	λs: Status.
320	let sfr ≝ special_function_registers_8051 s in
321	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
322	get_index Bool eight psw Z ?.
323	nnormalize.
324	napply (less_than_or_equal_monotone ? ?).
325	napply (less_than_or_equal_zero).
326	nrepeat (napply (less_than_or_equal_monotone ? ?)).
327	napply (less_than_or_equal_zero).
328	nqed.
329
330	ndefinition get_ac_flag ≝
331	λs: Status.
332	let sfr ≝ special_function_registers_8051 s in
333	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
334	get_index Bool eight psw (S Z) ?.
335	nnormalize.
336	nrepeat (napply (less_than_or_equal_monotone ? ?)).
337	napply (less_than_or_equal_zero).
338	nrepeat (napply (less_than_or_equal_monotone ? ?)).
339	napply (less_than_or_equal_zero).
340	nqed.
341
342	ndefinition get_fo_flag ≝
343	λs: Status.
344	let sfr ≝ special_function_registers_8051 s in
345	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
346	get_index Bool eight psw two ?.
347	nnormalize.
348	nrepeat (napply (less_than_or_equal_monotone ? ?)).
349	napply (less_than_or_equal_zero).
350	nrepeat (napply (less_than_or_equal_monotone ? ?)).
351	napply (less_than_or_equal_zero).
352	nqed.
353
354	ndefinition get_rs1_flag ≝
355	λs: Status.
356	let sfr ≝ special_function_registers_8051 s in
357	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
358	get_index Bool eight psw three ?.
359	nnormalize.
360	nrepeat (napply (less_than_or_equal_monotone ? ?)).
361	napply (less_than_or_equal_zero).
362	nrepeat (napply (less_than_or_equal_monotone ? ?)).
363	napply (less_than_or_equal_zero).
364	nqed.
365
366	ndefinition get_rs0_flag ≝
367	λs: Status.
368	let sfr ≝ special_function_registers_8051 s in
369	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
370	get_index Bool eight psw four ?.
371	nnormalize.
372	nrepeat (napply (less_than_or_equal_monotone ? ?)).
373	napply (less_than_or_equal_zero).
374	nrepeat (napply (less_than_or_equal_monotone ? ?)).
375	napply (less_than_or_equal_zero).
376	nqed.
377
378	ndefinition get_ov_flag ≝
379	λs: Status.
380	let sfr ≝ special_function_registers_8051 s in
381	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
382	get_index Bool eight psw five ?.
383	nnormalize.
384	nrepeat (napply (less_than_or_equal_monotone ? ?)).
385	napply (less_than_or_equal_zero).
386	nrepeat (napply (less_than_or_equal_monotone ? ?)).
387	napply (less_than_or_equal_zero).
388	nqed.
389
390	ndefinition get_ud_flag ≝
391	λs: Status.
392	let sfr ≝ special_function_registers_8051 s in
393	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
394	get_index Bool eight psw six ?.
395	nnormalize.
396	nrepeat (napply (less_than_or_equal_monotone ? ?)).
397	napply (less_than_or_equal_zero).
398	nrepeat (napply (less_than_or_equal_monotone ? ?)).
399	napply (less_than_or_equal_zero).
400	nqed.
401
402	ndefinition get_p_flag ≝
403	λs: Status.
404	let sfr ≝ special_function_registers_8051 s in
405	let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in
406	get_index Bool eight psw seven ?.
407	nnormalize.
408	nrepeat (napply (less_than_or_equal_monotone ? ?)).
409	napply (less_than_or_equal_zero).
410	nrepeat (napply (less_than_or_equal_monotone ? ?)).
411	napply (less_than_or_equal_zero).
412	nqed.
413
414	ndefinition set_flags ≝
415	λs: Status.
416	λcy: Bit.
417	λac: Maybe Bit.
418	λov: Bit.
419	let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in
420	let old_cy ≝ get_index … nu Z ? in
421	let old_ac ≝ get_index … nu one ? in
422	let old_fo ≝ get_index … nu two ? in
423	let old_rs1 ≝ get_index … nu three ? in
424	let old_rs0 ≝ get_index … nl Z ? in
425	let old_ov ≝ get_index … nl one ? in
426	let old_ud ≝ get_index … nl two ? in
427	let old_p ≝ get_index … nl three ? in
428	let new_ac ≝ match ac with [ Nothing ⇒ old_ac \| Just j ⇒ j ] in
429	let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;
430	old_rs0 ; old_ov ; old_ud ; old_p ]] in
431	set_8051_sfr s SFR_PSW new_psw.
432	##[##1,2,3,4,5,6,7,8:
433	nnormalize;
434	nrepeat (napply less_than_or_equal_monotone);
435	napply (less_than_or_equal_zero);
436	##]
437	nqed.
438
439	ndefinition initialise_status ≝
440	let status ≝ mk_Status (Stub Byte sixteen) (* Code mem. *)
441	(Stub Byte seven) (* Low mem. *)
442	(Stub Byte seven) (* High mem. *)
443	(Stub Byte sixteen) (* Ext mem. *)
444	(zero sixteen) (* PC. *)
445	(replicate Byte nineteen (zero eight)) (* 8051 SFR. *)
446	(replicate Byte five (zero eight)) (* 8052 SFR. *)
447	(zero eight) (* P1 latch. *)
448	(zero eight) in (* P3 latch. *)
449	set_program_counter status (bitvector_of_nat sixteen seven).
450
451	naxiom not_implemented: False.
452
453	include "Arithmetic.ma".
454
455	ndefinition get_bit_addressable_sfr ≝
456	λs: Status.
457	λn: Nat.
458	λb: BitVector n.
459	λl: Bool.
460	let address ≝ nat_of_bitvector … b in
461	if (decidable_equality address one_hundred_and_twenty_eight) then
462	?
463	else if (decidable_equality address one_hundred_and_forty_four) then
464	if l then
465	(p1_latch s)
466	else
467	(get_8051_sfr s SFR_P1)
468	else if (decidable_equality address one_hundred_and_sixty) then
469	?
470	else if (decidable_equality address one_hundred_and_seventy_six) then
471	if l then
472	(p3_latch s)
473	else
474	(get_8051_sfr s SFR_P3)
475	else if (decidable_equality address one_hundred_and_fifty_three) then
476	get_8051_sfr s SFR_SBUF
477	else if (decidable_equality address one_hundred_and_thirty_eight) then
478	get_8051_sfr s SFR_TL0
479	else if (decidable_equality address one_hundred_and_thirty_nine) then
480	get_8051_sfr s SFR_TL1
481	else if (decidable_equality address one_hundred_and_forty) then
482	get_8051_sfr s SFR_TH0
483	else if (decidable_equality address one_hundred_and_forty_one) then
484	get_8051_sfr s SFR_TH1
485	else if (decidable_equality address two_hundred) then
486	get_8052_sfr s SFR_T2CON
487	else if (decidable_equality address two_hundred_and_two) then
488	get_8052_sfr s SFR_RCAP2L
489	else if (decidable_equality address two_hundred_and_three) then
490	get_8052_sfr s SFR_RCAP2H
491	else if (decidable_equality address two_hundred_and_four) then
492	get_8052_sfr s SFR_TL2
493	else if (decidable_equality address two_hundred_and_five) then
494	get_8052_sfr s SFR_TH2
495	else if (decidable_equality address one_hundred_and_thirty_five) then
496	get_8051_sfr s SFR_PCON
497	else if (decidable_equality address one_hundred_and_thirty_six) then
498	get_8051_sfr s SFR_TCON
499	else if (decidable_equality address one_hundred_and_thirty_seven) then
500	get_8051_sfr s SFR_TMOD
501	else if (decidable_equality address one_hundred_and_fifty_two) then
502	get_8051_sfr s SFR_SCON
503	else if (decidable_equality address one_hundred_and_sixty_eight) then
504	get_8051_sfr s SFR_IE
505	else if (decidable_equality address one_hundred_and_eighty_four) then
506	get_8051_sfr s SFR_IP
507	else if (decidable_equality address one_hundred_and_twenty_nine) then
508	get_8051_sfr s SFR_SP
509	else if (decidable_equality address one_hundred_and_thirty) then
510	get_8051_sfr s SFR_DPL
511	else if (decidable_equality address one_hundred_and_thirty_one) then
512	get_8051_sfr s SFR_DPH
513	else if (decidable_equality address two_hundred_and_eight) then
514	get_8051_sfr s SFR_PSW
515	else if (decidable_equality address two_hundred_and_twenty_four) then
516	get_8051_sfr s SFR_ACC_A
517	else if (decidable_equality address two_hundred_and_forty) then
518	get_8051_sfr s SFR_ACC_B
519	else
520	?.
521	ncases not_implemented.
522	nqed.
523
524	ndefinition set_bit_addressable_sfr ≝
525	λs: Status.
526	λb: Byte.
527	let address ≝ nat_of_bitvector … b in
528	if (decidable_equality address one_hundred_and_twenty_eight) then
529	?
530	else if (decidable_equality address one_hundred_and_forty_four) then
531	let status_1 ≝ set_8051_sfr s SFR_P1 b in
532	let status_2 ≝ set_p1_latch s b in
533	status_2
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	let status_1 ≝ set_8051_sfr s SFR_P3 b in
538	let status_2 ≝ set_p3_latch s b in
539	status_2
540	else if (decidable_equality address one_hundred_and_fifty_three) then
541	set_8051_sfr s SFR_SBUF b
542	else if (decidable_equality address one_hundred_and_thirty_eight) then
543	set_8051_sfr s SFR_TL0 b
544	else if (decidable_equality address one_hundred_and_thirty_nine) then
545	set_8051_sfr s SFR_TL1 b
546	else if (decidable_equality address one_hundred_and_forty) then
547	set_8051_sfr s SFR_TH0 b
548	else if (decidable_equality address one_hundred_and_forty_one) then
549	set_8051_sfr s SFR_TH1 b
550	else if (decidable_equality address two_hundred) then
551	set_8052_sfr s SFR_T2CON b
552	else if (decidable_equality address two_hundred_and_two) then
553	set_8052_sfr s SFR_RCAP2L b
554	else if (decidable_equality address two_hundred_and_three) then
555	set_8052_sfr s SFR_RCAP2H b
556	else if (decidable_equality address two_hundred_and_four) then
557	set_8052_sfr s SFR_TL2 b
558	else if (decidable_equality address two_hundred_and_five) then
559	set_8052_sfr s SFR_TH2 b
560	else if (decidable_equality address one_hundred_and_thirty_five) then
561	set_8051_sfr s SFR_PCON b
562	else if (decidable_equality address one_hundred_and_thirty_six) then
563	set_8051_sfr s SFR_TCON b
564	else if (decidable_equality address one_hundred_and_thirty_seven) then
565	set_8051_sfr s SFR_TMOD b
566	else if (decidable_equality address one_hundred_and_fifty_two) then
567	set_8051_sfr s SFR_SCON b
568	else if (decidable_equality address one_hundred_and_sixty_eight) then
569	set_8051_sfr s SFR_IE b
570	else if (decidable_equality address one_hundred_and_eighty_four) then
571	set_8051_sfr s SFR_IP b
572	else if (decidable_equality address one_hundred_and_twenty_nine) then
573	set_8051_sfr s SFR_SP b
574	else if (decidable_equality address one_hundred_and_thirty) then
575	set_8051_sfr s SFR_DPL b
576	else if (decidable_equality address one_hundred_and_thirty_one) then
577	set_8051_sfr s SFR_DPH b
578	else if (decidable_equality address two_hundred_and_eight) then
579	set_8051_sfr s SFR_PSW b
580	else if (decidable_equality address two_hundred_and_twenty_four) then
581	set_8051_sfr s SFR_ACC_A b
582	else if (decidable_equality address two_hundred_and_forty) then
583	set_8051_sfr s SFR_ACC_B b
584	else
585	?.
586	ncases not_implemented.
587	nqed.
588
589	ndefinition bit_address_of_register ≝
590	λs: Status.
591	λb, c, d: Bit.
592	let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in
593	let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index four un two ?) (get_index four un three ?) in
594	let offset ≝
595	if conjunction (negation r1) (negation r0) then
596	Z
597	else if conjunction (negation r1) r0 then
598	eight
599	else if conjunction r1 r0 then
600	twenty_four
601	else
602	sixteen
603	in
604	bitvector_of_nat seven (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).
605	nnormalize.
606	nrepeat (napply less_than_or_equal_monotone).
607	napply less_than_or_equal_zero.
608	nrepeat (napply less_than_or_equal_monotone).
609	napply less_than_or_equal_zero.
610	nqed.
611
612	ndefinition get_register ≝
613	λs: Status.
614	λb, c, d: Bit.
615	let address ≝ bit_address_of_register s b c d in
616	lookup … address (low_internal_ram s) (zero eight).
617
618	ndefinition set_register ≝
619	λs: Status.
620	λb, c, d: Bit.
621	λv: Byte.
622	let address ≝ bit_address_of_register s b c d in
623	let old_low_internal_ram ≝ low_internal_ram s in
624	let new_low_internal_ram ≝ insert … address v old_low_internal_ram in
625	set_low_internal_ram s new_low_internal_ram.
626
627	ndefinition read_at_stack_pointer ≝
628	λs: Status.
629	let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
630	let m ≝ get_index … nu Z ? in
631	let r1 ≝ get_index … nu one ? in
632	let r2 ≝ get_index … nu two ? in
633	let r3 ≝ get_index … nu three ? in
634	let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in
635	let memory ≝
636	if m then
637	(low_internal_ram s)
638	else
639	(high_internal_ram s)
640	in
641	lookup … address memory (zero eight).
642	##[##1,2,3,4:
643	nnormalize;
644	nrepeat (napply less_than_or_equal_monotone);
645	napply less_than_or_equal_zero;
646	##]
647	nqed.
648
649	ndefinition write_at_stack_pointer ≝
650	λs: Status.
651	λv: Byte.
652	let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in
653	let bit_zero ≝ get_index … nu Z ? in
654	let bit_one ≝ get_index … nu one ? in
655	let bit_two ≝ get_index … nu two ? in
656	let bit_three ≝ get_index … nu three ? in
657	if bit_zero then
658	let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
659	v (low_internal_ram s) in
660	set_low_internal_ram s memory
661	else
662	let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl)
663	v (high_internal_ram s) in
664	set_high_internal_ram s memory.
665	##[##1,2,3,4:
666	nnormalize;
667	nrepeat (napply less_than_or_equal_monotone);
668	napply less_than_or_equal_zero;
669	##]
670	nqed.
671
672	include "ASM.ma".
673
674	ndefinition set_arg_16: Status → Word → [[ dptr ]] → Status ≝
675	λs,v,a.
676	match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with
677	[ DPTR ⇒ λ_:True.
678	let 〈 bu, bl 〉 ≝ split … eight eight v in
679	let status ≝ set_8051_sfr s SFR_DPH bu in
680	let status ≝ set_8051_sfr status SFR_DPL bl in
681	status
682	\| _ ⇒ λK.
683	match K in False with
684	[
685	]
686	] (subaddressing_modein … a).
687
688	ndefinition get_arg_16: Status → [[ data16 ]] → Word ≝
689	λs, a.
690	match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with
691	[ DATA16 d ⇒ λ_:True. d
692	\| _ ⇒ λK.
693	match K in False with
694	[
695	]
696	] (subaddressing_modein … a).

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

Download in other formats:

Original Format