source: Deliverables/D4.1/Matita/ASM.ma @ 248

Last change on this file since 248 was 248, checked in by mulligan, 10 years ago

More changes. Added datatype for addressing modes.

File size: 790 bytes
Line 
1include "Universes.ma".
2include "Equality.ma".
3include "BitVector.ma".
4
5ninductive AddressingMode: Type[0] ≝
6  Direct: Byte → AddressingMode
7| Indirect: Bit → AddressingMode
8| ExtIndirect: Bit → AddressingMode
9| Register: Bit → Bit → Bit → AddressingMode
10| AccumulatorA: AddressingMode
11| AccumulatorB: AddressingMode
12| DPointer: AddressingMode
13| Data: Byte → AddressingMode
14| Data16: Word → AddressingMode
15| AccumulatorDPointer: AddressingMode
16| AccumulatorProgramCounter: AddressingMode
17| ExternalIndirectDPointer: AddressingMode
18| IndirectDPointer: AddressingMode
19| Carry: AddressingMode
20| Bit: Bit → AddressingMode
21| ComplementBit: Bit → AddressingMode
22| Relative: Byte → AddressingMode
23| Address11: Word11 → AddressingMode
24| Address16: Word → AddressingMode.
Note: See TracBrowser for help on using the repository browser.