impl/experimental/serial/serial.cogent

--
-- Copyright 2019, Data61
-- Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-- ABN 41 687 119 230.
--
-- This software may be distributed and modified according to the terms of
-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
-- See "LICENSE_GPLv2.txt" for details.
--
-- @TAG(DATA61_GPL)
--
include <gum/common/common.cogent>

const_UART_REF_CLK : U32
const_UART_REF_CLK = 50000000


-- UART flags
flag_UART_SR1_RRDY : U32
flag_UART_SR1_RRDY = 1 << 9

flag_UART_SR1_TRDY : U32
flag_UART_SR1_TRDY = 1 << 13

-- CR1
flag_UART_CR1_UARTEN : U32
flag_UART_CR1_UARTEN = 1 << 0

flag_UART_CR1_RRDYEN : U32
flag_UART_CR1_RRDYEN = 1 << 9

-- CR2
flag_UART_CR2_SRST : U32
flag_UART_CR2_SRST = 1 << 0

flag_UART_CR2_RXEN : U32
flag_UART_CR2_RXEN = 1 << 1

flag_UART_CR2_TXEN : U32
flag_UART_CR2_TXEN = 1 << 2

flag_UART_CR2_ATEN : U32
flag_UART_CR2_ATEN = 1 << 3

flag_UART_CR2_RTSEN : U32
flag_UART_CR2_RTSEN = 1 << 4

flag_UART_CR2_WS : U32
flag_UART_CR2_WS = 1 << 5

flag_UART_CR2_STPB : U32
flag_UART_CR2_STPB = 1 << 6

flag_UART_CR2_PROE : U32
flag_UART_CR2_PROE = 1 << 7

flag_UART_CR2_PREN : U32
flag_UART_CR2_PREN = 1 << 8

flag_UART_CR2_RTEC : U32
flag_UART_CR2_RTEC = 1 << 9

flag_UART_CR2_ESCEN : U32
flag_UART_CR2_ESCEN = 1 << 11

flag_UART_CR2_CTS : U32
flag_UART_CR2_CTS = 1 << 12

flag_UART_CR2_CTSC : U32
flag_UART_CR2_CTSC = 1 << 13

flag_UART_CR2_IRTS : U32
flag_UART_CR2_IRTS = 1 << 14

flag_UART_CR2_ESCI : U32
flag_UART_CR2_ESCI = 1 << 15

-- CR3
flag_UART_CR3_RXDMUXDEL : U32
flag_UART_CR3_RXDMUXDEL = 1 << 2

-- FCR
uart_FCR_RFDIV : U32 -> U32
uart_FCR_RFDIV x = x * (1 << 7)

uart_FCR_RFDIV_MASK : () -> U32
uart_FCR_RFDIV_MASK () = uart_FCR_RFDIV 0x7

uart_FCR_RXTL : U32 -> U32
uart_FCR_RXTL x = x * (1 << 0)

uart_FCR_RXTL_MASK : () -> U32
uart_FCR_RXTL_MASK () = uart_FCR_RXTL 0x1F

-- SR2
flag_UART_SR2_RXFIFO_RDR : U32
flag_UART_SR2_RXFIFO_RDR = 1 << 0

flag_UART_SR2_TXFIFO_EMPTY : U32
flag_UART_SR2_TXFIFO_EMPTY = 1 << 14

-- RXD
flag_UART_URXD_READY_MASK : U32
flag_UART_URXD_READY_MASK = 1 << 15

flag_UART_BYTE_MASK : U32
flag_UART_BYTE_MASK = 0xFF

-- External function - implemented in antiquoted C
uart_setup_phase1_ac : SysState -> SysState

-- Register readers
imx_uart_regs_read_rxd   : SysState -> (U32, SysState)
imx_uart_regs_read_txd   : SysState -> (U32, SysState)
imx_uart_regs_read_cr1   : SysState -> (U32, SysState)
imx_uart_regs_read_cr2   : SysState -> (U32, SysState)
imx_uart_regs_read_cr3   : SysState -> (U32, SysState)
imx_uart_regs_read_cr4   : SysState -> (U32, SysState)
imx_uart_regs_read_fcr   : SysState -> (U32, SysState)
imx_uart_regs_read_sr1   : SysState -> (U32, SysState)
imx_uart_regs_read_sr2   : SysState -> (U32, SysState)
imx_uart_regs_read_esc   : SysState -> (U32, SysState)
imx_uart_regs_read_tim   : SysState -> (U32, SysState)
imx_uart_regs_read_bir   : SysState -> (U32, SysState)
imx_uart_regs_read_bmr   : SysState -> (U32, SysState)
imx_uart_regs_read_brc   : SysState -> (U32, SysState)
imx_uart_regs_read_onems : SysState -> (U32, SysState)
imx_uart_regs_read_ts    : SysState -> (U32, SysState)

-- Register writers
imx_uart_regs_write_rxd   : (U32, SysState) -> SysState
imx_uart_regs_write_txd   : (U32, SysState) -> SysState
imx_uart_regs_write_cr1   : (U32, SysState) -> SysState
imx_uart_regs_write_cr2   : (U32, SysState) -> SysState
imx_uart_regs_write_cr3   : (U32, SysState) -> SysState
imx_uart_regs_write_cr4   : (U32, SysState) -> SysState
imx_uart_regs_write_fcr   : (U32, SysState) -> SysState
imx_uart_regs_write_sr1   : (U32, SysState) -> SysState
imx_uart_regs_write_sr2   : (U32, SysState) -> SysState
imx_uart_regs_write_esc   : (U32, SysState) -> SysState
imx_uart_regs_write_tim   : (U32, SysState) -> SysState
imx_uart_regs_write_bir   : (U32, SysState) -> SysState
imx_uart_regs_write_bmr   : (U32, SysState) -> SysState
imx_uart_regs_write_brc   : (U32, SysState) -> SysState
imx_uart_regs_write_onems : (U32, SysState) -> SysState
imx_uart_regs_write_ts    : (U32, SysState) -> SysState


