blob: 6e2cbac4590185109164500bfd7ee2e0d99140aa (
plain)
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
|
# VeriFuzz [](https://travis-ci.com/ymherklotz/verifuzz)
Verilog Fuzzer to test the major verilog compilers by generating random, valid
verilog.
It currently supports the following synthesisers:
- [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.
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.
## Reported bugs
21 bugs were found in total over the course of a month. 8 of those bugs were
reported and 3 were fixed.
- **MS** :: Mis-synthesis
- **C** :: Crash
### Yosys
| Type | Issue | Confirmed | Fixed |
|------|------------------------------------------------------------|-----------|-------|
| MS | [Issue 1047](https://github.com/YosysHQ/yosys/issues/1047) | ✓ | ✓ |
| MS | [Issue 997](https://github.com/YosysHQ/yosys/issues/997) | ✓ | ✓ |
| C | [Issue 993](https://github.com/YosysHQ/yosys/issues/993) | ✓ | ✓ |
### Vivado
| Type | Issue | Confirmed | Fixed |
|------|-------------------------------------------------------------------------------------------------------------------------------------|-----------|-------|
| C | [Forum 981787](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Verilog-If-statement-nesting-crash/td-p/981787) | ✓ | 𐄂 |
| C | [Forum 981136](https://forums.xilinx.com/t5/Synthesis/Vivado-2018-3-synthesis-crash/td-p/981136) | ✓ | 𐄂 |
| MS | [Forum 981789](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Unsigned-bit-extension-in-if-statement/td-p/981789) | ✓ | 𐄂 |
| MS | [Forum 982518](https://forums.xilinx.com/t5/Synthesis/Vivado-2019-1-Signed-with-shift-in-condition-synthesis-mistmatch/td-p/982518) | ✓ | 𐄂 |
| MS | [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
```
## 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).
|
