@@ -58,6 +58,10 @@ val plat_rom_size = {ocaml: "Platform.rom_size", interpreter: "Platform.rom_si
5858val plat_clint_base = {ocaml : "Platform.clint_base" , interpreter : "Platform.clint_base" , c : "plat_clint_base" , lem : "plat_clint_base" } : unit -> xlenbits
5959val plat_clint_size = {ocaml : "Platform.clint_size" , interpreter : "Platform.clint_size" , c : "plat_clint_size" , lem : "plat_clint_size" } : unit -> xlenbits
6060
61+ /* Location of UART, which should match with the spec in the DTB */
62+ val plat_uart_base = {ocaml : "Platform.uart_base" , interpreter : "Platform.uart_base" , c : "plat_uart_base" , lem : "plat_uart_base" } : unit -> xlenbits
63+ val plat_uart_size = {ocaml : "Platform.uart_size" , interpreter : "Platform.uart_size" , c : "plat_uart_size" , lem : "plat_uart_size" } : unit -> xlenbits
64+
6165/* Location of HTIF ports */
6266val plat_htif_tohost = {ocaml : "Platform.htif_tohost" , c : "plat_htif_tohost" , lem : "plat_htif_tohost" } : unit -> xlenbits
6367function plat_htif_tohost () = to_bits (sizeof (xlen ), elf_tohost ())
@@ -117,6 +121,18 @@ function within_htif_writable forall 'n, 0 < 'n <= max_mem_access . (addr : xlen
117121function within_htif_readable forall 'n , 0 < 'n <= max_mem_access . (addr : xlenbits , width : atom ('n )) -> bool =
118122 plat_htif_tohost () == addr | (plat_htif_tohost () + 4 == addr & width == 4 )
119123
124+ function within_uart forall 'n , 0 < 'n <= max_mem_access . (addr : xlenbits , width : atom ('n )) -> bool = {
125+ /* To avoid overflow issues when physical memory extends to the end
126+ * of the addressable range, we need to perform address bound checks
127+ * on unsigned unbounded integers.
128+ */
129+ let addr_int = unsigned (addr );
130+ let uart_base_int = unsigned (plat_uart_base ());
131+ let uart_size_int = unsigned (plat_uart_size ());
132+ uart_base_int <= addr_int
133+ & (addr_int + sizeof ('n )) <= (uart_base_int + uart_size_int )
134+ }
135+
120136/* CLINT (Core Local Interruptor), based on Spike. */
121137
122138val plat_insns_per_tick = {ocaml : "Platform.insns_per_tick" , interpreter : "Platform.insns_per_tick" , c : "plat_insns_per_tick" , lem : "plat_insns_per_tick" } : unit -> int
@@ -386,20 +402,77 @@ function htif_tick() = {
386402/* Top-level MMIO dispatch */
387403$ifndef RVFI_DII
388404function within_mmio_readable forall 'n , 0 < 'n <= max_mem_access . (addr : xlenbits , width : atom ('n )) -> bool =
389- within_clint (addr , width ) | (within_htif_readable (addr , width ) & 1 <= 'n )
405+ within_uart ( addr , width ) | within_clint (addr , width ) | (within_htif_readable (addr , width ) & 1 <= 'n )
390406$else
391407function within_mmio_readable forall 'n , 0 < 'n <= max_mem_access . (addr : xlenbits , width : atom ('n )) -> bool = false
392408$endif
393409
394410$ifndef RVFI_DII
395411function within_mmio_writable forall 'n , 0 < 'n <= max_mem_access . (addr : xlenbits , width : atom ('n )) -> bool =
396- within_clint (addr , width ) | (within_htif_writable (addr , width ) & 'n <= 8 )
412+ within_uart ( addr , width ) | within_clint (addr , width ) | (within_htif_writable (addr , width ) & 'n <= 8 )
397413$else
398414function within_mmio_writable forall 'n , 0 < 'n <= max_mem_access . (addr : xlenbits , width : atom ('n )) -> bool = false
399415$endif
400416
417+ /* This is a very minimal UART implementation: just enough to allow a basic
418+ driver to output to the console. It ignores the configuration registers and
419+ does not supporting reading except from the line status register which indictes
420+ it is always ready to transmit. Does not support interrupts. */
421+
422+ let UART_OFFSET_DATA = 0x00000000
423+ let UART_OFFSET_LINE_CTL = 0x0000000c
424+ let UART_OFFSET_LINE_STATUS = 0x00000014
425+ /* Divisor latch access bit. We need this so that we can ignore writes to data
426+ register while the driver programs the baud rate (otherwise we might print
427+ garbage on console). */
428+ register UART_DLAB : bit = bitzero
429+
430+ val uart_load : forall 'n , 'n > 0 . (AccessType (ext_access_type ), xlenbits , int ('n )) -> MemoryOpResult (bits (8 * 'n ))
431+ function uart_load (t , addr , width ) = {
432+ let offset = addr - plat_uart_base ();
433+ /* We only support reading the status register, which always indicates ready to write output */
434+ if offset == zero_extend (UART_OFFSET_LINE_STATUS ) & ('n == 4 )
435+ then {
436+ let result = 0b100000 ; /* TXBufEmpty always */
437+ if get_config_print_platform ()
438+ then print_platform ("uart[" ^ BitStr (offset ) ^ "] -> " ^ BitStr (result ));
439+ MemValue (sail_zero_extend (result , sizeof (8 * 'n )))
440+ } else {
441+ if get_config_print_platform ()
442+ then print_platform ("uart[" ^ BitStr (offset ) ^ "] -> <not-mapped>" );
443+ match t {
444+ Execute () => MemException (E_Fetch_Access_Fault ()),
445+ Read (Data ) => MemException (E_Load_Access_Fault ()),
446+ _ => MemException (E_SAMO_Access_Fault ())
447+ }
448+ }
449+ }
450+
451+ val uart_store : forall 'n , 'n > 0 . (xlenbits , int ('n ), bits (8 * 'n )) -> MemoryOpResult (bool )
452+ function uart_store (addr , width , data ) = {
453+ let offset = addr - plat_uart_base ();
454+ /* only support writing to the data register for output, ignore other writes */
455+ if offset == zero_extend (UART_OFFSET_DATA ) & ('n == 8 | 'n == 4 ) then {
456+ if get_config_print_platform ()
457+ then print_platform ("uart[" ^ BitStr (offset ) ^ "] <- " ^ BitStr (data ));
458+ if UART_DLAB == bitzero then plat_term_write (data [7 .. 0 ]);
459+ MemValue (true )
460+ } else if offset == zero_extend (UART_OFFSET_LINE_CTL ) & ('n == 8 | 'n == 4 ) then {
461+ if get_config_print_platform ()
462+ then print_platform ("uart[" ^ BitStr (offset ) ^ "] <- " ^ BitStr (data ));
463+ UART_DLAB = data [7 ];
464+ MemValue (true )
465+ } else {
466+ if get_config_print_platform ()
467+ then print_platform ("uart[" ^ BitStr (offset ) ^ "] <- " ^ BitStr (data ) ^ " (<ignored>)" );
468+ MemValue (true )
469+ }
470+ }
471+
401472function mmio_read forall 'n , 0 < 'n <= max_mem_access . (t : AccessType (ext_access_type ), paddr : xlenbits , width : atom ('n )) -> MemoryOpResult (bits (8 * 'n )) =
402- if within_clint (paddr , width )
473+ if within_uart (paddr , width )
474+ then uart_load (t , paddr , width )
475+ else if within_clint (paddr , width )
403476 then clint_load (t , paddr , width )
404477 else if within_htif_readable (paddr , width ) & (1 <= 'n )
405478 then htif_load (t , paddr , width )
@@ -410,7 +483,9 @@ function mmio_read forall 'n, 0 < 'n <= max_mem_access . (t : AccessType(ext_acc
410483 }
411484
412485function mmio_write forall 'n , 0 <'n <= max_mem_access . (paddr : xlenbits , width : atom ('n ), data : bits (8 * 'n )) -> MemoryOpResult (bool ) =
413- if within_clint (paddr , width )
486+ if within_uart (paddr , width )
487+ then uart_store (paddr , width , data )
488+ else if within_clint (paddr , width )
414489 then clint_store (paddr , width , data )
415490 else if within_htif_writable (paddr , width ) & 'n <= 8
416491 then htif_store (paddr , width , data )
0 commit comments