VlogHammer

VlogHammer is a Verilog regression tester used to verify the correctness of Yosys's Verilog frontend. At the moment VlogHammer only tests combinatorial circuits described using Verilog expressions.

VlogHammer also exposed a couple of bugs in other programs. Here is a list of currently open bugs found using VlogHammer:

Bug IDLast checkedTitle
issue_001_quartusQuartus 17.0Quartus handling of constant first argument in Verilog ?: operator
issue_002_quartusQuartus 17.0Quartus Verilog bug in handling $signed in an unsigned expression
issue_003_quartusQuartus 17.0Quartus Verilog bug in signdness handling of 2nd shift operand
issue_016_quartusQuartus 17.0Bug in Quartus signed/unsigned handling in power operator
issue_021_quartusQuartus 17.0Quartus hangs on power operations with large exponents
issue_026_quartusQuartus 17.0Incorrect bit-extension of undef const in ?: operator
issue_026_vivadoVivado 2017.2Incorrect bit-extension of undef const in ?: operator
issue_029_quartusQuartus 17.0Handling of large constant RHS in shift operator
issue_031_quartusQuartus 17.0Invalid optimization of or-reduce with undef bits
issue_040_verilatorVerilator 3_906Verilator uses undeclared helper function for power op > 64 bits
issue_042_quartusQuartus 17.0Invalid optimization of reduce expression with undef bits
issue_044_quartusQuartus 17.0Ignored width extension for constant ?: condition
issue_057_quartusQuartus 17.0Quartus handling of partly out-of-bounds parts select
issue_057_verilatorVerilator 3_906Incorrect results with partially out-of-bounds part select
issue_057_vivadoVivado 2017.2Vivado handling of partly out-of-bounds parts select

And here is a list of now closed bugs found using VlogHammer:

