mirror of
https://github.com/SpinalHDL/SpinalTemplateSbt.git
synced 2025-10-25 16:58:45 +08:00
Add test folder
This commit is contained in:
@@ -1,24 +0,0 @@
|
||||
package projectname
|
||||
|
||||
import spinal.core._
|
||||
import spinal.core.formal._
|
||||
|
||||
// You need SymbiYosys to be installed.
|
||||
// See https://spinalhdl.github.io/SpinalDoc-RTD/master/SpinalHDL/Formal%20verification/index.html#installing-requirements
|
||||
object MyTopLevelFormal extends App {
|
||||
FormalConfig
|
||||
.withBMC(10)
|
||||
.doVerify(new Component {
|
||||
val dut = FormalDut(MyTopLevel())
|
||||
|
||||
// Ensure the formal test start with a reset
|
||||
assumeInitial(clockDomain.isResetActive)
|
||||
|
||||
// Provide some stimulus
|
||||
anyseq(dut.io.cond0)
|
||||
anyseq(dut.io.cond1)
|
||||
|
||||
// Check the state initial value and increment
|
||||
assert(dut.io.state === past(dut.io.state + U(dut.io.cond0)).init(0))
|
||||
})
|
||||
}
|
||||
@@ -1,31 +0,0 @@
|
||||
package projectname
|
||||
|
||||
import spinal.core._
|
||||
import spinal.core.sim._
|
||||
|
||||
object MyTopLevelSim extends App {
|
||||
Config.sim.compile(MyTopLevel()).doSim { dut =>
|
||||
// Fork a process to generate the reset and the clock on the dut
|
||||
dut.clockDomain.forkStimulus(period = 10)
|
||||
|
||||
var modelState = 0
|
||||
for (idx <- 0 to 99) {
|
||||
// Drive the dut inputs with random values
|
||||
dut.io.cond0.randomize()
|
||||
dut.io.cond1.randomize()
|
||||
|
||||
// Wait a rising edge on the clock
|
||||
dut.clockDomain.waitRisingEdge()
|
||||
|
||||
// Check that the dut values match with the reference model ones
|
||||
val modelFlag = modelState == 0 || dut.io.cond1.toBoolean
|
||||
assert(dut.io.state.toInt == modelState)
|
||||
assert(dut.io.flag.toBoolean == modelFlag)
|
||||
|
||||
// Update the reference model value
|
||||
if (dut.io.cond0.toBoolean) {
|
||||
modelState = (modelState + 1) & 0xff
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user