Questa® SLEC, the formal analysis app from Mentor, was designed to automatically compare a block of code ("specification" RTL) with its functional equivalent that has been slightly modified ("implementation" RTL), helping design teams save considerable amounts of time and resources. Codasip, the leading provider of configurable RISC-V® IP, has come up with a new use of this tool: the verification team uses it to compare a fully UVM-verified HDL code, for example Verilog, with a new HDL output, such as SystemVerilog or VHDL, making sure that they are functionally identical – in a fraction of the time needed before. Total time required for full verification of a new processor design is then reduced by up to 66%, depending on the desired number of HDL outputs.
WHAT IS SLEC?
SLEC, or the Sequential Logic Equivalence Check, is used to formally verify that two designs that differ sequentially but are supposed to be functionally equivalent, really are equivalent—that is, that they produce the same output for the same input at all times. SLEC is typically used when a design has been modified in a small, yet operationally critical way, and verification of the new code is needed. RTL simulation can be also used for this purpose, but it is limited in testing all corner cases, which means that the verification will not be complete, thus not entirely reliable. RTL simulation is also very time-consuming.
WHAT IS QUESTA® SLEC?
The Questa® SLEC application was developed by Mentor, a Siemens Business, to perform a fast and reliable SLEC, which is a useful feature in many testing scenarios. The Questa® SLEC app performs SLEC by finding corresponding blocks of RTL code and comparing them through deep formal analysis. This automatic, formal-based approach covers the entire state space and all scenarios including rare corner cases and takes only hours or minutes (depending on design size and complexity), outperforming even the best-designed simulation.
Benefits of the Questa® SLEC tool include speed, exhaustiveness, optional customization of the whole process (input, runtime, output reports), and a user-friendly interface that summarizes any found differences in a well-arranged manner. Also, no knowledge of formal or assertion languages is required and no testbench needed, which means that the tool setup is fast and convenient.
 |
Figure 1 - The Mentor Questa® SLEC flow
CODASIP DESIGN FLOW
At Codasip, we design new processor IPs in Codasip Studio, which is our own integrated set of EDA tools that covers the complete process of creating or customizing a core. Codasip Studio works with CodAL, our proprietary C-based language for processor architecture description.
The design process starts by the IP team describing the new processor in CodAL. From the CodAL representation, Studio can automatically produce all necessary outputs including a complete SDK, verification and testing environment, and any common HDL code such as VHDL, Verilog, and SystemVerilog, depending on customer’s needs and requests.
CODASIP VERIFICATION FLOW
The verification team must then ensure the logical equivalence of multiple HDL representations of the processor, in other words, the HDL output must be thoroughly verified to ensure that all the variants are functionally identical and correct.
Codasip’s verification methodology is based on a common approach: simulation and static formal analysis. We use standard full UVM verification to check that the resulting RTL corresponds to specification.
Our verification process takes two processor models, written in CodAL by two different engineers, as input: an instruction-accurate (IA) model and a cycle-accurate (CA) model. The IA model consists of a basic procedural description of the processor (what is to be done) and is used to generate an instruction set simulator, which then serves as a reference model for the functional verification – see Codasip's Verification Flow schema below. The CA model is essentially an IA model enhanced with a precise simulation of cycle-by-cycle timing (the "when") and is used to generate a cycle-accurate simulator and synthesizable RTL code, as shown below.
 |
Figure 2 - Codasip's verification flow
How Questa® SLEC Fits in The Codasip Verification Flow
The verification team at Codasip decided to employ the Questa® SLEC app in the process of ensuring that each HDL representation is the same, expecting that it will significantly reduce total verification time. The workflow is as follows:
One of the HDL outputs, for example the Verilog code, is thoroughly verified using UVM as before. All other HDLs, for example VHDL and SystemVerilog, are then verified using Questa® SLEC to compare the code against the already verified one (Verilog).
 |
Figure 3 - Codasip's Questa® SLEC flow
OPTIMIZATION OF THE QUESTA® SLEC FLOW
Although the formal analysis performed by Questa® SLEC is very fast, it can still take hours on more complex designs that contain many nested submodules. The more levels of module nesting, the more complicated the formal verification becomes, and the total time increases exponentially. As this complexity issue applies to Codasip’s processors, too, we had to come up with a suitable optimization of the whole process.
To avoid the exponential growth, the verification team wrote a script based on model decomposition to submodules. It instructs the Questa® SLEC tool to analyze each individual submodule separately, starting from those at the lowest level (the most deeply nested). Once a submodule is analyzed and compared to its counterpart in the other HDL code, it is “blackboxed” and the Questa® SLEC tool does not inspect it any further. Moving upwards through the model, higher-level modules are checked and marked as “blackbox”, which simplifies the whole process. Total runtime is thus reduced to a fraction of time needed without the optimization, going from hours to minutes.
RESULTS AND BENEFITS
The speed of the formal analysis performed by Questa® SLEC made it possible to accelerate verification of any additional HDL from tens of hours to tens of minutes. The following table shows the results for specific configurations of two Codasip’s RISC-V® cores from the Bk series, as shown below.
 |
Table 1 - Codasip's RISC-V® cores configuration results
In the case of three HDL outputs, whole days and considerable effort can be saved, bringing financial benefits as well as a competitive advantage.
To sum up, Questa® SLEC from Mentor provided Codasip with a fast and reliable verification method for alternative HDL outputs which our verification team further enhanced with their own runtime optimization, saving hours of effort and ensuring better positioning thanks to faster time-to-market. Our results may serve as an inspiration for using the Questa® SLEC app in innovative ways wherever an ability to perform automated, fast, and thorough formal comparison of code is needed.
Back to Top
