0

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.

4

1 回答 1

0

您的问题很可能是该工具正在探索它可以应用重置的所有可能状态。也就是说，如果我用 4 加载寄存器 A，用 8 加载寄存器 B 并应用复位，会发生什么。现在尝试寄存器 A 为 5，寄存器 B 为 8，然后我应用复位，会发生什么。现在尝试寄存器 A 是 6 并且 .... 你明白了。

您可以编写这些测试，但您需要做一些事情：

  • 开始时不要重置。这样所有寄存器都是未定义的，可以取任何值。这使得工具可以轻松访问设计中的所有状态。
  • 如有必要，添加一个约束，以便只能发生一个复位脉冲，否则它可能会尝试 1 次复位、2 次复位、3 次复位……等等。希望它应该意识到它们最终都处于相同的状态。
  • 您可能必须将其他输入限制为空闲，以便它不会尝试以这种方式使用它们来探索状态，但这可能是不必要的。

注意：与其他功能测试相比，这往往是重置测试的一组不同约束，因此您需要单独的正式运行。

于 2016-01-12T17:21:56.503 回答