Stucked at UART formal verification

In reply to ben@SystemVerilog.us:

If I treat my UART coding as blackbox, I would not be able to verify it formally.

Note: I am not using any UVM library. I am just using a free formal tool, yosys-smtbmc