device serial {
    register_map serial_reg_map
    {
        .=default {
           stride = 4;
           size = 4;
           access = RW;
           read_value = static;
           write_value = dont_change;
           [31:8]: reserved; write_value=fixed(0b0); read_value=dont_matter; 
        }

        .=0x00 { 
            RX;
            access = RO;
            read_value = volatile;
            [7:0]: RX;
        }

        .=0x00 { 
            TX;
            access = WO;
            write_value = no_default;
            [7:0]: TX;
        }

        .=0x00 {
            DLL;
            [7:0]: DLL; 
        }

        .=0x04 {
            DLM; 
            [7:0]: DLM;
        }

        .=0x04 { 
            IER;
            [7]: DMAE; 
            [6]: UUE;
            [5]: NRZE; 
            [4]: RTOIE;
            [3]: MSI; 
            [2]: RLSI;
            [1]: THRI; 
            [0]: RDI;
        }

        .=0x08 { 
            IIR;
            access = RO;
            read_value = volatile;
            [7:6]: FIFOES; enum = {NON_FIFIO=0b00, FIFO=0b11}; 
            [5]: EOC;
            [4]: ABL;
            [3]: TOD; 
            [2:1]: ID; enum = {MSI=0b0, THRI=0b01, RDI=0b10, RLSI=0b11};
            [0]: NO_INT;
            /* other bits meaningful only when nIP=0 */
            /* FIFOES = 0b11 => TRFIFOE=1 */
            /* FIFOES = 0b00 => TRFIFOE=0 */
        }

        .=0x08 { 
            FCR;
            access = WO;
            [7:6]: TRIGGER_MASK; write_value = no_default; enum = {TRIGGER_1=0b00, TRIGGER_8=0b01, TRIGGER_16=0b10, TRIGGER_14=0b11};
            [5]: BUS; write_value = no_default;
            [4]: TRAIL; write_value = no_default;
            [3]: DMA_SELECT;  write_value = no_default;
            [2]: CLEAR_XMIT; write_value = no_default;
            [1]: CLEAR_RCVR; write_value = no_default;
            [0]: ENABLE_FIFO; write_value = no_default;
            /* TRFIFOE=1 when other bits are written */
        }
        .=0x0C { 
            LCR;
            [7]: DLAB;
            [6]: SBC;
            [5]: SPAR;
            [4]: EPAR; enum = {ODD_PARITY= 0, EVEN_PARITY=1};
            [3]: PARITY; enum = {PARITY=0, NO_PARITY=1};
            [2]: STOP; enum = {STOP_BIT_1=0, STOP_BIT_2=1};
            [1:0]: WLS; enum = {WLEN5 = 0b00, WLEN6=0b01, WLEN7=0b10, WLEN8 =0b11};
        }

        .=0x14 { 
            LSR;
            access = RO;
            read_value = volatile;
            [7]: FIFOE;
            [6]: TEMT;
            [5]: THRE;
            [4]: BI;
            [3]: FE;
            [2]: PE;
            [1]: OE;
            [0]: DR;
            /* LSR must be read before IIR is read */
            /* TX=0 && TSR=0 => TEMT=1 */
            /* FIFOE is reset when all error data is read from FIFO, then
               enable DMA */
            /* R(LSR) =i> BI=0 && FE=0 && PE=0 */
        }

        .=0x10 { 
            MCR;
            [31:6]: reserved; write_value=fixed(0b0); read_value = dont_matter; 
            [5]: AFE;
            [4]: LOOP;
            [3]: OUT2;
            [2]: OUT1;
            [1]: RTS;
            [0]: DTR;
        }

        .=0x10 { 
            MSR;
            access = RO;
            read_value = volatile;
            [7]: DCD;
            [6]: RI;
            [5]: DSR;
            [4]: CTS;
            [3]: DDCD;
            [2]: TERI;
            [1]: DDSR;
            [0]: DCTS;
            /* 3:0 is set && IER[MIE]=1 => interrupt */
        }

        .=0x1C { 
            SCR;
            [7:0]: Scratchpad;
        }
        

/* ZOAR specific
        .=0x20 { 
            ISR;
            [31:5]: reserved; write_value=fixed(0b0); read_value = dont_matter; 
            [4]: RXPL;
            [3]: TXPL;
            [2]: XMODE;
            [1]: RCVEIR;
            [0]: XMITIR;
        }

        .=0x24 { 
            FOR;
            [31:6]: reserved; write_value=fixed(0b0); read_value = dont_matter; 
            [5:0]: ByteCount;
        }

        .=0x28 { 
            ABR;
            [31:4]: reserved; write_value=fixed(0b0); read_value = dont_matter; 
            [3]: ABT;
            [2]: ABUP;
            [1]: ABLIE;
            [0]: ABE;
             ACR => interrupt if ABLIE=1 && program DLL and DLM if ABUP=1 
        }

        .=0x2C { 
            ACR;
            access = RO;
            [31:16]: reserved; read_value = dont_matter; 
            [15:0]: CountValue;
        }
*/
    }
}

instantiate my_serial as serial {
	multi_instance = no;
	serial_reg_map => cpu_virtual {
		base_address = static(0xF8100000);
	};	
}

/*
gated_spec i2c {
	data_width = {1, 2};
	access_function = arcom_i2c;
};

instantiate my_serial as serial {
	multi_instance = no;
	i2c {
		base_address = static(0xF8100000);
	};	
}
  arcom_i2c_get_2(base+ offset);
  arcom_i2c_set_2(base+ offset, val);
*/



invariant {
/* 
 * To ensure the at the DMA controller and programmed IO do not access the same
 * FIFO, software must not set DMAE while the TIE or RAVIE bits are set
 */
 
((r(IER_THRI) == 0 && r(IER_RDI) == 0) || w(IER_DMAE) == 0)  {w(IER_DMAE)} ;

/*
 * What DIAB bit is set, we can access DLL & DLM;
 * Otherwise we get to access RX, TX, IER
 */
 
(r(LCR_DLAB) == 1) {rw(DLL), rw(DLM)};
(r(LCR_DLAB) == 0) {r(RX), w(TX), rw(IER)};

/*
 * in FIFO mode, wait until the transmitter is idle to set and clear SB.
 */
 
((r(IIR_FIFOES) == FIFO && r(LSR_TEMT) == 1) || w(LCR_SB) == 0) {w(LCR_SB)};
}