Hi Oak, That's interesting. i.MX6 has 4 host controllers(SDHC). The first and the second one are not connected on SabreLite. SDHC3 is connected to the SD card slot, and SDHC4 is connected to the micro-SD card slot. If you take a closer look at the board, on the left side of the micro-SD card slot, there's a label says "SD4" and "SD3" right above the SD card slot. When calling "sdio_default_id()", the function would return "SDHC4"(defined in libsdhcdrivers/plat_include/imx6/sdhc/plat/sdio.h) which should be the micro-SD card slot. I double-checked with the reference manual, the device memory address in the source code is correct. Maybe your SabreLite is a different revision. You could try passing SDHC1/2/3 to function "sdio_init()" as sdio_id, to find out which one is connected to the micro-SD card slot. But this doesn't explain why you've got the correct card capacity out of a different slot. I'm totally confused. Anyway, good to know the code works finally, although in an unexpected way. - Siwei On Fri, Feb 10, 2017 at 08:20:09PM -0800, Norrathep Rattanavipanon wrote: #Hi Siwei, # #So, I tried the code using Kingston microSDHC but it still couldnt read the #card. # #However, the code works perfectly when loaded from the SD slot (with microSD to #SD adapter), instead of the microSD slot. I also found that for some reasons, #if mmc dev 1 is used in u-boot, the program wouldnt be able to read/write the #micro-sd card. # #I'm kind of good for now but still curious about that. Do you have any idea #what might have caused this? # #Best, #Oak # #On Mon, Jan 23, 2017 at 11:07 AM, Norrathep Rattanavipanon <nrattana@uci.edu> #wrote: # # Thanks Siwei. I really appreciate your help. # Yeah so I tried your image with three different micro-sd cards and none of # them works (still stuck after printing the card's capacity). # I'll buy Kingston microsdhc class 4 and try on that, will let you know if # it works or not. # # Best, # Oak # # On Mon, Jan 23, 2017 at 12:03 AM, <Siwei.Zhuang@data61.csiro.au> wrote: # # # Hi Oak, # # # Here is what exactly I did, # # # $ mkdir sel4-sdcard # # $ cd sel4-sdcard # # $ repo init -u https://github.com/SEL4PROJ/ # sel4-tutorials-manifest.git -m sel4-tutorials-master.xml # # $ repo sync # # $ cd projects # # $ git clone https://github.com/SEL4PROJ/projects_libs.git # # $ cd ../libs # # $ ln -sf ../projects/projects_libs/libsdhcdrivers libsdhcdrivers # # $ ln -sf ../projects/seL4_libs/libsel4sync libsel4sync # # # Then, I copied my sdcard app into sel4-sdcard/apps. # # The sdcard app directory has Kconfig, Kbuild, Makefile and src/main.c # # # ------------ Kconfig ---------------- # # menuconfig APP_SDCARD # bool "SD card" # default y # depends on HAVE_LIBC # depends on LIB_SEL4_PLAT_SUPPORT # depends on LIB_SEL4_VKA # depends on LIB_SEL4_UTILS # depends on LIB_UTILS # depends on LIB_CPIO # depends on LIB_SEL4 # depends on LIB_ELF # help # SD card app. # # # # ------------ Kbuild ----------------- # # apps-$(CONFIG_APP_SDCARD) += sdcard # # sdcard: common libsel4utils libutils libsel4 libmuslc libsel4muslcsys # \ # libsel4vka libsel4allocman libsel4vspace libsel4simple # libsel4simple-default \ # libsel4platsupport libsel4platsupport libcpio libelf \ # libsel4sync libsdhcdrivers libsel4debug # # # ------------ Makefile --------------- # # # Targets # TARGETS := sdcard.bin # # ENTRY_POINT := _sel4_start # # # Source files required to build the target # CFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/ # src/*.c)) # ASMFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/ # src/*.S)) # OFILES := archive.o # # # Libraries required to build the target # LIBS = c sel4 sel4muslcsys sel4vka sel4allocman \ # platsupport sel4platsupport sel4vspace elf \ # sel4utils sel4simple utils sel4simple-default cpio \ # sel4sync sdhcdrivers sel4debug # #CFLAGS += -Werror # # include $(SEL4_COMMON)/common.mk # # archive.o: ${COMPONENTS} # $(Q)mkdir -p $(dir $@) # ${COMMON_PATH}/files_to_obj.sh $@ _cpio_archive $^ # # # # I also edited sel4-sdcard/Kconfig, added the following to the related # menus, # # source "apps/sdcard/Kconfig" # # source "libs/libsdhcdrivers/Kconfig" # # source "libs/libsel4sync/Kconfig" # # # I've attached the config file, copy it to configs directory, then do # "make sdcard_defconfig". # # I've also attached the binary image that I compiled. # # # Since the u-boot command works, it doesn't seem that the controller is # disabled. Also try another card if possible, my card is Kingston micro # SDHC class 4. The driver only implements very basic single block read/ # write. I'm not surprised that it doesn't work for some cards. # # # - Siwei # # # ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ # From: Norrathep Rattanavipanon <nrattana@uci.edu> # Sent: Monday, 23 January 2017 4:59 PM # To: Zhuang, Siwei (Data61, Kensington NSW) # # Subject: Re: [seL4] SDHC drivers (cont.) # # Hi Siwei, # # Thank you for helping me out. I am still unable to get it to work even # if using your code with the latest kernel (4.0) and latest libraries # (downloaded from https://github.com/SEL4PROJ/sel4-tutorials-manifest # master branch) # # I also tried calling mmc read command in u-boot and it was able to read # data from the card just fine. # I'm not really sure how I can check if the host controller works # properly. Do you mean I can do it in seL4? # # Also, is it possible if you can upload the binary image file (and the # build config) so that I can test on my board really quick? I suspect # that either I miss something for the build or my micro-sd is not # working. # # Thank you again for your help, # Oak # # On Thu, Jan 19, 2017 at 11:12 AM, Norrathep Rattanavipanon < # nrattana@uci.edu> wrote: # # Hi Siwei, # # Yes, I believe mmc_card_capacity returns the correct value # (4026531840 - my microsd is 4GB). # # And my code does not do any interrupt handling. In fact, that's all # the code in the root userspace process (besides initializing vka, # vspace and simple objects) and there is no other process. # # I also tried using a callback as mmc_block_read's argument, instead # of using NULL, but it also does not work. # # On Wed, Jan 18, 2017 at 8:41 PM, <Siwei.Zhuang@data61.csiro.au> # wrote: # # # Hi Oak, # # # Do you get the correct card capacity by calling # mmc_card_capacity? If you don't, you'd need to check if the # hardware is enabled in your bootloader. # # # Are you doing any interrupt handling? As you don't supply a # callback function to mmc_block_read, the read function would # block until the hardware responses. In this case, # mmc_block_read handles the interrupt itself. It would trigger a # dead lock if you also handles the interrupt. # # # - Siwei # # # # ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ # From: Devel <devel-bounces@sel4.systems> on behalf of Norrathep # Rattanavipanon <nrattana@uci.edu> # Sent: Thursday, 19 January 2017 9:54 AM # To: Danis, Adrian (Data61, Kensington NSW) # Cc: devel@sel4.systems; GTS # Subject: Re: [seL4] SDHC drivers (cont.) # # Hi Adrian, # # Thank you for the reply. I fix it according to what you suggest # but it still does not solve the problem (still hang at the same # place. Do you have any other suggestions on what I should fix # or how I should look into debugging it? # # Best, # Oak # # On Tue, Jan 17, 2017 at 8:58 PM, <Adrian.Danis@data61.csiro.au> # wrote: # # Hi Oak, # # I don't know much about SD cards or this driver but it # seems to me like passing it a physical address of 0 isn't # what you want, and whilst I know nothing about the mmc # hardware it seems reasonable to me that it might hang # trying to DMA to memory that doesn't exist. There is also # the additional problem that even if paddr was correct for # the first page, there is no guarantee that the 5 pages you # have allocated are contiguously physically even though they # will be mapped contiguous virtually. # # My recommendation is to use the page dma allocator in # seL4_libs/libsel4utils/include/sel4utils/page_dma.h, this # will provide you an easy way to allocate/map pages for the # purposes of DMA. So instead of # # void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); # uintptr_t paddr = 0; # # You would have # # ps_dma_man_t dma_man; # error = sel4utils_new_page_dma_alloc(&vka, &vspace, & # dma_man); # void *vaddr = ps_dma_alloc(&dma_man, 5 * PAGE_SIZE_4K, # PAGE_SIZE_4K, 0, PS_MEM_NORMAL); # uintptr_t paddr = ps_dma_pin(&dma_man, vaddr, 5 * # PAGE_SIZE_4K); # # As I said at the start, I don't know if this will actually # fix your current problem, but it's still something you will # need to fix. # # Adrian # # # On Wed 18-Jan-2017 6:31 AM, Norrathep Rattanavipanon wrote: # # My apology that I have to continue the discussion from # the old thread: (http://sel4.systems/pipermail/devel/ # 2016-October/001056.html). # My goal is to read and write data from/to micro sd in # SabreLite platform. # I tried both Adrain and Anna's suggestions in that # thread and they dont seem to fix the problem. Nothing # returns error and I also changed cacheable parameter in # sel4utils_new_pages_at_vaddr to 0 (I believe this is # what Anna meant instead of setting 3rd argument of # vspace_new_pages). # # The code's still stuck inside mmc_block_read function. # I tracked it down and it seems like BRR and BWR # interrupt statuses are never set to 1 # I add my code below, please let me know if anything is # wrong with my code. # # # ps_io_mapper_t io_mapper = {0}; # error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); # assert(error == 0); # # ps_io_ops_t io_ops = { # .io_mapper = io_mapper # }; # # 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(); // return id=3 # error = sdio_init(id, &io_ops, dev); # assert(error == 0); # # mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); # error = mmc_init(dev, &io_ops, mmc_card); # assert(error == 0 && mmc_card != NULL); # # void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); # assert(vaddr != NULL); # # uintptr_t paddr = 0; # printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); # long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here # printf("read %lu bytes\n", read_len); # # # # Thanks # Oak # # # # -- # Norrathep (Oak) Rattanavipanon # M.S. in Computer Science # University of California - Irvine # # # # _______________________________________________ # Devel mailing list # Devel@sel4.systems # https://sel4.systems/lists/listinfo/devel # # # # # # # -- # Norrathep (Oak) Rattanavipanon # M.S. in Computer Science # University of California - Irvine # # # # # -- # Norrathep (Oak) Rattanavipanon # M.S. in Computer Science # University of California - Irvine # # # # # -- # Norrathep (Oak) Rattanavipanon # M.S. in Computer Science # University of California - Irvine # # # # # -- # Norrathep (Oak) Rattanavipanon # M.S. in Computer Science # University of California - Irvine # # # # #-- #Norrathep (Oak) Rattanavipanon #M.S. in Computer Science #University of California - Irvine -- Siwei Zhuang Research Engineer DATA61 | CSIRO E siwei.zhuang@data61.csiro.au T +61 2 8306 0516 Level 3, K17 Building, UNSW Gate 14, Barker Street, Kensington, NSW 2033 www.data61.csiro.au CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61