96
4 Verification and Testing
such, it is beneficial to use programs that statically analyse the code for suspicious
constructs like variables that are never read, truncation of a signal when it is assigned
to another variable, not taking care of overflow in adders, etc. These tools are commonly referred to as linting tools. The tool can also check that the code adheres
to certain ways of coding that are less prone to produce problematic code. Some
tools additionally incorporate formal-verification techniques to detect for instance
unreachable states in a state machine.
Some linting behaviour is commonly built into the synthesizers, but their analysis
is not as exhaustive as with stand-alone tools. Since there are variations on the
different checks that different tools do, this design used Verilator [7], Mentor HDL
Designer [8] and Cadence Incisive HDL Analysis and Lint (HAL) [9]. The tools
have a tendency to report several false positives, for instance, if you bring a packed
configuration-register vector into a module, but only use parts of the vector in that
module, the remaining bits will be reported as unused. Other types of warnings that
might present themselves are if there are unused outputs on a module, or if there are
registers without a reset. For v3 of the SAMPA, Verilator reports 80 warnings and
HAL reports 2 errors and 785 warnings. Numbers for HDL designer is not available
as the tool no longer is able to parse the code for SAMPA v3 due to the introduction
of more System-Verilog code in v3, which is not as well supported by it, but the
numbers for an earlier analysis was on order of what HAL reports.
When the log has been parsed thoroughly once, it is later possible to do only a
diff between the previous log and the current to detect any changes. Running the
linting tools before new changes are committed to the repository reduces the time
spent on unnecessary debugging of code. For instance, a warning will be reported if
the bit-width of a register that is distributed to several modules was changed in one
module, but not updated in all places where it is instantiated or used.
4.1.1.2 Formal Verification
After converting high-level RTL code to lower level gate-level code in the synthesis
process, there is a need to verify that the converted code has the same functionality as
the original source. This can be done through simulations, but simulations are only
as thorough as the testbench itself. Logic Equivalence Checks (LECs) are instead
preferred to simulations as LECs are an exhaustive analysis of all logical possibilities.
A complete analysis with LEC is also faster than an exhaustive testing through
simulations,
To provide redundant testing, this design used both Mentor FormalPro [10] and
Cadence Conformal Equivalence Checker [11] to verify the equivalency between the
RTL, the synthesized code, and the post place and route code.
4 Verification and Testing
such, it is beneficial to use programs that statically analyse the code for suspicious
constructs like variables that are never read, truncation of a signal when it is assigned
to another variable, not taking care of overflow in adders, etc. These tools are commonly referred to as linting tools. The tool can also check that the code adheres
to certain ways of coding that are less prone to produce problematic code. Some
tools additionally incorporate formal-verification techniques to detect for instance
unreachable states in a state machine.
Some linting behaviour is commonly built into the synthesizers, but their analysis
is not as exhaustive as with stand-alone tools. Since there are variations on the
different checks that different tools do, this design used Verilator [7], Mentor HDL
Designer [8] and Cadence Incisive HDL Analysis and Lint (HAL) [9]. The tools
have a tendency to report several false positives, for instance, if you bring a packed
configuration-register vector into a module, but only use parts of the vector in that
module, the remaining bits will be reported as unused. Other types of warnings that
might present themselves are if there are unused outputs on a module, or if there are
registers without a reset. For v3 of the SAMPA, Verilator reports 80 warnings and
HAL reports 2 errors and 785 warnings. Numbers for HDL designer is not available
as the tool no longer is able to parse the code for SAMPA v3 due to the introduction
of more System-Verilog code in v3, which is not as well supported by it, but the
numbers for an earlier analysis was on order of what HAL reports.
When the log has been parsed thoroughly once, it is later possible to do only a
diff between the previous log and the current to detect any changes. Running the
linting tools before new changes are committed to the repository reduces the time
spent on unnecessary debugging of code. For instance, a warning will be reported if
the bit-width of a register that is distributed to several modules was changed in one
module, but not updated in all places where it is instantiated or used.
4.1.1.2 Formal Verification
After converting high-level RTL code to lower level gate-level code in the synthesis
process, there is a need to verify that the converted code has the same functionality as
the original source. This can be done through simulations, but simulations are only
as thorough as the testbench itself. Logic Equivalence Checks (LECs) are instead
preferred to simulations as LECs are an exhaustive analysis of all logical possibilities.
A complete analysis with LEC is also faster than an exhaustive testing through
simulations,
To provide redundant testing, this design used both Mentor FormalPro [10] and
Cadence Conformal Equivalence Checker [11] to verify the equivalency between the
RTL, the synthesized code, and the post place and route code.