- Details
- Published: Tuesday, 17 September 2019 19:43
- Hits: 2802
JASPER Gold: JASPER Design Automation bought by Cadence in 2014, and tool now called Jasper Gold (JG):
JG gives more ROI compared to sims, as bugs are caught early and require only 50% manpower.
Jasper provides a wide range of Applications (Apps) covering: Formal Property Verification, Sequential Equivalence Checking, Low-Power Verification, Connectivity Verification, Config/Status Register Verification, X-Propagation Analysis, Structural Property Synthesis, and Behavioral Property Synthesis (just to name a few). Lint and CDC (synchronizers and data coherency issues) too.
formal property verification (FPV):
-----------------------
it checks if RTL meets certain properties specified. It uses design only, no tb as illegal states specified in assertions are checked for. It helps catch bugs early.
In any line of RTL code, we can right click, and select Activate->visualize line and that will bring up waveform, showing how that RTL target is reached w/o the need for tb.
proofgrid => properties are being proven by running engines.
Sequential Equivalence Checking (SEC):
----------------
Formally prove RTL vs RTL. This is for ECO where we want to formally prove that only intended changes are there.
Low-Power Verification:
----------
automatically creates power aware RTL (UPF/CPF), creates set of checks and evaluates them for all possible i/p combos/ does power aware structural, func and Seq checks
Reduce transitions on clk/mem, does pwr opt, minimizes retention flops
Config/Status Register Verification (CSR):
-------------------
given a reg spec and RTL, automatically derives all properties and runs formal to prove them. IP_XACT i/p as in reg modelling of UVM.
any discrepancy b/w RTL and spec are highlighted with counter examples
X-Propagation Analysis:
--------------
Detect X. verify design init and reset behaviour. Flop reset minimization flow. It can replace GLS.
AFL (automatic Formal Linting):
------------------------------
This consists of
1. Basic Lint checks (HAL = HDL Analysis and Linting) - Naming, coding style, structural, DFT, sim-synth mismatch, etc.
- Naming and File format checks = RTL_NAMING, RTL_FILEFORMAT
- Coding style checks - semantics, portability of code = RTL_CODINGSTYLE
- synthesizability/sim-synth mismatch checks - identifies unsynthesizable constructs, pre-synth/post-synth mismatch = RTL_SYNTH, RTL_SIMSYNTH
- Structural checks - pesudo synthesize RTL to get structural view, look for feedthru, combinatorial paths = STRUCTURAL
- FSM checks - compliance to FSM modeling style = FSM
- Race condition checks - detect all sim race statically possible - read-write, write-write etc = RTL_SIMRACE
- DFT checks - both in func and test mode that make nodes Uncontrollable and Unobservable = DFT. ADVANCE_DFT
2. Advanced Lint checks - (also known as SPS) Structural Property synthesis (SPS):
- automatic checks from RTL such as arithmetic/range overflow, dead code, FSM livelock/deadlock, pragma, bus contention etc. No TB required. These checks do require specifying clock and reset.
- X assignment = checks whether X assignment are reachable
- Arithmetic overflow = whetheroverflow can occur in case of arithmetic op
- Bus contention = whether multiple drivers can drive conflicting values on bus
- Range overflow = for array access
- FSM Livelock/deadlock = when design gets stuck in a state.
- Case = whether certain synthesis pragmas are honored
- code coverage reachability:
- Block = If all branches in RTL are reachable
- FSM = If all branches of FSM are reachable
- Toggle = If all signals can be toggled
- automated and manual property ranking and classification
- these properties can be fed back into formal or sim env
Behavioral Property synthesis (BPS):
---------------
while SPS is automatically extracted from RTL, BPS is extracted from sim traces (which can be in VCD, FSDB or SHM format), so quality of properties tied to quality and maturity of sims. It's suggested to run periodically thru out the project.
- synthesis of multi cycle, hand shake, implication, black box and white box properties from sim (flow is there w/o sim also).
- multi cycle = more than 1 or 2 cycle that may never fire in sims
- automatic properties (assert, assume, cover) as FIFO, counters, FSMs, 1-hot.
= assert: onehot = $onehot0 ({c0.hit,c1.hit,c2.hit}) => implies one hot
= assert: FIFO = (q.head == q.tail) |-> q.empty => implies empty state if head eq tail
= cover: FIFO = !$stable(fifo.rd_ptr) && !$stable(fifo.wr_ptr) => implies tests never change both fifo ptr together
- user defined properties by specifying interacting signals
- automated and manual property ranking and classification
- properties are classified, and coverage holes are identified via sim. TB is refined and sim rerun to inc func cov. formal cov is also enhanced by analyzing these properties.
- these properties can be fed back into formal or sim env
Formal coverage:
--------
Coverage is of 3 types:
- Code coverage => checked via imc
- Func coverage: via cover properties written in TB as SVA/PSL
- Formal coverage: proof coverage, bound coverage, stimuli coverage
Is my property set complete?
Unreachability:
---------
analyze sim coverage. determine formally unreachable code. No formal expertise reqd, as it just proves reachability/unreachabilty of coverage holes
-------------------------------------
running JG for AFL checks: run irun as usual, just add -jg option.
-------
irun ¡Vjg ¡Vafl ¡Vgui -64 ¡Vjgargs ¡¥-use_license_option¡¦ ¡Vinput <setup>.tcl => this invokes JG with AFL
inputs:
1. custom rule file - selected checks
2. design info file - blackbox, lint pragma
3. custom tcl file - clock, reset, selected checks => This does advanced lint checks
- syntax: clock <clk_signal> reset <rst_signal>
on the gui, under AFL section on top, we see buttons for these:
1. configure Auto Formal checks
2. extract Auto Formal checks
3. export properties to a task
4. prove exported Auto Formal coverage and checks
5. generate reports: from the extra pull down button at end, click "generate_report -> auto or violation checks". This generates concise report for all viols in html format.
On the bottom of gui, we have violation viewer, waiver list, Auto Formal properties, ..
To create waiver, click on any violation, right click waiver and add waiver for that viol.
--------------------