-
FV Interview Questions (VIII) – What is a Liveness Property?
Designers are typically more familiar with safety properties, whose intention is to check a “bad thing” can never happen. For example, in the following safety property, when valid is asserted while ready is low, valid should keep asserted in the very next cycle. If valid is deasserted in the next cycle without ready being high…
-
FV Interview Questions (VII) – What is Precondition Reachability Check?
Assert and assume properties often use a triggering event, or a precondition, to define when the test expression should be checked. If the precondition is unreachable, then the assert property will never trigger, and it does not check what was intended. Consequently, the tool can never find a violation trace regardless of the logic driving…
-
FV Interview Questions (VI) – Dealing with Complexity by Abstraction
From Black Box to Behavioral Model, to VIP We discussed black boxing, but black boxing assumes a logic X at the output ports. One can further add assume properties at black box module outputs, to constrain their behavior. Designers can wrap these assume properties into a separate module, and this module has the exact same…
-
FV Interview Questions (V) – Dealing with Complexity by Black Boxing
Other than design reduction, black boxing is another effective approach to deal with FV complexity. Black boxing can be done in design analyzing phase: Or it can be done in design elaboration phase: By default, the outputs of a black-boxed module always produce a logic X, i.e., the tool ensures a “pessimistic” verification by allowing…
-
FV Interview Questions (IV) – Dealing with Complexity by Design Reduction
In our book “Crack the Hardware Interview: Verification, Implementation, Synthesis & Power”, we briefly discussed what to do if FV cannot achieve full proof. Design reduction is an important technique to tackle this problem. We will dive a little deeper in post. Many designs have parameters for structures that we can reduce, for example, FIFO…
-
FV Interview Questions (III) – How to Waive an Expected Failing Property?
Typically we want to get full proof for all assert properties and see all cover properties proven reachable. However, sometimes we may want to disable certain properties from being run during FV. For example, the FV VIP supports all features of a protocol, but the design itself only supports a subset. In Jasper Gold, one…
-
FV Interview Questions (II) – How to Do FSM Checks?
Jasper Gold offers “fsm_checks” command to auto-generate properties for FSM state / transition reachability. When running this command, the tool automatically detects FSM state variables or accepts user-specified FSM state variables, and extracts cover properties to prove. To define a conceptual FSM from the the concatenation of “signal0” and “signal1“: To generate properties for state…
-
FV Interview Questions (I) – How to Debug Unreachable Properties?
During formal verification, sometimes we may see unreachable properties. Using Cadence Jasper Gold for example, it can be flagged as either unreachable cover properties, or passing yet never triggered assert properties. This can be caused by over constraints, i.e., excessive assume properties, or design bugs. In order to isolate the root cause, RTL designers can…
-
Why Should We Never Use Self-Determined Expressions in RTL?
A self-determined expression is the one whose bit length is solely determined by the expression itself. SystemVerilog LRM defines the bit lengths resulting from self-determined expressions. In the table below, i, j, and k represent expressions of an operand, while L(i) represents the operand i’s bit width. Designers should avoid using self-determined expressions in RTL,…
-
Hash Function and Its Applications: Hash CAM & Bloom Filter
A hash function defines the mapping relationship of (key, value) pairs. Good hash functions should be very fast to compute (easy for hardware implementation), and should minimize duplication of output values (less collisions). How to Implement a Hash Function? One common approach to implement a hash function, is to use modulo operations: value = mod(key,…
Chipress 