diff --git a/hw/acpi_piix4.c b/hw/acpi_piix4.c
index 59a4d0f..aa63f0e 100644
--- a/hw/acpi_piix4.c
+++ b/hw/acpi_piix4.c
@@ -29,6 +29,12 @@
 
 //#define DEBUG
 
+#ifdef DEBUG
+# define PIIX4_DPRINTF(format, ...)     printf(format, ## __VA_ARGS__)
+#else
+# define PIIX4_DPRINTF(format, ...)     do { } while (0)
+#endif
+
 #define ACPI_DBG_IO_ADDR  0xb044
 
 #define GPE_BASE 0xafe0
@@ -170,9 +176,7 @@ static void pm_ioport_writew(void *opaque, uint32_t addr, uint32_t val)
     default:
         break;
     }
-#ifdef DEBUG
-    printf("PM writew port=0x%04x val=0x%04x\n", addr, val);
-#endif
+    PIIX4_DPRINTF("PM writew port=0x%04x val=0x%04x\n", addr, val);
 }
 
 static uint32_t pm_ioport_readw(void *opaque, uint32_t addr)
@@ -195,9 +199,7 @@ static uint32_t pm_ioport_readw(void *opaque, uint32_t addr)
         val = 0;
         break;
     }
-#ifdef DEBUG
-    printf("PM readw port=0x%04x val=0x%04x\n", addr, val);
-#endif
+    PIIX4_DPRINTF("PM readw port=0x%04x val=0x%04x\n", addr, val);
     return val;
 }
 
@@ -205,9 +207,7 @@ static void pm_ioport_writel(void *opaque, uint32_t addr, uint32_t val)
 {
     //    PIIX4PMState *s = opaque;
     addr &= 0x3f;
-#ifdef DEBUG
-    printf("PM writel port=0x%04x val=0x%08x\n", addr, val);
-#endif
+    PIIX4_DPRINTF("PM writel port=0x%04x val=0x%08x\n", addr, val);
 }
 
 static uint32_t pm_ioport_readl(void *opaque, uint32_t addr)
@@ -224,9 +224,7 @@ static uint32_t pm_ioport_readl(void *opaque, uint32_t addr)
         val = 0;
         break;
     }
-#ifdef DEBUG
-    printf("PM readl port=0x%04x val=0x%08x\n", addr, val);
-#endif
+    PIIX4_DPRINTF("PM readl port=0x%04x val=0x%08x\n", addr, val);
     return val;
 }
 
@@ -248,9 +246,7 @@ static void apm_ctrl_changed(uint32_t val, void *arg)
 
 static void acpi_dbg_writel(void *opaque, uint32_t addr, uint32_t val)
 {
-#if defined(DEBUG)
-    printf("ACPI: DBG: 0x%08x\n", val);
-#endif
+    PIIX4_DPRINTF("ACPI: DBG: 0x%08x\n", val);
 }
 
 static void pm_io_space_update(PIIX4PMState *s)
@@ -262,9 +258,7 @@ static void pm_io_space_update(PIIX4PMState *s)
         pm_io_base &= 0xffc0;
 
         /* XXX: need to improve memory and ioport allocation */
-#if defined(DEBUG)
-        printf("PM: mapping to 0x%x\n", pm_io_base);
-#endif
+        PIIX4_DPRINTF("PM: mapping to 0x%x\n", pm_io_base);
         register_ioport_write(pm_io_base, 64, 2, pm_ioport_writew, s);
         register_ioport_read(pm_io_base, 64, 2, pm_ioport_readw, s);
         register_ioport_write(pm_io_base, 64, 4, pm_ioport_writel, s);
@@ -450,9 +444,7 @@ static uint32_t gpe_readb(void *opaque, uint32_t addr)
             break;
     }
 
-#if defined(DEBUG)
-    printf("gpe read %x == %x\n", addr, val);
-#endif
+    PIIX4_DPRINTF("gpe read %x == %x\n", addr, val);
     return val;
 }
 
@@ -492,9 +484,7 @@ static void gpe_writeb(void *opaque, uint32_t addr, uint32_t val)
             break;
    }
 
-#if defined(DEBUG)
-    printf("gpe write %x <== %d\n", addr, val);
-#endif
+    PIIX4_DPRINTF("gpe write %x <== %d\n", addr, val);
 }
 
 static uint32_t pcihotplug_read(void *opaque, uint32_t addr)
@@ -512,9 +502,7 @@ static uint32_t pcihotplug_read(void *opaque, uint32_t addr)
             break;
     }
 
-#if defined(DEBUG)
-    printf("pcihotplug read %x == %x\n", addr, val);
-#endif
+    PIIX4_DPRINTF("pcihotplug read %x == %x\n", addr, val);
     return val;
 }
 
@@ -530,16 +518,12 @@ static void pcihotplug_write(void *opaque, uint32_t addr, uint32_t val)
             break;
    }
 
-#if defined(DEBUG)
-    printf("pcihotplug write %x <== %d\n", addr, val);
-#endif
+    PIIX4_DPRINTF("pcihotplug write %x <== %d\n", addr, val);
 }
 
 static uint32_t pciej_read(void *opaque, uint32_t addr)
 {
-#if defined(DEBUG)
-    printf("pciej read %x\n", addr);
-#endif
+    PIIX4_DPRINTF("pciej read %x\n", addr);
     return 0;
 }
 
@@ -558,9 +542,7 @@ static void pciej_write(void *opaque, uint32_t addr, uint32_t val)
     }
 
 
-#if defined(DEBUG)
-    printf("pciej write %x <== %d\n", addr, val);
-#endif
+    PIIX4_DPRINTF("pciej write %x <== %d\n", addr, val);
 }
 
 static int piix4_device_hotplug(void *opaque, PCIDevice *dev, int state);
