-
FV Interview Questions (XIV) – What If SEC Cannot Achieve Full Proof?
It is not always possible to achieve full proof in the SEC, but there are still a few things we can try for better SEC convergence. We discussed a few techniques for FPV convergence, including design reduction, black boxing, and abstraction. They can all be applied to SEC as well. In addition, there are a…
-
FV Interview Questions (XIII) – What is SEC and How Does It Work?
In our book “Crack the Hardware Interview: Verification, Implementation, Synthesis and Power”, we discussed Formal Equivalence Verification (FEV). The goal of FEV is to check if two designs, Specification Model (SPEC design) and Implementation Model (IMP design), are equivalent. There are 2 major applications of FEV in ASIC / digital design flow: Logical Equivalence Check…
-
Jim Keller’s View Towards “HW / SW Contract” in AI Chips
In DAC61, Jim presented his view towards “HW / SW Contract” in AI chips. It is definitely worth watching his keynote in DAC61. In the CPU world, the ISA + programming & execution model is obviously the contract between HW and SW engineers. However, unlike CPUs, the contract is not quite clearly defined in AI…
-
FV Interview Questions (XII) – How to Define Clocks for Designs using Both Posedge & Negedge?
If the design is using only posedge of a single clock, then the clock can be defined as: # assume clk is the clock input signal name at top level If the design is using only negedge of a clock, then the clock can be defined as: It is not uncommon for a design using…
-
FV Interview Questions (XI) – Does a Liveness Property Failure Mean a Deadlock?
Liveness property debug may often be tricky. If we ever find a liveness property failure, it does not necessarily mean a deadlock exists in the design. Instead, it could be due to lack of proper assumptions. Assuming we have a data processing block, in which both input and output data interfaces follow Valid-Ready protocols. We…
-
FV Interview Questions (X) – How does Liveness Property Impact DV & How to Work Around it?
In the last post, we mentioned that liveness properties may not be useful in simulation. Some simulation tools do not always report liveness property failure in DV tests. In addition, liveness properties may even significantly degrade simulation speed. Simulation tools use checker threads for SVA properties. Due to its nature of “infinity”, liveness properties have…
-
FV Interview Questions (IX) – How to Write Efficient Liveness Properties?
Should You Use Liveness Properties in the First Place? Liveness properties are often more complex to prove, and challenging to debug. Plus, they may not be useful in simulations (covered in the next post). Before writing liveness properties, designers should ask themselves, is it really necessary to use liveness properties in the first place? In…
-
Chipress’ Social Profile is Up!
As an effort to enhance our online presence, we set up our social profile in various social media platforms. Follow us on LinkedIn, X, Instagram, Threads, and Facebook, to get instant updates from us. For everyone’s convenience, we aggregated all our social profile in LinkTree, a powerful link in bio tool. You are also welcome…
-
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…
Chipress 