In reply to feiphung:
When you write “assume(axis_valid);” the formal verification tool makes axis_valid ==1 for all analyses, meaning that it does not change. If your assertions pass with that signal being 1 or 0, then you would not have a negative report from the tool; thus, the above line does not affect the SMT solver result.
The “assume” defines conditions that should not be considered.
Should your model fail when that input is 0?
Ben Ben@systemverilog.us