xhcidma32
static int xhcidma32;
&xhcidma32, 0, "Set to only use 32-bit DMA for the XHCI controller");
TUNABLE_INT("hw.usb.xhci.dma32", &xhcidma32);
xhcidma32 == 0 && dma32 == 0) ? 64 : 32;