MIN_TSB_BYTES
uint_t iommu_tsb_size_min = MIN_TSB_BYTES;
tsb_min = MAX(iommu_tsb_size_min, MIN_TSB_BYTES);