The formal verification is more like a math approach, because basically every digital circuit is nothing but a mapping from input to output, which mathematically fits the definition of Function.
In that sense, the DUT is treated as a math function, whose property is described by SVA (System Verilog Assertion), as illustrated below:
As it is like a math approach, there is no need to prepare test vectors for input and output. And the formal verification tool will use analytic method to check the DUT against those SVAs, and to make sure those properties are satisfied in all conditions.
SpinalHDL also supports Formal Verification, which can be found in
Because Formal Verification is an analytic method, no simulation is needed. We will just leave the rest of it to inquisitive viewers.
2. Functional Simulation
This is the main topic we will discuss today. And for functional simulation, there are also two approaches:
a) static approach, for which we will prepare the expected input/output before hand and make them as test vectors. After the simulation run, the simulation output is matched against the test vectors to verify the DUT, as illustrated below
b) dynamic approach, for which the input is randomized. And the simulation output is compared against a functional model to verify the DUT, as illustrated below:
In the figure above, the driver will generate the random inputs, and feed them to both the simulator and the functional model. And the monitor will capture the simulation outputs, and feed them into the checker to match against the functional model.
Simulation Flow for SpinalHDL
For SpinalHDL, it can support multiple simulators as its backend. And the fastest one will be verilator.
As illustrated in the figure above, the DUT will be compiled into verilog and passed onto the verilator. The verilator will turn them into C++ code and use GCC to make a shared object. The test bench in scala, together with shared object, will finally produce the waveform dump.
Currently the waveform dump can be in either VCD format or FST format. Comparing to VCD (a text format), the FST is a binary format and is a lot smaller than the VCD. So we would recommend using the FST format. Both VCD and FST can be viewed by GTKWave (
https://gtkwave.sourceforge.net/)
Now let’s take a look at the test bench in Hello World example
The code can be checked out with
git clone --depth 1 --branch v1.2.3 https://github.com/PulseRain/FpgaLimerick.git
The test bench is under
HelloWorld/test/spinal/NcoCounterSim.scala
First of all, please note that although SpinalHDL is built on top of Scala language, the test bench is 100% in vanilla Scala. In other words, the test bench is not in SpinalHDL at all. So when we try to get and compare the value from DUT, every data type originally in SpinalHDL has to be converted into Scala type. For example, the IO port could be “bits” in SpinalHDL. But when comparing it to the test vector, we need to use .toInt or .toLong to convert it to a data type understandable by vanilla Scala. Another example is the Boolean type. In SpinalHDL, the Boolean type is actually spelled as Bool, and the True/False literature is spelled with the first level as capital letter. But for vanilla scala language, the Boolean type is spelled as Boolean, with the true/false literature spelled in all small letter. So when we need to use .toBoolean to convert the Boolean type in SpinalHDL to the one in vanilla Scala.
Also, when we drive the DUT’s input ports, we also need to use data type from vanilla Scala. For the Boolean type, it means we should use “true/false” instead of “True/False”, and the syntax would be like
dut.io.srst #= false
Boilerplate Code for Test Bench
As we can see from the Hello World example, the Scala testbench is pretty much in boilerplate form. And we need the following method call:
.withConfig
For the validation of the simulation, this SpinalConfig should match the one used by the DUT generation.
.withWave / .withFstWave / .withVcdWave
If waveform dump is needed, please use those methods to specify the dump format. As we will use verilator as our backend simulator, using .withFstWave is recommended.
.compile
Instantiate the DUT in this method
.doSim
Now this is the main body of the simulation, which we will elaborate next
Multithread Simulation
The Hello World example we use here demonstrates the static approach (test vector matching) for Functional Simulation. (And we will demonstrate the dynamic in later episodes when we talk about cocotb)
The main body of the simulation is contained in the .doSim method in the testbench. It basically has three threads:
*) clkThread
*) measure
*) compare
And they are forked when they are created, and then joined afterwards. For more complicated designs, more than one compare thread could be launched to match multiple test vectors.
The measure thread is not typical in the verification. It is just included in the Hello World as a way to sanity check the verification.
The clkThread is used to initialized the test, and keep track of the start/end of the test with accurate clock count.
To View the Wave
After the simulation, if the waveform is dumped, we can use GTKWave to view the wave. On Windows, the GTKWave can be installed in MSYS2. Please open MSYS2 MINGW64, and type in
pacman -S mingw-w64-x86_64-gtkwave
And then open a command prompt and type in “gtkwave” to launch the waveviewer. For the Hello World example, the wave dump (.fst or .vcd) can be found as .simWorkspace/NcoCounter/test.fst
Post a Comment