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.
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:
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.