形式化验证

介绍

SpinalHDL 允许生成 SystemVerilog 断言 (SVA) 的子集。主要是断言（assert）、假设（assume）、覆盖（cover）和其他一些内容。

此外，它还提供了形式化验证后端，允许直接在开源 Symbi-Yosys 工具链中运行形式化验证。

形式化验证后端

您可以通过以下方式运行组件的形式化验证：

import spinal.core.formal._
FormalConfig.withBMC(15).doVerify(new Component {
    // Toplevel to verify
})

目前支持3种模式：

withBMC(depth)
withProve(depth)
withCover(depth)

安装要求

要安装 Symbi-Yosys，您有几种选择。您可以在以下位置获取预编译包：

https://github.com/YosysHQ/oss-cad-suite-build/releases
https://github.com/YosysHQ/fpga-toolchain/releases（EOL - 由 oss-cad-suite 取代）

或者你可以从头开始编译：

https://symbiyosys.readthedocs.io/en/latest/install.html

示例

外部断言

这是一个简单计数器和相应的形式化测试代码的示例。

import spinal.core._

// Here is our DUT
class LimitedCounter extends Component {
  // The value register will always be between [2:10]
  val value = Reg(UInt(4 bits)) init(2)
  when(value < 10) {
    value := value + 1
  }
}

object LimitedCounterFormal extends App {
  // import utilities to run the formal verification, but also some utilities to describe formal stuff
  import spinal.core.formal._

  // Here we run a formal verification which will explore the state space up to 15 cycles to find an assertion failure
  FormalConfig.withBMC(15).doVerify(new Component {
    // Instantiate our LimitedCounter DUT as a FormalDut, which ensure that all the outputs of the dut are:
    // - directly and indirectly driven (no latch / no floating signal)
    // - allows the current toplevel to read every signal across the hierarchy
    val dut = FormalDut(new LimitedCounter())

    // Ensure that the state space start with a proper reset
    assumeInitial(ClockDomain.current.isResetActive)

    // Check a few things
    assert(dut.value >= 2)
    assert(dut.value <= 10)
  })
}

内部断言

如果您愿意，可以将形式化验证语句直接嵌入到 DUT 中：

class LimitedCounterEmbedded extends Component {
  val value = Reg(UInt(4 bits)) init(2)
  when(value < 10) {
    value := value + 1
  }

  // That code block will not be in the SpinalVerilog netlist by default. (would need to enable SpinalConfig().includeFormal. ...
  GenerationFlags.formal {
    assert(value >= 2)
    assert(value <= 10)
  }
}

object LimitedCounterEmbeddedFormal extends App {
  import spinal.core.formal._

  FormalConfig.withBMC(15).doVerify(new Component {
    val dut = FormalDut(new LimitedCounterEmbedded())
    assumeInitial(ClockDomain.current.isResetActive)
  })
}

外部激励

如果您的 DUT 有输入，您需要从测试代码中驱动它们。您可以使用所有常规硬件语句来执行此操作，但您也可以使用形式化验证中的 anyseq、anyconst、allseq、allconst 语句：

class LimitedCounterInc extends Component {
  // Only increment the value when the inc input is set
  val inc = in Bool()
  val value = Reg(UInt(4 bits)) init(2)
  when(inc && value < 10) {
    value := value + 1
  }
}

object LimitedCounterIncFormal extends App {
  import spinal.core.formal._

  FormalConfig.withBMC(15).doVerify(new Component {
    val dut = FormalDut(new LimitedCounterInc())
    assumeInitial(ClockDomain.current.isResetActive)
    assert(dut.value >= 2)
    assert(dut.value <= 10)

    // Drive dut.inc with random values
    anyseq(dut.inc)
  })
}

假设内存中的内容

这是一个示例，我们希望防止值 1 出现在内存中：

class DutWithRam extends Component {
  val ram = Mem.fill(4)(UInt(8 bits))
  val write = slave(ram.writePort)
  val read = slave(ram.readAsyncPort)
}

object FormalRam extends App {
  import spinal.core.formal._

  FormalConfig.withBMC(15).doVerify(new Component {
    val dut = FormalDut(new DutWithRam())
    assumeInitial(ClockDomain.current.isResetActive)

    // assume that no word in the ram has the value 1
    for(i <- 0 until dut.ram.wordCount) {
      assumeInitial(dut.ram(i) =/= 1)
    }

    // Allow the write anything but value 1 in the ram
    anyseq(dut.write)
    clockDomain.withoutReset() { // As the memory write can occur during reset, we need to ensure the assume apply there too
      assume(dut.write.data =/= 1)
    }

    // Check that no word in the ram is set to 1
    anyseq(dut.read.address)
    assert(dut.read.data =/= 1)
  })
}

实用工具和原语

断言/时钟/复位

断言（assert）是一直被时钟驱动的，但在复位期间被禁用。这也适用于假设（assume）和覆盖（cover）。

如果您想在复位期间保持断言被检查，您可以执行以下操作：

ClockDomain.current.withoutReset() {
  assert(wuff === 0)
}

指定信号的初始值

For instance, for the reset signal of the current clockdomain (useful at the top)

ClockDomain.current.readResetWire initial(False)

指定初始假设

assumeInitial(clockDomain.isResetActive)

内存内容（Mem）检查

如果您的设计中有 Mem，并且想要检查其内容，可以通过以下方式进行：

// Manual access
for(i <- 0 until dut.ram.wordCount) {
  assumeInitial(dut.ram(i) =/= X) // No occurrence of the word X
}

assumeInitial(!dut.ram.formalContains(X)) // No occurrence of the word X

assumeInitial(dut.ram.formalCount(X) === 1) // only one occurrence of the word X

在复位的时候进行断言检查，可以这样做

ClockDomain.current.duringReset {
  assume(rawrrr === 0)
  assume(wuff === 3)
}