verilog system-verilog formal-languages formal-verification asic

how to write a restore reset formal test which has a long timing

I used to verify a module that consists of a serial port with a set of registers by dynamic tests. One of the test is a restore reset test. The timing sequence is (i) write a random data into a register from serial port (took 40 clock cycles) (ii) put this register in reset and release it (iii) read this register from serial port (took another 40 clock cycles)

This is easily implemented in a dynamic test. Now I want to write this timing formally, but I found formal tools struggled to determine this assertion as the timing is so long, about 82 cycles, the formal tools could not explore so many space states. Is it possible to write such a test formally?

Moreover, the common reset formal test is simple, which takes 1 cycle only, the formal tool start to explore the space states from the state of reset. But now I am trying write a test that saying after the DUT did something, put the reg in reset, read it out, the value is still the reset value.

Solution

Your problem is likely to be that the tool is exploring all the possible states where it could apply reset. That is, if I load register A with 4 and I load register B with 8 and I apply reset, what happens. Now try register A is 5 and register B is 8 and I apply reset, what happens. Now try register A is 6 and .... you get the idea.

You can write these tests, but you need to do a few things:

Don't have a reset at the start. This way all registers are undefined and can take any value. This makes all states in the design easily accessible to the tool.
If necessary, add a constraint so only a single reset pulse can occur, otherwise it may try 1 reset, 2 resets, 3 resets... etc. Hopefully it should realise they all end up in the same state though.
You may possibly have to constrain other inputs to idle so that it doesn't try to use them to explore states that way, but that may be unnecessary.

Note: this tends to be a different set of constraints for reset testing than for other functional tests, so you'll need a separate formal run.