In reply to ben@SystemVerilog.us:
Hi Ben,
Seems it does not work. I added the assumption, but nothing changed. Then I changed the assumption to be tag<2, so it could only be 0 and 1. But the assertion is still vacuity. I also used the analysis tool provided by the formal tool to analyze this vacuity, but it reported: no constraint is related to this.