Linting tools take advantage of fast and shallow analysis to provide quick feedback on very large designs.
Designers have been using Linting tools for many years to ensure designs adhere to recommended coding guidelines. Linting tools verify that RTL is written in an unambiguous way to ensure that downstream tools (simulation, synthesis, etc.) do not interpret the code incorrectly, resulting in design, verification, timing or implementation issues.
Linting tools take advantage of fast and shallow analysis to provide quick feedback on very large size designs. However, this can lead to a huge number of violations reported – a beast of a problem. As a result, when under typical time pressures, users often do not review each and every violation carefully. Instead, they waive violations without really understanding design failure risks.
There is a growing subset of these violations that can be analyzed functionally, with formal techniques, to validate whether they can cause real design problems or not. This is where formal linting comes in. It significantly reduces the number of violations allowing users to concentrate on real violations.
Let’s consider few examples:
Example 1: Lint violations as part of dead code
input c;
input [4:0] a;
reg [3:0] b;
wire e = a & !a; // or a very complex sequential condition that reduces to 0
always @(posedge c)
if(e) b <= a;
In this example, Lint reports a width mismatch violation for the assignment. However, this violation is reported on part of the design that is dead code since “e” always evaluates to “0”. Formal techniques can be used to automatically filter out this type of violation.
Example 2: Lint reports width mismatch (functionally not a design problem)
input c,r;
wire [3:0] o;
reg [4:0] counter;
always@(posedge c or nedgede r) begin
if(!r) counter <= 0;
else if (counter < 8) counter <= counter +1; // maximum value counter reaches is 7
end
assign o = counter;
In this example, Lint would typically report a width mismatch for the last assignment. Formal analysis realizes that the maximum value counter takes is 7 and thus there is no width mismatch. Such violations can be automatically filtered out.
We can think of functional analysis as an automatic and powerful approach to reduce the noise in Lint violations. Designers can spend time reviewing real design problems instead of just waiving the noisy violations. The advantage of a functional approach to analyzing lint violations is that no additional designer resources are required. Designers need only to turn on formal engines and explore Lint results. It simply requires additional machine time and saves precious designers’ time. Additionally, there are options available to use formal to functionally verify the designs to find FSMs, dead code, and case-related (full / parallel / unique / priority, etc.) issues without requiring any testbench.
There is a smarter way to tame the Linting ‘beast’.
 |
 |
 |
 |
 |
 |
 |
 |
 |
 |
nice article