open-source-silicon.dev

Hi everyone. I was wondering if anyone here has used the formal verification tools included with Yosis before. The tool is called SymbiYosis and I have a question about cover statements. I come from a formal background and understand the assert statements and how the logic works. I don't quite understand what exactly the cover statements do. Looking at one of their examples we have:
```   if (~rst) begin
          // waddr and raddr can only be non zero if reset is low
            w_nreset: cover (waddr || raddr);```
I don't understand how this proves that when rst is high, waddr and raddr can only be zero

One thing I failed to notice is that they also assert that waddr and raddr are zero when reset is high, so that is understandable. But I still don't get what would be the use of this cover statement

Another example of a cover statement is:
```            w_full:  cover  (wen &amp;&amp; !ren &amp;&amp; count == MAX_DATA-1);```
Which basically states that there is a point where you would write data and the fifo is almost full. What does this prove?

What is Linen?