Hi Peng, The ASIDs defined in smmu.h are arbitrary and defined by the kernel. They get loaded into the different SMMUs as the IOASID for the particular SMMU. Can you explain in what way the PCIE device has the 0 IOASID? Adrian On Mon 16-Jan-2017 10:00 AM, PX wrote: Hi, I am confused by the SMMU management for PCIE device in the updated TK1 VMM. The IO ASID for PCIE device is 0. However, the start IO ASID is from 1 as defined in smmu.h. When initialized, the lookup table, smmu_ioasid_to_pd, has no entry for IO asid 0 at all. I don't understand how the page table for PCIE device is generated and used by SMMU? which part source code should I check ? thanks Peng _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel