verismith: Random verilog generation and simulator testing.

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Verismith provides random verilog generation modules implementing functions to test supported simulators.


[Skip to Readme]

Properties

Versions 0.4.0.0, 0.4.0.1, 0.4.0.1, 0.5.0.0, 0.5.0.1, 0.6.0.0, 0.6.0.1, 0.6.0.2, 1.0.0.0, 1.0.0.1, 1.0.0.2
Change log None available
Dependencies array (>=0.5 && <0.6), base (>=4.7 && <5), binary (>=0.8.5.1 && <0.9), blaze-html (>=0.9.0.1 && <0.10), bytestring (>=0.10 && <0.11), cryptonite (>=0.25 && <0.26), deepseq (>=1.4.3.0 && <1.5), DRBG (>=0.5 && <0.6), exceptions (>=0.10.0 && <0.11), fgl (>=5.6 && <5.8), fgl-visualize (>=0.1 && <0.2), filepath (>=1.4.2 && <1.5), gitrev (>=1.3.1 && <1.4), hedgehog (>=1.0 && <1.2), lens (>=4.16.1 && <4.18), lifted-base (>=0.2.3 && <0.3), memory (>=0.14 && <0.15), monad-control (>=1.0.2 && <1.1), optparse-applicative (>=0.14 && <0.15), parsec (>=3.1 && <3.2), prettyprinter (>=1.2.0.1 && <1.3), random (>=1.1 && <1.2), recursion-schemes (>=5.0.2 && <5.2), shakespeare (>=2 && <2.1), shelly (>=1.8.0 && <1.9), statistics (>=0.14.0.2 && <0.16), template-haskell (>=2.13.0 && <2.15), text (>=1.2 && <1.3), time (>=1.8.0.2 && <1.9), tomland (>=1.0 && <1.2), transformers (>=0.5 && <0.6), transformers-base (>=0.4.5 && <0.5), unordered-containers (>=0.2.10 && <0.3), vector (>=0.12.0.1 && <0.13), verismith [details]
License BSD-3-Clause
Copyright 2018-2019 Yann Herklotz
Author Yann Herklotz
Maintainer yann [at] yannherklotz [dot] com
Category Hardware
Home page https://github.com/ymherklotz/verismith#readme
Source repo head: git clone https://github.com/ymherklotz/verismith
this: git clone https://github.com/ymherklotz/verismith(tag v0.4.0.0)
Uploaded by ymherklotz at 2019-12-25T20:13:57Z

Modules

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


Readme for verismith-0.4.0.1

[back to package description]

Verismith Build Status

Verilog Fuzzer to test the major verilog compilers by generating random, valid and deterministic Verilog. There is a presentation about Verismith and a thesis which goes over all the details of the implementation and results that were found.

It currently supports the following synthesis tools:

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:

Reported bugs

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
Mis-synthesis Issue 1047
Mis-synthesis Issue 997
Crash Issue 993

Vivado

Type Issue Confirmed Fixed
Crash Forum 981787 𐄂
Crash Forum 981136 𐄂
Mis-synthesis Forum 981789 𐄂
Mis-synthesis Forum 982518 𐄂
Mis-synthesis Forum 982419 𐄂

Install the Fuzzer

The fuzzer now supports building with nix, which pulls in all the extra dependencies that are needed to build the project. The main files and their functions are described below:

It may be possible to build it purely with 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.

Build from hackage

A stable version of Verismith is available on hackage and can be installed using cabal directly without having to build the project from the repository:

cabal install verismith

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

nix-build

If one wants to work in the project with all the right dependencies loaded, one can use

nix-shell

and use cabal to build and run the program.

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:

cabal configure
cabal build

Verismith can then be run using:

cabal run verismith

Configuration

Verismith can be configured using a TOML file. There are four main sections in the configuration file, an example can be seen here.

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.

Benchmark Results

Current benchmark results to compare against.

benchmarking generation/default
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                 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                 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 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.