/* In TDX a serial of TdIoWrite16 is invoked to write data to the I/O port. */
VOID EFIAPI IoWriteFifo16(IN UINTN Port, IN UINTN Count, IN VOID *Buffer)
/* In TDX a serial of TdIoWrite16 is invoked to write data to the I/O port. */
VOID EFIAPI IoWriteFifo16(IN UINTN Port, IN UINTN Count, IN VOID *Buffer)
{
  if (IsTdxGuest ()) {
    TdIoWriteFifo16 (Port, Count, Buffer);
  } else {
    SevIoWriteFifo16 (Port, Count, Buffer);
  }
}