Formal prove is a great method to find bugs into our gateware. But for many years, this was reserved to big companies with lot of $$. Some years ago, Clifford opened the method with it’s synthesis software Yosys. Explanation about formal prove with Yosys-smtbmc and can be found in this presentation. Dan Guisselquist (ZipCPU) give lot of great tutorials on formal prove with Verilog and SystemVerilog design on it’s blog. It’s a good start to learn formal prove.
But, Yosys-smtbmc is made for Verilog (and a bit of SystemVerilog). It’s too bad but it’s the only open source formal tool available for gateware.
How can we prove our VHDL, Clash or Chisel gateware ?
One of the solution consist of writing a TOP component in SystemVerilog that integrate the assume/assert/cover method and instantiate our DUT in it. It’s the way Pepijn De Vos choose for verifying it’s VHDL gateware. Its VHDL code is converted into Verilog with the new GHDL feature not-yet-finished and a systemVerilog top component instantiate the VHDL gateware converted in verilog by GHDL synthesis feature.
That’s an interesting way to do it and it can be done in the same way with Chisel. But it’s a bit limited to input/output ports of our gateware. If we want to add some property about internal counters or flags or others internals states machines registers, we have to export it with some conditional preprocessor value like follows:
`ifdef FORMAL
// Declare some signal output ports
`endifIt’s became little bit difficult to do that with chisel and its blackbox system. Then if we want to include formal property under the verilog generated module, we have to open the generated verilog code and write it directly.
It’s not a lasting solution. Because each time we regenerate Verilog code from Chisel, each time we have to re-write formal properties. It’s rapidly become a pain !
To (temporarily) fix this problem a little python tools has been written by Martoni for injecting rules automatically under generated Verilog module. We will see how it’s work in this article with a simple project named ChisNesPad.
ChisNesPad project
ChisNesPad is a little project that aim to drive Super Nintendo Pad with an FPGA.
The gamepad pinout is relativelly easy to find on the web.
For FPGA point of view 3 signals interest us :
- DATA : Gamepad output for serial datas
- LATCH: Game pad input to take a « picture » of 16 buttons
- CLOCK: To synchronize shifter
Internally, the game pad is composed of two 4021 chips serialized.
Basic Chisel/Formal directory structure
The directory structure of the project is following :
/
|-- build.sbt <- scala build configuration
|-- src/ <- all chisel sources
| |-- main/
| |-- scala/
| |-- chisnespad.scala <- Chisel module we will prove
| |-- snespadled.scala <- "top" module to test with
| tang nano (gowin)
|-- formal/ <- formal directory where systemVerilog
| and sby yosys configuration are.
|-- platform/ <- some usefull file for synthesis with
final platform (gowin).To generate Verilog file we just have to launch following command in main project directory:
sbt 'runMain chisnespad.ChisNesPad'The generated file will be named ChisNesPad.v
smtbmcify tool
smtbmcify tool is a python3 module that can be found on this github project. It can be installed on the dev machine as follow:
$ git clone https://github.com/Martoni/chisverilogutils
$ cd chisverilogutils/smtbmcify
$ python -m pip install -e .A command named smtbmcify will then be available on system :
$ smtbmcify -h
Usages:
$ python smtbmcify.py [options]
-h, --help print this help message
-v, --verilog=module.v verilog module to read
-f, --formal=formal.sv formals rules
-o, --output=name.sv output filename, default is moduleFormal.sv
To use smtbmc formal tools with smtbmcify we will need two more source/configuration files :
ChisNesPadRules.svThat contain SystemVerilog formals propertiesChisNesPadRules.sbyThat contain yosys-smtbmc script configuration
These two files must be saved in formal/ directory. sby files are SymbiYosys configuration files, installation instruction of SymbiYosys can be found here.
For simply testing, the rule (written in file ChisNesPadRules.sv) we want to « inject » is following:
//BeginModule:ChisNesPad
always@(posedge clock) begin
assume(io_dlatch == 1'b1);
assert(stateReg == 2'b00);
end
//EndModule:ChisNesPadWith this rule, we assert that if io.dlatch output is 1, the internal stateReg will be set to sInit state (00).
The comments BeginModule and EndModule must be set with the exact chisel module name :
//...
class ChisNesPad (val mainClockFreq: Int = 100,
val clockFreq: Int = 1,
val regLen: Int = 16) extends Module {
val io = IO(new Bundle{
//...Hence, the tool smtbmcify will find the module in verilog generated module and inject the rules at the end of it:
$ cd formal
$ smtbmcify -v ../ChisNesPad.v -f ChisNesPadRules.sv -o ChisNesPadFormal.sv...
end else begin
validReg <= _T_19;
end
_T_21 <= stateReg == 2'h1;
_T_23 <= stateReg == 2'h0;
end
//BeginModule:ChisNesPad
always@(posedge clock) begin
assume(io_dlatch == 1'b1);
assert(stateReg == 2'b00);
end
//EndModule:ChisNesPad
endmoduleThe module name is mandatory because a Chisel Verilog generated module can contain several module.
Some naming convention should be know to write systemverilog rules:
- dot ‘.’ syntax is replaced with ‘_’ in Verilog: for this example
io.dlatchchisel signal is replaced withio_dlatch. - Some registers can disappear (be simplified) in generated Verilog. dontTouch() can be used to keep it in generated Verilog.
To launch the formal engine we are using a sby script like it (named ChisNesPad.sby:
[options]
mode bmc
depth 30
[engines]
smtbmc
[script]
read -formal ChisNesPadFormal.sv
prep -top ChisNesPad
[files]
ChisNesPadFormal.svThe launch command is :
$ sby ChisNesPad.sby
SBY 21:12:00 [ChisNesPad] Copy 'ChisNesPadFormal.sv' to 'ChisNesPad/src/ChisNesPadFormal.sv'.
SBY 21:12:00 [ChisNesPad] engine_0: smtbmc
SBY 21:12:00 [ChisNesPad] base: starting process "cd ChisNesPad/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 21:12:00 [ChisNesPad] base: finished (returncode=0)
SBY 21:12:00 [ChisNesPad] smt2: starting process "cd ChisNesPad/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 21:12:00 [ChisNesPad] smt2: finished (returncode=0)
SBY 21:12:00 [ChisNesPad] engine_0: starting process "cd ChisNesPad; yosys-smtbmc --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 21:12:01 [ChisNesPad] engine_0: ## 0:00:00 Solver: yices
SBY 21:12:01 [ChisNesPad] engine_0: ## 0:00:00 Checking assumptions in step 0..
SBY 21:12:01 [ChisNesPad] engine_0: ## 0:00:00 Checking assertions in step 0..
[...]
SBY 21:12:01 [ChisNesPad] engine_0: ## 0:00:00 Checking assumptions in step 29..
SBY 21:12:01 [ChisNesPad] engine_0: ## 0:00:00 Checking assertions in step 29..
SBY 21:12:01 [ChisNesPad] engine_0: ## 0:00:00 Status: passed
SBY 21:12:01 [ChisNesPad] engine_0: finished (returncode=0)
SBY 21:12:01 [ChisNesPad] engine_0: Status returned by engine: pass
SBY 21:12:01 [ChisNesPad] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:12:01 [ChisNesPad] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:12:01 [ChisNesPad] summary: engine_0 (smtbmc) returned pass
SBY 21:12:01 [ChisNesPad] DONE (PASS, rc=0)
This simple rule finish with success (PASS) and create a directory with all generated file under it.
Rapidly, we will need a Makefile to launch each step of this procedure and to clean generated file.
Of course, all code described so far is available on the github ChisNesPad project.
Find bugs
Ok the test we done so far PASS without problem. Let’s find a bug adding this rules in ChisNesPadRules.sv :
always@(posedge clock) begin
assert(regCount <= 16);
endThis rule generate a FAIL :
$ make
cd ..;sbt "runMain chisnespad.ChisNesPad"
[info] Loading project definition from /home/fabien/myapp/chisNesPad/project
[info] Loading settings for project chisnespad from build.sbt ...
[info] Set current project to chisNesPad (in build file:/home/fabien/myapp/chisNesPad/)
[warn] Multiple main classes detected. Run 'show discoveredMainClasses' to see the list
[info] running chisnespad.ChisNesPad
Generating Verilog sources for ChisNesPad Module
[info] [0.004] Elaborating design...
[info] [1.735] Done elaborating.
Total FIRRTL Compile Time: 1396.1 ms
[success] Total time: 5 s, completed Feb 3, 2020 9:49:48 PM
smtbmcify -v ../ChisNesPad.v -f ChisNesPadRules.sv -o ChisNesPadFormal.sv
Generating file ChisNesPadFormal.sv
1 module will be filled :
ChisNesPad
rm -rf ChisNesPad
sby ChisNesPad.sby
SBY 21:49:48 [ChisNesPad] Copy 'ChisNesPadFormal.sv' to 'ChisNesPad/src/ChisNesPadFormal.sv'.
SBY 21:49:48 [ChisNesPad] engine_0: smtbmc
SBY 21:49:48 [ChisNesPad] base: starting process "cd ChisNesPad/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 21:49:49 [ChisNesPad] base: finished (returncode=0)
SBY 21:49:49 [ChisNesPad] smt2: starting process "cd ChisNesPad/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 21:49:49 [ChisNesPad] smt2: finished (returncode=0)
SBY 21:49:49 [ChisNesPad] engine_0: starting process "cd ChisNesPad; yosys-smtbmc --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Solver: yices
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Checking assumptions in step 0..
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Checking assertions in step 0..
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Checking assumptions in step 1..
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Checking assertions in step 1..
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 BMC failed!
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Assert failed in ChisNesPad: ChisNesPadFormal.sv:230
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Writing trace to VCD file: engine_0/trace.vcd
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Writing trace to constraints file: engine_0/trace.smtc
SBY 21:49:49 [ChisNesPad] engine_0: ## 0:00:00 Status: failed (!)
SBY 21:49:49 [ChisNesPad] engine_0: finished (returncode=1)
SBY 21:49:49 [ChisNesPad] engine_0: Status returned by engine: FAIL
SBY 21:49:49 [ChisNesPad] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:49:49 [ChisNesPad] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:49:49 [ChisNesPad] summary: engine_0 (smtbmc) returned FAIL
SBY 21:49:49 [ChisNesPad] summary: counterexample trace: ChisNesPad/engine_0/trace.vcd
SBY 21:49:49 [ChisNesPad] DONE (FAIL, rc=2)
make: *** [Makefile:10: ChisNesPad/PASS] Error 2An error is found at second step. A vcd trace is generated that we can see with gtkwave:
$ gtkwave ChisNesPad/engine_0/trace.vcd
We can also get verilog testbench that reproduce the bug under the same directory (trace_tb.v).
The problem here is that we didn’t define initial reset condition as explained in ZipCPU course. To solve this problem we have to change the rule adding initial rules (reset should be set at the begining) and assert counter value only when reset is not set :
initial
assume(reset==1'b1);
always@(posedge clock) begin
if(reset == 1'b0)
assert(regCount <= 16);
endWith that rules, it pass :
$ make
cd ..;sbt "runMain chisnespad.ChisNesPad"
[info] Loading project definition from /home/fabien/myapp/chisNesPad/project
[info] Loading settings for project chisnespad from build.sbt ...
[info] Set current project to chisNesPad (in build file:/home/fabien/myapp/chisNesPad/)
[warn] Multiple main classes detected. Run 'show discoveredMainClasses' to see the list
[info] running chisnespad.ChisNesPad
Generating Verilog sources for ChisNesPad Module
[info] [0.004] Elaborating design...
[info] [1.612] Done elaborating.
Total FIRRTL Compile Time: 1324.0 ms
[success] Total time: 5 s, completed Feb 3, 2020 10:04:37 PM
smtbmcify -v ../ChisNesPad.v -f ChisNesPadRules.sv -o ChisNesPadFormal.sv
Generating file ChisNesPadFormal.sv
1 module will be filled :
ChisNesPad
rm -rf ChisNesPad
sby ChisNesPad.sby
SBY 22:04:38 [ChisNesPad] Copy 'ChisNesPadFormal.sv' to 'ChisNesPad/src/ChisNesPadFormal.sv'.
SBY 22:04:38 [ChisNesPad] engine_0: smtbmc
SBY 22:04:38 [ChisNesPad] base: starting process "cd ChisNesPad/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 22:04:38 [ChisNesPad] base: finished (returncode=0)
SBY 22:04:38 [ChisNesPad] smt2: starting process "cd ChisNesPad/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 22:04:38 [ChisNesPad] smt2: finished (returncode=0)
SBY 22:04:38 [ChisNesPad] engine_0: starting process "cd ChisNesPad; yosys-smtbmc --presat --unroll --noprogress -t 30 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 22:04:38 [ChisNesPad] engine_0: ## 0:00:00 Solver: yices
SBY 22:04:38 [ChisNesPad] engine_0: ## 0:00:00 Checking assumptions in step 0..
[...]
SBY 22:04:39 [ChisNesPad] engine_0: ## 0:00:00 Checking assertions in step 29..
SBY 22:04:39 [ChisNesPad] engine_0: ## 0:00:00 Status: passed
SBY 22:04:39 [ChisNesPad] engine_0: finished (returncode=0)
SBY 22:04:39 [ChisNesPad] engine_0: Status returned by engine: pass
SBY 22:04:39 [ChisNesPad] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 22:04:39 [ChisNesPad] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 22:04:39 [ChisNesPad] summary: engine_0 (smtbmc) returned pass
SBY 22:04:39 [ChisNesPad] DONE (PASS, rc=0)
This is just a little introduction on how to use yosys-smtbmc and symbiYosys to formally prove your chisel design.
Maybe this formal rules injector will be integrated in Chisel a day ?