uart_getchar_cg : SysState -> (SysState, U32)
uart_getchar_cg world =
   let (rxd, world) = imx_uart_regs_read_rxd world
   and (sr2, world) = imx_uart_regs_read_sr2 world
   and c = if ( sr2 .&. flag_UART_SR2_RXFIFO_RDR ) /= 0 then rxd else 0
   and c = if ( c .&. flag_UART_URXD_READY_MASK ) /= 0 then c else 0
   and c = c .&. flag_UART_BYTE_MASK
   in (world, c)

imx_uart_set_baud_cg : (U64, SysState) -> SysState
imx_uart_set_baud_cg (bps, world) =
   let (fcr, world) = imx_uart_regs_read_fcr world
   and fcr = fcr .&. complement (uart_FCR_RFDIV_MASK ())
   and fcr = fcr .|. uart_FCR_RFDIV 4
   and bir = 0xF
   and bmr = const_UART_REF_CLK / (u64_to_u32 bps - 1)
   and world = imx_uart_regs_write_fcr (fcr, world)
   and world = imx_uart_regs_write_bir (bir, world)
   and world = imx_uart_regs_write_bmr (bmr, world)
   in world

type Parity = < PARITY_NONE | PARITY_EVEN  | PARITY_ODD >

compute_cr2_by_parity : (Parity, U32) -> U32
compute_cr2_by_parity (p, cr2) = p
   | PARITY_NONE  -> let cr2 = cr2 .&. complement flag_UART_CR2_PREN
                     in cr2
   | PARITY_ODD   -> let cr2 = cr2 .|. flag_UART_CR2_PREN
                     and cr2 = cr2 .|. flag_UART_CR2_PROE
                     in cr2
   | PARITY_EVEN  -> let cr2 = cr2 .|. flag_UART_CR2_PREN
                     and cr2 = cr2 .&. complement flag_UART_CR2_PROE
                     in cr2

serial_configure_cg : (U64, U32, Parity, U32, SysState) -> SysState
serial_configure_cg (bps, char_size, parity, stop_bits, world) =
   let (cr2, world) = imx_uart_regs_read_cr2 world
   and cr2 =
     -- character size
     if | char_size == 8 -> cr2 .|. flag_UART_CR2_WS
        | char_size == 7 -> cr2 .&. complement flag_UART_CR2_WS
        | else           -> 0 -- Need to fail here
   and cr2 =
     -- stop bits
     if | stop_bits == 2 -> cr2 .|. flag_UART_CR2_STPB
        | stop_bits == 1 -> cr2 .&. complement flag_UART_CR2_STPB
        | else           -> 0 -- Need to fail here
   and cr2 = compute_cr2_by_parity (parity, cr2)
   and world = imx_uart_regs_write_cr2 (cr2, world)
   and world = imx_uart_set_baud_cg (bps, world)
   in world

uart_sw_reset_cg : SysState -> SysState
uart_sw_reset_cg world =
   let (cr2, world) = imx_uart_regs_read_cr2 world
   and cr2 = cr2 .&. complement flag_UART_CR2_SRST
   and world = imx_uart_regs_write_cr2 (cr2, world)
   in world

uart_setup : SysState -> SysState
uart_setup world =
   -- Perform a software reset
   let world = uart_sw_reset_cg world
   and world = uart_setup_phase1_ac world
   -- Serial line configuration
   and world = serial_configure_cg (11520, 8, PARITY_NONE, 1, world)
   -- Enable the UART
   and (cr1, world) = imx_uart_regs_read_cr1 world
   and cr1 = cr1 .|. flag_UART_CR1_UARTEN
   and world = imx_uart_regs_write_cr1 (cr1, world)
   -- RX/TX Enable
   and (cr2, world) = imx_uart_regs_read_cr2 world
   and cr2 = cr2 .|. flag_UART_CR2_RXEN .|. flag_UART_CR2_TXEN
   and world = imx_uart_regs_write_cr2 (cr2, world)
   -- Ignore RTS
   and (cr2, world) = imx_uart_regs_read_cr2 world
   and cr2 = cr2 .|. flag_UART_CR2_IRTS
   and world = imx_uart_regs_write_cr2 (cr2, world)
   -- Configure the RX MUX
   and (cr3, world) = imx_uart_regs_read_cr3 world
   and cr3 = cr3 .|. flag_UART_CR3_RXDMUXDEL
   and world = imx_uart_regs_write_cr3 (cr3, world)
   -- Initialise the receiver interrupt
   -- Disable recv interrupt
   and (cr1, world) = imx_uart_regs_read_cr1 world
   and (fcr, world) = imx_uart_regs_read_fcr world
   and cr1 = cr1 .&. complement flag_UART_CR1_RRDYEN
   and world = imx_uart_regs_write_cr1 (cr1, world)
   -- Clear the trigger value
   and fcr = fcr .&. complement (uart_FCR_RXTL_MASK ())
   and world = imx_uart_regs_write_fcr (fcr, world)
   and (cr1, world) = imx_uart_regs_read_cr1 world
   and (fcr, world) = imx_uart_regs_read_fcr world
   -- Set the rx tigger level to 1
   and fcr = fcr .|. uart_FCR_RXTL 1
   and world = imx_uart_regs_write_fcr (fcr, world)
   -- Enable recv interrupt
   and cr1 = cr1 .|. flag_UART_CR1_RRDYEN
   and world = imx_uart_regs_write_cr1 (cr1, world)
   in world