Bus contention and floating busses are well defined issues and therefore excellent candidates for being addressed with early-stage formal verification.
Bus issues are a familiar but persistent source of bugs. There are two main types:
- Bus contention arises when more than one device is trying to place a value on a bus at once.
- Floating bus problems occur when a bus is driven by an input signal, but is not connected to an output.
While we have faced these problems for some time, we still have no off-the-shelf or convenient way of fixing them. It is best to stop them happening entirely or at least catch them early in the design flow.
Bus standards – most of them proprietary – do have arbitration schemes that seek to resolve these issues. However, logic errors in the implementation of such schemes can still leave a design open to bus contention.
More recently, the growing use of on-chip busses in SoCs has further complicated the verification and resolution of contention and floating bus problems.
Verify for bus contention and floating busses before simulation
Any potential source of bugs that can be anticipated and whose error types have been well characterized is a candidate for early RTL verification, even at the SoC level.
Productivity demands that this is undertaken before simulation. If you debug bus contention within simulation, you will see unknown X states in the analysis result. The largely manual review of simulation VCD traces to find Xs is tedious and time-consuming. Moreover, this kind of analysis can become confused with that required to identify other X-sources in a design (i.e., X-pessimism).
The fact that a floating bus and/or bus contention can lead to a physical device failure (typically due to overheating or fusing) makes tools that can identify and repair these errors early in the verification process attractive.
Bus failures are part of the functional verification process – a design is explicitly failing to match the original intent. Within that category, intelligent formal verification can help design teams confront and fix bus problems quickly.
Real Intent’s Ascent IIV Autoformal is a good example of the kind of early-stage verification software that addresses bus issues.
Applied before simulation and with no need for a testbench, it carries out a hierarchical analysis of the RTL, automatically generates a set of appropriate functional assertions, runs these and then reports back on areas for concern.
In addition to bus issues, the Ascent IIV Autoformal package also runs checks for:
- FSM deadlocks and unreachable states
- Full- and parallel-case pragma violations
- X-value propagation
- Array bounds
- Constant RTL expressions, nets and state vector bits
- Dead code
- SystemVerilog ‘unique’, ‘unique0’, and ‘priority’ checks for ‘if’ and ‘case’ constructs
By addressing these issues hierarchically, and drawing on accumulated knowledge of bug causes, Ascent IIV Autoformal finds deeply embedded bugs. These can be missed in simulation, but may start daisy chains that lead to alerts further down the design flow which will then be more complex and expensive to find and fix.
Ascent IIV Autoformal also uses a smart reporting feature that allows the user to track a bug back to its source.
In the cases of bus contention and floating busses, early and in-depth verification that concentrates on the original design team’s intent has obvious advantages.
Divide and conquer endless verification
Verification now accounts for more than 50% of the SoC design cycle, due to increasing gate counts, functionality and manufacturing challenges. This growing complexity means that some projects may face ‘endless verification’ issues, in which the variety of bugs and their interdependencies are so great that the design cannot be signed off in time to meet its market window.
Although the industry continues to improve traditional approaches, there is a pressing need for divide-and-conquer techniques that take over the verification of entire bug classes, reducing the scope of the design that has to be addressed using simulation.
Well-informed hierarchical and formal verification strategies that can be deployed before simulation are therefore playing a vital role in maintaining and increasing productivity.