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

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

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

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

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

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

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

```Scala
ClockDomain.current.readResetWire initial(False)
```

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

```Scala
assumeInitial(clockDomain.isResetActive)
```

### 四、存储内容(Memory content)

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

```Scala
// 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)

```Scala
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：
> ```Scala
> when(past(enable) init(False)){ ... }
> ```