diff --git a/Kconfig b/Kconfig
index a5991afd1..ab9e308c5 100644
--- a/Kconfig
+++ b/Kconfig
@@ -235,6 +235,13 @@ config ARM_HYPERVISOR_SUPPORT
 
     endchoice
 
+    config ARM_SMMU
+        bool "Enable SystemMMU for Tegra K1 SoC"
+        depends on PLAT_TK1
+        help
+            Support for TK1 SoC-specific SystemMMU
+
+
 source "$KERNEL_PATH/src/arch/arm/Kconfig"
 source "$KERNEL_PATH/src/plat/pc99/Kconfig"
 
diff --git a/include/arch/arm/arch/32/mode/object/structures.bf b/include/arch/arm/arch/32/mode/object/structures.bf
index 4593d2511..35e4ee304 100644
--- a/include/arch/arm/arch/32/mode/object/structures.bf
+++ b/include/arch/arm/arch/32/mode/object/structures.bf
@@ -98,6 +98,45 @@ block vcpu_cap {
 }
 #endif
 
+
+-- IO space caps
+-- each module has an engine that can be enabled
+-- the clients use the same module can be separately enabled
+block io_space_cap {
+    field   capModuleID       16
+    field   capClientID       16
+
+    padding                   24
+    field   capType           8
+}
+
+block io_space_capdata {
+    padding                 32
+
+    field   moduleID        16
+    field   clientID        16
+}
+
+block io_page_directory_cap (capType, capIOPDIsMapped, capIOPDASID, capIOPDBasePtr) {
+    field_high  capIOPDBasePtr      20
+    padding                         12
+
+    padding                         16
+    field       capIOPDASID         7       -- TK1 has 7-bit ASID
+    field       capIOPDIsMapped     1
+    field       capType             8
+}
+
+block io_page_table_cap (capType, capIOPTIsMapped, capIOPTASID, capIOPTBasePtr) {
+    field_high  capIOPTBasePtr      20
+    padding                         12
+
+    padding                         16
+    field       capIOPTASID         7
+    field       capIOPTIsMapped     1
+    field       capType             8
+}
+
 -- NB: odd numbers are arch caps (see isArchCap())
 tagged_union cap capType {
     mask 4 0xe
@@ -132,8 +171,13 @@ tagged_union cap capType {
 
     -- 8-bit tag arch caps
 #ifdef ARM_HYP
-    tag vcpu_cap                               0x0f
+    tag vcpu_cap            0x0f
 #endif /* ARM_HYP */
+
+    -- we use the same names as for x86 IOMMU caps
+    tag io_space_cap            0x1f
+    tag io_page_directory_cap   0x2f
+    tag io_page_table_cap       0x3f
 }
 
 ---- Arch-independent object types
diff --git a/include/plat/tk1/plat/machine/hardware.bf b/include/plat/tk1/plat/machine/hardware.bf
index f2b53f07d..b443ccbb8 100644
--- a/include/plat/tk1/plat/machine/hardware.bf
+++ b/include/plat/tk1/plat/machine/hardware.bf
@@ -10,3 +10,46 @@
 
 base 32
 
+-- Tegra K1 System MMU page table structures
+-- Note: the structures are not the ones defined in
+-- the ARM system mmu specification, but SoC-specific
+-- to the TK1 platform. This is because SoC vendors
+-- tend to design their own SMMUs.
+-- see 16.4.4.1 of the TK1 manual for details
+
+
+-- IO PD entries
+tagged_union iopde page_size {
+    tag iopde_4m        0
+    tag iopde_pt        1
+}
+
+block iopde_pt {
+    field       read        1
+    field       write       1
+    field       secure      1
+    field       page_size   1
+    padding                 6
+    field_high  address     22
+}
+
+block iopde_4m {
+    field       read        1
+    field       write       1
+    field       secure      1
+    field       page_size   1
+    padding                 6
+    field_high  address     12
+    padding                 10
+}
+
+
+-- IO PT entries
+block iopte {
+    field       read        1
+    field       write       1
+    field       secure      1
+    padding                 7
+    field_high  address     22
+}
+