实用程序和原语(Utilities and primitives)

一、断言/时钟/复位(Assertions/clock/reset)

在复位时, 断言经常是计时和禁用的, 这也同样适用于假设和覆盖。

如果你想在复位期间保持断言使能, 你可以用如下操作：

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

二、给定信号初始值(Specifying the initial value of a signal)

例如, 对于当前时钟域的复位信号(在顶层很有用)：

ClockDomain.current.readResetWire initial(False)

三、给定初始化声明(Specifying a initial assumption)

assumeInitial(clockDomain.isResetActive)

四、存储内容(Memory content)

如果在你的设计中有Mem, 并且你想检查它的内容, 你可以用如下方式：

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

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

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

五、在复位区域内给定断言(Specifying assertion in the reset scope)

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

六、形式化原语(Formal primitives)

语句	返回类型	描述
`assert(Bool)`
`assume(Bool)`
`cover(Bool)`
`past(that: T, delay: Int)`	T	返回延时`delay`周期的`that`(默认1周期)
`rose(that: Bool)`	Bool	当`that`从False变换成True, 返回True
`fall(that: Bool)`	Bool	当`that`从False变换成True, 返回True
`changed(that: Bool)`	Bool	当`that`当前值与上周期相比发生变化, 返回True
`stable(that: Bool)`	Bool	当`that`当前值与上周期相比没有发生变化, 返回True
`initstate()`	Bool	第一个周期返回True

你也可以在past用initstate：
when(past(enable) init(False)){ ... }