Linting RISC-V designs with ALINT-PRO

As the open-source RISC-V instruction set architecture (ISA) continues to gain momentum, the growing number of RISC-V design solutions, and their flexibility, creates a problem when choosing the most reliable and robust solution from a number of contenders.

Sure, a RISC-V IP design must be compliant to basic ISA standards and should contain a testing suite demonstrating that compliance. But should this be the only metric used when selecting RISC-V IP?

In addition to RISC-V designs Functional Verification and Conformance Testing quality and completeness it is important to also check the quality of the design code with static verification tools.

Aldec’s ALINT-PRO™ provides an extensive and comprehensive means of validating design code robustness without running simulations. The tool includes several checks, such as naming conventions, confirming proper connectivity, and checking the code’s suitability for optimal synthesis.

Post synthesis, ALINT-PRO can be used an equivalency checker to confirm a functional match between simulation results and synthesized HDL - and can find some functional bugs without running simulations.

ALINT-PRO’s code verification rules reside within rule plugins.

To support the static verification of RISC-V ecosystems, a new rules plugin - based on best-practice processor system static analysis – has been added which supports both Verilog and SystemVerilog, the most commonly used languages used in RISC-V IP development.

The following rule sets - which are four of many sets at the heart of ALINT-PRO and accessed through a structured library of chapters and sections - are now available with a RISC-V focus. The user need only select which to include.

• Coding Styles
• Data Types and Operations
• Coding for Implementation
• SystemVerilog Constructs

Coding Styles verify the correctness of constants and variable usage, port definitions, instantiations and object references. For example, this rule verifies that for each constant, its bit width value is matched with the base number part, that there are no continuous assignments on input ports and references on output ports, and that all declared objects are assigned and referenced.

As an illustration, let’s consider the following code example:

Above, the max_value parameter value bit width was erroneously reduced from 4 to 3 bits. Because of this, the max_value is assigned to 0 instead of 8. As a result, the condition for dout never becomes True, causing dout to be assigned to a constant (namely 4’b1111).

The Data Types and Operations rule set verifies various issues related to proper Verilog and SystemVerilog data types usage in expressions. For example, they provide array index-to-bounds checks, warn about mixing signed and unsigned signals in one expression, bit width mismatches and so on. Let’s consider the following code example:

The array variable sel ranges from 0 to 7, while actual data array ranges from 0 to 3. Reading non-existing values causes X-generation on simulation. However, simulation may hide X-generation with the if-then-else or case statements. The advanced static design verification is recommended to locate and correct such issues.

The Coding for Implementation rule set contains important code checks for optimal synthesis, timing closure as well as for resets and Finite State Machine implementation. Also, they ensure an absence of undesired latches, the implementation of a proper reset method and simulation-to-synthesis functional equivalency.

This rule set also contains Finite State Machine-specific rules ensuring proper FSM design, proper states encoding and proper FSM type.

The following two code examples illustrate some of the checks in action.

The first example illustrates the usage of blocking and non-blocking assignments within sequential processes. The following process tries swapping d1 and d2 values while using blocking assignments:

Since the execution flow within the procedure is blocked until the assignment is completed, d1 is assigned to d2 value, and then d2 is assigned to an already changed d1 value (being an old value of d2). As a result, we observe the following waveform:

This situation may also cause simulation-to-synthesis mismatch issues, as some synthesis tools automatically change the blocking assignments within sequential processes to the non-blocking ones.

ALINT-PRO’s RISC-V linting rules ensure the usage of nonblocking assignments in sequential processes only, and the usage of blocking assignments in combinational processes only, leading to the correct behavior of the above example:

Now, let’s see a simple Finite State Machine design check in action:

ALINT-PRO extracts the FSM structure, analyses its topology and its ability to activate all transitions. Here’s the FSM model ALINT-PRO creates from the above code:

Since ‘a’ variable contains three bits only, it cannot exceed the value of 7, prohibiting the activation of “RUN” to “STOP” state transition and making the “STOP” state unreachable; hence the red cross and the ghosting out (grey) of the “STOP” state.

Violation messages are also generated in ALINT-PRO’s violation viewer.

The fourth set of rules to be given an RISC-V focus, SystemVerilog Constructs, ensures optimal SystemVerilog usage for the RTL coding. Checks are applied on instantiations and interfaces on SystemVerilog types and on SystemVerilog procedural blocks, such as always_comb.

Although the SystemVerilog standard allows wildcard connections for instances, the design practice shows that their debug time significantly exceeds the time savings from the wildcard-based RTL coding.

Accordingly, RISC-V rules recommend named connection preferences over the wildcard ones.

The type-based checking suggests the limitations of using 2-state SystemVerilog types such as int, bit, byte, and so on. These types can hide design problems and lead to simulation vs. synthesis mismatches. The one exception is to use an int variable for the iterator variable in for-loops.

SystemVerilog introduced processes such as always_comb, always_ff and always_latch. These processes clearly identify design intent for implementation tools. For example, the following code will generate the “latch insertion” warning in implementation tools, since tools understand the designer’s intent of using this process to implement combinational logic only:

Also, SystemVerilog checks set the preference of using such SystemVerilog constructs as case_inside, unique_case, priority_case and so on over regular Verilog constructs to eliminate possible simulation-to-synthesis mismatches and to express the design intent for the implementation tools in a more clear and concise manner.

The RISC-V Plugin facilitates the advanced static linting for the RISC-V IP designs and System-On-Chips, increasing the quality, safety and robustness of the design code.