diff options
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 138 |
1 files changed, 57 insertions, 81 deletions
@@ -1,10 +1,6 @@ -# VeriFuzz [](https://travis-ci.com/ymherklotz/verifuzz) +# Verismith [](https://travis-ci.com/ymherklotz/verismith) -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. +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 Verismith 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: @@ -19,9 +15,7 @@ and the following simulator: ## 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: +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, @@ -35,13 +29,13 @@ following: ## Reported bugs -21 bugs were found in total over the course of a month. 8 of those bugs were -reported and 3 were fixed. +9 bugs have been reported and confirmed to be bugs by the vendors, out of which 4 have been fixed. ### Yosys | Type | Issue | Confirmed | Fixed | |---------------|------------------------------------------------------------|-----------|-------| +| Mis-synthesis | [Issue 1243](https://github.com/YosysHQ/yosys/issues/1243) | ✓ | ✓ | | 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) | ✓ | ✓ | @@ -56,11 +50,9 @@ reported and 3 were fixed. | 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 +## Install the Fuzzer -The fuzzer now supports building with [nix](https://nixos.org/nix/manual/), -which pulls in all the extra dependencies that are needed to build the -project. The main files and their functions are described below: +The fuzzer now supports building with [nix](https://nixos.org/nix/manual/), which pulls in all the extra dependencies that are needed to build the project. The main files and their functions are described below: - `default.nix`: describes the main Haskell package and it's dependencies that have to be pulled in. @@ -71,82 +63,70 @@ project. The main files and their functions are described below: dependencies so that everything builds nicely. The exact versions of the packages that should be overridden are in [nix](/nix). -It may be possible to build it purely with -[cabal-install](https://hackage.haskell.org/package/cabal-install), however -it may not have all the right versions of the dependencies that are needed. +It may be possible to build it purely with [cabal-install](https://hackage.haskell.org/package/cabal-install), however it may not have all the right versions of the dependencies that are needed. -Instead, stack could be used and the `stack.yaml` file could contain the -overrides that are used by nix. +Instead, stack could be used and the `stack.yaml` file could contain the overrides that are used by nix. -### Build with nix +### Build from hackage -Nix build is completely supported, therefore if nix is installed, building the -project is as simple as +A stable version of Verismith is available on [hackage](https://hackage.haskell.org/package/verismith) and can be installed using cabal directly without having to build the project from the repository: ``` shell -nix-build release.nix +cabal install verismith ``` -If one wants to work in the project with all the right dependencies loaded, one -can use +It will be placed under the `bin` cabal folder which can be added to your path to run Verismith. + +### Build with nix from source + +Nix build is completely supported, therefore if nix is installed, building the project is as simple as + +``` shell +nix-build +``` + +If one wants to work in the project with all the right dependencies loaded, one can use ``` shell nix-shell ``` -### Build with cabal and nix +and use cabal to build and run the program. -After entering a development environment with `nix-shell`, the project can -safely be built with `cabal-install`. +### Build with cabal from source + +After entering a development environment with `nix-shell`, the project can safely be built with `cabal-install`. However, even without `nix`, the project can still be built with cabal alone using: ``` shell -cabal v2-configure -cabal v2-build +cabal configure +cabal build ``` -This should not have to download any extra dependencies and just have to build -the actual project itself. +Verismith can then be run using: + +``` shell +cabal run verismith +``` ## 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). +Verismith 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. +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. +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. +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. +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. ## Benchmark Results @@ -154,34 +134,30 @@ Current benchmark results to compare against. ``` text benchmarking generation/default -time 21.16 ms (17.34 ms .. 24.27 ms) - 0.877 R² (0.742 R² .. 0.977 R²) -mean 20.74 ms (18.40 ms .. 22.70 ms) -std dev 4.741 ms (3.372 ms .. 7.002 ms) -variance introduced by outliers: 85% (severely inflated) +time 65.16 ms (42.67 ms .. 84.90 ms) + 0.837 R² (0.722 R² .. 0.966 R²) +mean 82.87 ms (71.13 ms .. 105.9 ms) +std dev 27.59 ms (15.80 ms .. 42.35 ms) +variance introduced by outliers: 90% (severely inflated) benchmarking generation/depth -time 155.9 ms (90.11 ms .. 209.1 ms) - 0.855 R² (0.680 R² .. 0.983 R²) -mean 92.37 ms (67.36 ms .. 118.2 ms) -std dev 40.56 ms (33.70 ms .. 49.28 ms) -variance introduced by outliers: 88% (severely inflated) +time 860.8 ms (2.031 ms .. 1.488 s) + 0.900 R² (0.668 R² .. 1.000 R²) +mean 483.9 ms (254.1 ms .. 647.6 ms) +std dev 224.4 ms (100.8 ms .. 283.5 ms) +variance introduced by outliers: 74% (severely inflated) benchmarking generation/size -time 117.9 ms (10.21 ms .. 209.1 ms) - 0.616 R² (0.030 R² .. 0.992 R²) -mean 160.5 ms (126.2 ms .. 187.1 ms) -std dev 45.03 ms (27.55 ms .. 68.66 ms) -variance introduced by outliers: 70% (severely inflated) +time 541.1 ms (-749.1 ms .. 1.263 s) + 0.568 R² (0.005 R² .. 1.000 R²) +mean 698.8 ms (498.2 ms .. 897.5 ms) +std dev 229.8 ms (195.0 ms .. 239.7 ms) +variance introduced by outliers: 73% (severely inflated) + ``` ## Acknowledgement -Clifford Wolf's [VlogHammer](http://www.clifford.at/yosys/vloghammer.html) is an -existing Verilog fuzzer that generates random Verilog to test how expressions -are handled in synthesis tools and simulators. It was the inspiration for the -general structure of this fuzzer, which extends the fuzzing to the behavioural -parts of Verilog. +Clifford Wolf's [VlogHammer](http://www.clifford.at/yosys/vloghammer.html) is an existing Verilog fuzzer that generates random Verilog to test how expressions are handled in synthesis tools and simulators. It was the inspiration for thegeneral 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). +Tom Hawkins' Verilog parser was used to write the lexer, the parser was then rewritten using [Parsec](https://hackage.haskell.org/package/parsec). |