-
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,…
-
Best Practice for Defining Configuration Registers
In the ASIC design industry, there are certain configuration register definition guidelines that RTL designers should follow. This is to achieve the following purposes: Guidelines for Configuration Register Content Guidelines for Configuration Register Address Map
-
Best Practice for RTL Naming Conventions
In this post, we share a few RTL naming conventions for better readability. See the table below. RTL Naming Convention RTL Naming Convention Use intelligible signal / variable names Better readability is achieved if the RTL code is “self-documented” Use “<name>_clk” for the name of a module’s clock input Use “_n” suffix for asserted low…
Chipress 