RFC: FormalAfterReset

[danielkasza]

This is related to #4.

These changes add a new FormalAfterReset trait for modules where the assertions should only apply after a reset. This is just a prototype to start the discussion. I will to redo the whole thing if I have to.

[danielkasza]

I am going to close this and work on a bigger rework of the library. A couple of things I want to change:

• Use FIRRTL transformations to add cover statements
• Remove numResets and timeSinceReset
• Focus only on verification after the initial reset

[tdb-alcorn]

• Use FIRRTL transformations to add cover statements

Sounds like a great approach.

• Remove numResets and timeSinceReset

Do you have any ideas on how to replace them? IMO timeSinceReset is necessary because sometimes you know that an assertion will need some time to become valid.

• Focus only on verification after the initial reset

This is good, I'd only caution to make sure you include some kind of escape valve for the odd situation where you do want a property to be true universally.

[danielkasza]

Do you have any ideas on how to replace them?

Yes. My plan is to:

• use a blackbox to add a 1b "reset done" register
• Add a new method for checking if we are at least n clocks after reset
• Create a saturating counter for each call of this method that counts up to n

This way, we do not have to worry about the counter ever overflowing.

I am also planning to change the past API to:

• Not require a block
• Work across resets

The reason for this is that I found that requiring a block for each past value leads to very nested code when asserting the behavior of state machines because you have to grab multiple values from the past.

I'd only caution to make sure you include some kind of escape valve for the odd situation where you do want a property to be true universally.

I agree. I will include this in my prototype.