1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
|
# VeriFuzz [](https://travis-ci.com/ymherklotz/verifuzz)
Verilog Fuzzer to test the major verilog compilers by generating random, valid
and deterministic Verilog. There is a
[presentation](https://yannherklotz.com/docs/presentation.pdf) about VeriFuzz
and a [thesis](https://yannherklotz.com/docs/thesis.pdf) which goes over all the
details of the implementation and results that were found.
It currently supports the following synthesis tools:
- [Yosys](http://www.clifford.at/yosys/)
- [Xst](https://www.xilinx.com/support/documentation/sw_manuals/xilinx11/ise_c_using_xst_for_synthesis.htm)
- [Vivado](https://www.xilinx.com/products/design-tools/ise-design-suite.html)
- [Quartus](https://www.intel.com/content/www/us/en/programmable/downloads/download-center.html)
and the following simulator:
- [Icarus Verilog](http://iverilog.icarus.com)
## Supported Verilog Constructs
The fuzzer generates combinational and behavioural Verilog to test the various
tools. The most notable constructs that are supported and generated are the
following:
- module definitions with parameter definitions, inputs and outputs
- module items, such as instantiations, continuous assignment, always blocks,
initial blocks, parameter and local parameter declarations
- most expressions, for example concatenation, arithmetic operations, ternary
conditional operator
- behavioural code in sequential always blocks
- behavioural control flow such as if-else and for loops
- declaration of wires and variables of any size, signed or unsigned
- bit selection from wires and variables
## Reported bugs
21 bugs were found in total over the course of a month. 8 of those bugs were
reported and 3 were fixed.
### Yosys
| Type | Issue | Confirmed | Fixed |
|---------------|------------------------------------------------------------|-----------|-------|
| Mis-synthesis | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓ | ✓ |
| Mis-synthesis | [Issue 997](https://github.com/YosysHQ/yosys/issues/997) | ✓ | ✓ |
| Crash | [Issue 993](https://github.com/YosysHQ/yosys/issues/993) | ✓ | ✓ |
### Vivado
| Type | Issue | Confirmed | Fixed |
|---------------|-------------------------------------------------------------------------------------------------------------------------------------|-----------|-------|
| Crash | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787) | ✓ | 𐄂 |
| Crash | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136) | ✓ | 𐄂 |
| Mis-synthesis | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789) | ✓ | 𐄂 |
| Mis-synthesis | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓ | 𐄂 |
| Mis-synthesis | [Forum 982419](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Bit-selection-synthesis-mismatch/td-p/982419) | ✓ | 𐄂 |
## Build the Fuzzer
The fuzzer is split into an executable (in the [app](/app) folder) and a
library (in the [src](/src) folder). To build the executable, you will need
[stack](https://docs.haskellstack.org/en/stable/README/) installed. Building
directly using [cabal-install](https://www.haskell.org/cabal/download.html) is
possible but not recommended and not directly supported.
To build the executable:
```
stack build
```
To run the executable:
```
stack exec verifuzz
```
To install the executable (which defaults to installing it in `~/.local`):
```
stack install
```
## Running tests
There are two test-suites that currently test the library. One of the
test-suites tests the random code generation and generation of the acyclic
graph. It also contains some property based tests for this. The other test-suite
uses `doctest` to test the examples that are in the documentation.
To run the test-suites:
```
stack test
```
## Configuration
VeriFuzz can be configured using a [TOML](https://github.com/toml-lang/toml)
file. There are four main sections in the configuration file, an example can be
seen [here](/examples/config.toml).
### Information section
Contains information about the command line tool being used, such as the hash of
the commit it was compiled with and the version of the tool. The tool then
verifies that these match the current configuration, and will emit a warning if
they do not. This ensures that if one wants a deterministic run and is therefore
passing a seed to the generation, that it will always give the same
result. Different versions might change some aspects of the Verilog generation,
which would affect how a seed would generate Verilog.
### Probability section
Provides a way to assign frequency values to each of the nodes in the
AST. During the state-based generation, each node is chosen randomly based on
those probabilities. This provides a simple way to drastically change the
Verilog that is generated, by changing how often a construct is chosen or by not
generating a construct at all.
### Property section
Changes properties of the generated Verilog code, such as the size of the
output, maximum statement or module depth and sampling method of Verilog
programs. This section also allows a seed to be specified, which would mean that
only that particular seed will be used in the fuzz run. This is extremely useful
when wanting to replay a specific failure and the output is missing.
### Synthesiser section
Accepts a list of synthesisers which will be fuzzed. These have to first be
defined in the code and implement the required interface. They can then be
configured by having a name assigned to them and the name of the output Verilog
file. By each having a different name, multiple instances of the same
synthesiser can be included in a fuzz run. The instances might differ in the
optimisations that are performed, or in the version of the synthesiser.
## Acknowledgement
Clifford Wolf's [VlogHammer](http://www.clifford.at/yosys/vloghammer.html) is an
existing Verilog fuzzer that generates random Verilog expressions. It was the
inspiration for the general structure of this fuzzer, which extends the fuzzing
to the behavioural parts of Verilog.
Tom Hawkins' Verilog parser was used to write the lexer, the parser was then
rewritten using [Parsec](https://hackage.haskell.org/package/parsec).
|
