USTX in U0S/U1S is broken

Hi,
I found USTX in registers U0S/U1S to be broken. It's always 0.
You can read about how I tested it here: https://www.esp8266.com/viewtopic.php?f=13&t=21169
I've also reported it here: https://bbs.espressif.com/viewtopic.php?f=66&t=56814

However, nobody confirmed it so far.

What's the best way to document this? I've used https://github.com/esp8266/Arduino/blob/master/cores/esp8266/esp8266_peri.h#L252 a lot as reference for developing, so I'd appreciate a comment there.

A possible workaround is to enable Loopback mode and read USRXD instead.

//UART STATUS Registers Bits
#define USTX    31 //TX PIN Level (Bug: Always 0! Enable loopback UxC0 |= 1<<UCLBE and read USRXD)
#define USRTS   30 //RTS PIN Level
#define USDTR   39 //DTR PIN Level
#define USTXC   16 //TX FIFO COUNT (8bit)
#define USRXD   15 //RX PIN Level
#define USCTS   14 //CTS PIN Level
#define USDSR   13 //DSR PIN Level
#define USRXC    0 //RX FIFO COUNT (8bit)

MCVE

#include <Arduino.h>
#include <Ticker.h>
Ticker tick;
// U1 TX: GPIO_02 / D4
#define P_DEBUG 14 // D5
#define DEBUG_HIGH GPOS = 1<<P_DEBUG
#define DEBUG_LOW GPOC = 1<<P_DEBUG

void ICACHE_RAM_ATTR send() {
  DEBUG_HIGH;
  DEBUG_LOW;
  U1F = 0x80;
}

void setup() {
  Serial1.begin(9600);
  pinMode(P_DEBUG,OUTPUT);
  U1S |= 0x01 << USTXC;
  U1D = 10*100;
  tick.attach(0.01, send);
}

void loop() {
  if(U1S & (1<<USTX)) DEBUG_HIGH;
  else DEBUG_LOW;
}

// What I get:
// IO_02: ‾‾‾‾|_______________|‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾|___
// DEBUG: ____|_________________________________|___
// What I expect:
// IO_02: ‾‾‾‾|_______________|‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾|___
// DEBUG: ‾‾‾‾|_______________|‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾|___