diff -r 5603534c62f9 xen/drivers/passthrough/iommu.c
--- a/xen/drivers/passthrough/iommu.c	Tue Jun 03 09:41:19 2008 +0100
+++ b/xen/drivers/passthrough/iommu.c	Fri Jun 06 11:06:30 2008 +0200
@@ -68,7 +68,7 @@ int assign_device(struct domain *d, u8 b
     if ( (rc = hd->platform_ops->assign_device(d, bus, devfn)) )
         return rc;
 
-    if ( has_iommu_pdevs(d) && !need_iommu(d) )
+    if ( has_iommu_pdevs(d) && !is_hvm_domain(d) && !need_iommu(d) )
     {
         d->need_iommu = 1;
         return iommu_populate_page_table(d);
@@ -114,6 +114,16 @@ void iommu_domain_destroy(struct domain 
     if ( !iommu_enabled || !hd->platform_ops )
         return;
 
+    if ( !is_hvm_domain(d) && !need_iommu(d)  )
+        return;
+
+    if ( need_iommu(d) )
+    {
+        d->need_iommu = 0;
+        hd->platform_ops->teardown(d);
+        return;
+    }
+
     if ( hvm_irq_dpci != NULL )
     {
         for ( i = 0; i < NR_IRQS; i++ )
@@ -207,10 +217,10 @@ static int iommu_setup(void)
     iommu_enabled = (rc == 0);
 
  out:
-    if ( !iommu_enabled || !vtd_enabled )
+    if ( !iommu_enabled )
         iommu_pv_enabled = 0;
     printk("I/O virtualisation %sabled\n", iommu_enabled ? "en" : "dis");
-    if (iommu_enabled)
+    if ( iommu_enabled )
         printk("I/O virtualisation for PV guests %sabled\n",
                iommu_pv_enabled ? "en" : "dis");
     return rc;