Bug IDFixed inTitle
issue_000_verificVerific 463_32_140722Verific sign handling bug in {N{...}} Verilog operator
issue_002_verilatorVerilator GIT 14fcfd8Verilator bug in handling $signed in an unsigned expression
issue_003_verilatorVerilator GIT b631b59Verilator bug with shift, expression width and signedness
issue_004_vivadoVivado 2015.1Strange output-const-zero bug with Vivado + >>> + signedness
issue_005_verilatorVerilator GIT 5c39420Verilator bug in extending $signed
issue_008_verilatorVerilator GIT fb4928bStrange Verilator behavior with power, signdness and more
issue_010_vivadoVivado 2015.1Vivado creates netlist with inputs shorted together
issue_011_icarusIcarus GIT d1c9dd5Icarus Verilog vvp asserts on reduce of one-bit .arith/sub
issue_012_icarusIcarus GIT 68f8de2Icarus Verilog undef propagation bug in power operator
issue_013_icarusIcarus GIT ac3aee0Icarus Verilog signedness handling in binary bitwise operations of constants
issue_014_vivadoVivado 2014.2Vivado GDpGen::implementDivMod(DFNode*, bool): Assertion `TBD' failed.
issue_015_vivadoVivado 2014.2Vivado bug in undef handling for relational operators
issue_016_verilatorVerilator GIT ff19dd9Bug in Verilator signed/unsigned handling in power operator
issue_017_xsimXSim 2015.1Bug in XSIM when combining reduce op and $signed/$unsigned
issue_019_xsimXSim 2015.1XSim implements 0 ** -1 incorrectly
issue_020_xsimXSim 2014.1XSim fails to recognize signed expression with shift in localparam
issue_021_icarusIcarus GIT 66bdbb7Icarus Verilog efficiency of verinum and vpp_net pow() functions
issue_021_verificVerific 463_32_140722Verific hangs on power operations with large exponents
issue_021_xsimXSim 2017.2XSim hangs on power operations with large exponents
issue_022_icarusIcarus GIT ecce1d2Icarus Verilog: internal error: lval-rval width mismatch
issue_023_icarusIcarus GIT 5dcd2e8Icarus Verilog creates huge in-memory arrays for shifts with large rhs
issue_024_icarusIcarus GIT 5a06602Icarus Verilog bug in processing "1'b1 >= |1'bx"
issue_025_icarusIcarus GIT a3450bfIcarus does undef propagation of const adds incorrectly
issue_028_icarusIcarus GIT ed2e339Icarus does undef propagation of const multiplies incorrectly
issue_029_icarusIcarus GIT 020e280Icarus only using the lowest 32 bits of right shift operand
issue_029_verificVerific 463_32_140722Verific only using the lowest 32 bits of right shift operand
issue_029_xsimXSim 2017.2Handling of large RHS in shift operator
issue_032_icarusIcarus GIT bc9382eIcarus confused about signed/unsigned in strange ?: example
issue_033_verificVerific 482_32_150519Verific incorrectly const folds a == 1'bx
issue_034_verilatorVerilator GIT d04eb97Verilator thinks ~|a and ~(|a) are the same thing
issue_035_verilatorVerilator GIT adb39ceVerilator bug in signed/unsigned expression eval
issue_037_verilatorVerilator GIT a985a1fVerilator bug with signedness and arithmetic shift
issue_038_verilatorVerilator GIT 4a58e85Verilator bug in signdness of {..}
issue_039_verilatorVerilator GIT 621c515Verilator Internal Error for shift by undef value
issue_041_verilatorVerilator GIT 6ce2a52Yet another Verilator shift bug
issue_042_verilatorVerilator GIT 5f5a3dbBug in evaluating (defined) expression with undef bits
issue_043_verilatorVerilator GIT d7e4bc1Segfault in code generated by Verilator
issue_045_verilatorVerilator GIT 06744b6Verilator internal fault related to huge shifts
issue_046_verilatorVerilator GIT 06744b6Verilator bug in sign extending special boolean expression
issue_048_icarusIcarus GIT b7b77b2Another strange icarus expression eval bug (large shifts)
issue_049_verilatorVerilator GIT f705f9bAnother Verilator Internal Error for shift by undef value
issue_050_verilatorVerilator GIT f705f9bVerilator returns incorrect expression result
issue_051_verilatorVerilator GIT e8edbadAnother Verilotor bug with large shifts
issue_052_verilatorVerilator GIT e8edbadStrange Verilator "Unsupported" Error
issue_053_verilatorVerilator GIT e8edbadIncorrect results with XNOR/shift expression
issue_054_verificVerific 482_32_150519Verific sign handling in {N{...}} and {...} again
issue_055_verificVerific 482_32_150519Verific uses incorrect width for self-determined division
issue_056_verificVerific 482_32_150519Strange Verific bug with replicate and xor-reduce

The latest publicly released VlogHammer report can be viewed here (use of Google Chrome or Mozilla Firefox is highly recommended). The text below describes what VlogHammer does and how to interpret the report. So keep reading! Alternatively watch the screencast for a quick overview.

VlogHammer compares the implementation generated by Yosys with the implementations generated by the following proprietary free-to-use tools:

  • Xilinx Vivado WebPack
  • Xilinx ISE (XST) WebPack
  • Altera Quartus Web Edition

In addition the behavior of the generated circuits is compared of the behavior described in the original Verilog code, as interpreted by the following Verilog Simulators:

  • Xilinx Isim (bundled with Xilinx ISE)
  • Xilinx XSim (bundled with Xilinx Vivado)
  • Mentor Modelsim (bundled with Altera Quartus II)
  • Icarus Verilog (free software)

I have found bugs in Yosys and all of the above tools (with the exception of Modelsim) using VlogHammer. The bugs in Yosys have been fixed and I share my results in the hope that it will help the vendors of the other tools to fix the bugs in their programs.

The VlogHammer source code can be found on GitHub: https://github.com/cliffordwolf/VlogHammer

The name VlogHammer is inspired by the MC Hammer project from the AArch64 LLVM target. They got the cooler name but we got better google results. :)

Scope of Tests

VlogHammer is using many auto-generated test cases and a few hand-written test cases. The tests do not use behavioral modeling at the moment and concentrate on correct interpretation of Verilog expressions. Our experience with VlogHammer shows that while synthesis of Verilog expressions is not particular hard to do, it is hard-to-do-right for all corner cases. Thus we exposed bugs in Yosys as well as all three 3rd party synthesis tools under test.

While the 3rd party tools are only used for simple logic synthesis, Yosys is used in various ways within VlogHammer, intensively testing the following sub-systems within Yosys:

  • The Verilog frontend, especially
    • The Verilog to RTL netlist generator and
    • the Verilog AST const-folder.
  • The const evaluator for Yosys's coarse- and fine-grain internal representation
  • The standard synthesis pipeline in Yosys (excluding sequential optimizations such as FSM extraction)
  • The built-in SAT solver and the SAT models for all internal cell types.

Procedure

The following procedure is used in VlogHammer
Test case generation
The auto-generated test cases are generated using file names following the pattern rtl/<category>_<id>.v and the hand-written tests are copied to the rtl/ directory. This is usually done as a separate step, allowing for individual selection of test cases by modifying the rtl/ directory. As a full run of VlogHammer may take a couple of days of CPU time, manually selecting individual tests is recommended for most situations. All further steps are conveniently wrapped using the make world command.

Synthesis
Yosys and the 3rd party synthesis tools are used to create Verilog netlists for the RTL input. This step creates syn_<tool>/ directories with one netlist file per test case.

Checking
The Yosys SAT solver is used to verify the synthesis results against the Yosys coarse-grain RTL representation of the original Verilog input. Synthesizeable models of the xilinx and Altera technology cells are used to create SAT models for the outputs of the 3rd party tools. Test cases where any of this verifications fail are marked for report generation. This step creates the check_<tool>/ and cache_<tool>/ directories.

Report Generation
For each test case that resulted in an error in the Checking step, a detailed report is generated. The following steps are performed during this report generation:
  • Formal verification of all synthesis results and the Yosys RTL representation against each other.
  • Simulation of synthesis results and original Verilog using the counter-examples from the previous step as well as random bit patterns as test vectors.
  • Simulation using the Yosys internal const evaluation framework using the same test vectors. Cross-verification of this results with the forward-solutions from the SAT models for the same input.
  • Generation of HTML reports with the results of this tests.

Summary Report
All individual reports are bundled in a single large HTML file that can easily be distributed and browsed on a per-tool basis. The latter is especially useful as the target audience of this reports is primarily interested in the test cases that cause problems with their own tool.

How to read VlogHammer reports

The VlogHammer report is released as single interactive HTML page. It has a (top) navigation bar that allows browsing the individual reports, narrowing the reports to those that only concern an individual tool, and provides a drop-down menu for directly going to the individual report for a test case.

The report for an individual test case consists of 4 parts:

  1. Informal messages, such as the list of synthesis and simulation programs that VlogHammer thinks have troubles with the test case. Note that the Yosys synthesis features are listed as "yosys" and the constant evaluation and SAT solving capabilities are listed as "yosim", although there is no actual software package that is distributed under the name "yosim".
  2. A table summarising the VlogHammer results for this test case.
  3. The Verilog source-code for the test case and a test bench that also contains the test vectors used. Note that this is not the actual test bench used by VlogHammer but a simpler stripped-down version of it.
  4. A list of test patterns that produced interesting results, each listing the input values and the consolidated output values for the different <simulator>.<synthesizer> combinations. The <synthesizer> name rtl refers to the original Verilog source code fed into the simulator.

The most interesting-looking part of the report is the table. It looks like this:

In this example Altera Quartus II produces incorrect synthesis results and Xilinx ISIM produces incorrect simulation results. Modelsim on the other hand simulates the RTL correctly. So a good starting point for fixing this bug is by reproducing the bug using Modelsim as known-good reference and the provided test case and test bench. In case of the incorrect synthesis this can be done by trying to verify the synthesis results using Modelsim. In case of the ISIM bug by comparing ISIM and Modelsim output.

The table can be divided into four regions of interest. The upper-left area contains results from the SAT checks that compare the different synthesis outputs:

This is of course always a symmetrical matrix and all entries on the main diagonal are always "PASS" as a logic netlist is always formally equivalent to itself. This area can contain false-negatives when undefined behavior (such as results from division by zero) is implemented differently by the different tools.

The line below that matrix contains the results of SAT checking the synthesis outputs from the different tools against the Yosys RTL representation:

This line should not contain false negatives, as the RTL SAT models in Yosys do support modeling of undefined behavior (aka. x-bits) and only cases where defined behavior is implemented differently are used to indicate a "FAIL" here.

The lower right line contains checksums of simulation results for the different simulation tools for the original Verilog code of the test case and the auto-generated test vectors:

Here we see that ISIM creates a different output for the original Verilog test case than Modelsim and the Yosys internal const evaluator ("yosim"). Note that there is no column for Icarus Verilog in this case as Icarus Verilog crashed for this particular test case. This results are also used by VlogHammer to extract x-bits for the results for each individual test vector. The output of the synthesized modules is then treated as x for the bits that have been x in the RTL simulation of this individual test vector, so that the implementation of undefined behavior in the different synthesizers does not effect the checksums.

Finally the upper right region contains the checksums for the testbench outputs for the synthesized modules:

If a column in this region is different from the other columns, it is because the simulator returned a different pattern for the x-bits during simulation of the original Verilog code. It is almost certain that two simulators do not return different data bits for the same synthesized module.

In the right region it is possible to get false-positives, because the SAT solver could have generated a test pattern for undefined behavior and thus missed the opportunity to create a test pattern for a real problem (and also because of hash collisions, but this is very unlikely). However, false negatives are not possible here. So we know for certain that there is a bug in at least two tools here, and it is very likely that this two tools are Quartus II and Xilinx ISIM.

The latest publicly released VlogHammer report can be viewed here. Use of Google Chrome or Mozilla Firefox is highly recommended, as the HTML file uses some JavaScript and is not tested with other browsers.

Disclaimer and additional remarks

The test case discussed above is an example based on a screenshot taken in one point in time with one version of the tools discussed. It is the authors hope that in the future all bugs revealed by VlogHammer will be fixed. So it is possible that by the time you read this, the tools discussed here do not suffer of any bug that can be found by VlogHammer.

In fairness I have to add that I have found more bugs in Yosys using VlogHammer than in any of the other tools. Now Yosys performs perfect in-sample. It is likely that there are bugs in Yosys that are exposed by other regressions tests. If anyone with access to different test cases is reading this: I would be delighted to gain access to those test cases.