Currently, I'm struggling to read a block of data from micro-sd in seL4.

I use the following code (assertions are omitted here for readability) to instantiate the driver :

ps_io_mapper_t io_mapper = {0};

error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper);

ps_dma_man_t dma_man = {0};

error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man);

ps_io_ops_t io_ops = {

.io_mapper = io_mapper,

.dma_manager = dma_man

};

sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev));

assert(dev != NULL);

memset(dev,0, sizeof(*dev));

enum sdio_id id = sdio_default_id();

error = sdio_init(id, &io_ops, dev);

mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card));

error = mmc_init(dev, &io_ops, mmc_card);

void* vaddr = (void*) 0x1980000;

uintptr_t paddr = (uintptr_t) 0x119a7000;

long read_len = mmc_block_read(*mmc_card, 0, 5, vaddr, paddr, NULL, NULL);

And the code's stuck in mmc_block_read function where interrupt status (BRR and BWR) are never on.

Thanks in advance,

Oak

Norrathep (Oak) Rattanavipanon

M.S. in Computer Science

University of California - Irvine