HDL linting improves the quality of spacecraft RTL to reduce design risk, accelerate IP verification, increase productivity, and reduce debugging effort to meet time-to-market deadlines.
If you have ever aspired to write out-of-this-world RTL, there's never been a better time as satellites, spacecraft, landers, and rovers are increasingly using FPGAs and ASICs in their sub-systems.
Some recent peer-reviews have highlighted poor coding techniques that have resulted in space-electronics failures, e.g. a $1M CubeSat becoming inoperable by getting trapped in a finite state machine's dead state. HDL linting, including structural static analysis, can check the quality of RTL before simulation, synthesis, and implementation, and has proven to be so effective in identifying bad practices for high-reliability applications that some satellite manufacturers now mandate their HDL programmers lint files before they are formally checked-in. The run time is significantly shorter than logic simulation and it can be performed early in the design cycle, where mistakes are less expensive, and while RTL is being developed, without requiring an exhaustive testbench.
Linting parses RTL identifying issues such as race conditions, register conflicts, bus contention, implied latches, redundant logic, X-propagation, long paths, and dead states. The analyses allows company-specific standards to be set up to enforce coding clarity and naming conventions.
Structural static analysis can find false paths directly from the RTL where no sequence of inputs results in an event propagating along the path and can thus be ignored for timing analysis and optimising performance. For example, the path from Register B to C shown below can never be sensitised because the output from the cloud of logic is de-selected at MUX2.
Figure 1 Example of single-cycle false path
Some false paths require multiple cycle across many levels of hierarchy to complete their function such as pulse generators or pipelined structures. For example, Select1 and Select2 shown below cannot be high at the same time resulting in a false path.
Figure 2 Example of multi-cycle false path
Structural static analysis can find the longest path critical to achieving timing closure and device fit: identifying false and multi-cycle paths directly from the RTL helps synthesis and implementation avoid unnecessary effort to meet timing or other optimisations on those nets. Needlessly placing and routing false paths can cause critical logic to miss closure!
Linting improves the quality of reliability (QoR) of RTL by identifying poor coding early in the development cycle when engineers are under less pressure to finish. It reduces design risk, accelerates IP verification, increases productivity, and reduces debugging effort and test time spent in the lab to meet time-to-market deadlines.
An example of linting and structural static analysis increasingly being adopted by the space industry to improve the quality of RTL and sign-off IP is Blue Pearl's Visual Verification Suite. By using this software, Orbital ATK working on a NASA project recently detected 24 clock-domain crossing (CDC) errors in production SpaceWire IP that were not picked up by traditional formal-verification methods.
The Visual Verification Suite parses RTL before simulation and synthesis checking for quality and reliability problems followed by CDC investigations. Code is analysed in a sequence where the first issues addressed are either those whose solution will also fix other faults or may cause or reveal other types of problems that can then be examined separately. The diagram below illustrates where HDL linting and structural static analysis fits within the standard FPGA/ASIC design flow.
Figure 3 Blue Pearl's HDL linting flow
Spacechips peer-reviews space electronics and RTL for many satellite and spacecraft manufacturers and we have started evaluating Blue Pearl's Visual Verification Suite to check the quality of third-party IP. Given that we do not always know the original design intent, HDL linting has proven to be useful in debugging and verifying the functionality of code. A very useful feature of the software is its ability to automatically detect and quickly validate the behaviour of finite state machines using bubble diagrams to display all states and transitions between them, as well as identifying unreachable ones. Previously, we would have written exhaustive test benches, which is time consuming.
The software also analyses CASE statements reporting duplicate, overlapping, or missing items, as well as absent assignments or the default clause. The linter can be extended, allowing custom checks to be created using Tcl or SDC (timing constraint) commands. During linting and structural static analysis, the tool can be controlled using its interactive GUI or run automatically in batch mode using Tcl.
As digital space electronics complexities increase, avionics engineers are increasingly using commercial or existing IPs to meet time-to-market deadlines. Typically, these come in various formats, (e.g. synthesizable RTL, encrypted IP, simulation models, or non-synthesizable HDL), often from disparate sources, and operate with independent clocks with different frequency and phase relationships, i.e. separate domains.
With multiple domains containing non-integer-related or drifting clocks, one has to verify the synchronicity of signals going between them. CDC occurs when data is transferred from a flip-flop driven by one clock to another triggered by a different clock. Setup and hold violations can result in metastability, which can propagate through a design as an erroneous state causing functional failure. Traditional simulation and static-timing analysis cannot model this behaviour and are unable to confirm if data is transferred consistently and dependably across domains.
If third-party IP is delivered as synthesizable RTL, then CDC analysis can be performed on these. However, for other formats, instantiated blocks have traditionally been imported as black boxes, containing sensitive, proprietary IP, and the analysis has been unable to use any knowledge of their internals nor information regarding the interaction of ports with clocks.
The Visual Verification Suite supports the concept of a grey cell that provides clocking and register information for third-party IP, allowing for accurate CDC analysis beyond what is possible using the traditional black-box methodology. A grey cell is a representation of a module that excludes all internal register-to-register logic, including only all logic from each input up to and including the first register, and all logic from each output back to and including the last register. Grey cells preserve the confidentiality of third-party IP as shown below.
Figure 4 Black-box IP vs. grey-cell IP
For users of space-grade FPGAs, Blue Pearl's Visual Verification Suite is supported by Microsemi's Libero SoC and Xilinx Vivado IDEs. To help the space industry manage increasingly complex designs instantiating IPs from many different sources, e.g. FPGA/ASIC providers, space agencies, OEMs and third-parties, I recommend that all providers of high-reliability FPGAs and ASICs include linting and structural static analysis within their design environments to allow HDL programmers to improve the quality of RTL.
HDL linting, including structural static analysis, improves the quality of spacecraft RTL and reduces risk earlier in the design cycle, allowing IP to be signed-off with confidence. I intend to continue the discussion by presenting a webinar sharing examples of poor coding and demonstrating how Blue Pearl's Visual Verification Suite improves QoR of RTL, accelerates IP verification, decreases development time, and increases productivity to help meet time-to-market deadlines.
Until next month, the first person to tell why IP ports should be registered will win a Courses for Rocket Scientists World Tour tshirt. Congratulations to Sophie from Boston, USA, the first to answer the riddle from my previous post. I will be presenting a tutorial on Space Electronics at Space Tech Expo in Pasadena on Wednesday 23rd of May and hope to meet many of my US readers in Los Angeles. I will also be presenting two papers on Tuesday 10th of April at ESA’s FPGA conference to be held at ESTEC.
Rajan Bedi is the CEO and founder of Spacechips, which provides on-board processing products, design consultancy in space electronics, training, technical-marketing and business-intelligence services.