Insight Products

Insight :Simulation-Centric Formal Analysis

First behavioral-level formal analysis tool for verilog and SystemVerilog

Improve quality and streamline functional verification and DFT flows

Microarchitecture-level assertion and coverage property synthesis
- Automatically enhance verification and coverage property synthesis
- Augument user written assertions and coverage to fill holes
- Improve verification closure

At-Speed DFT Analysis and Repair
- Analyze RTL blocks for DFT rule checks
- Uncover issues preventing robust at-speed testing
- Automatically repair RTL with minimal test logic overhead
- Generate path delay fault test coverage and list of untestables
- Improve DFT closure

X-Verification
- Analyze designs for non-deterministic operation due to X sources
- Effectively debug X pessimism issues in gate-level simulations
- Mitigate X issues faster and make designs more robust

Simulation-centric formal analysis engine
- Easier to use than traditional formal tools
- Uses testbench or VCD for stimulus
- Integrated logic and symbolic simulator

 

Insight - At-Speed DFT Analysis and Repair

Analyze design for at-speed Path Delay Fault(PDF) testability
- Perform DFT design rule checks
- Generate coverage report for sample paths
- Perform robustness checks to diagnose low coverage
- Diagnose untestable paths

Automatically repair design RTL for improved testability
- User specifies test logic overhead limit

Benefits
- RTL repairs result in better test coverage for Small Delay Defect
Transition Dealy Fault(SDD-TDF) and PDF
- Better 1st pass ATPG coverage results
- Eliminate time consuming RTL/Gate-Level design iterations to improve
low test coverage.

 

 

	Use cover property to genearate interesting scenarios
Use assert property to catch unintended behavior S0 -> S3 is illegal

 

Insight - Reachability analysis

Find and diagnose unreachable code blocks due to RTL bugs, dead code,
and testbench limitations .

Use in early stage of design - Uncovered early design bugs without a testbench - Identify hard-to-verify code and properties. - Generate realistic code coverage goals for logic simulation Performs assertion and coverage property synthesis for later chip simulations including FM deadlock, FIFO overflow/underflow, register collisions, bus checks, size and index assignment, parallel case uniqueness
Use with testbench - Identify testbench limitations affecting quality - Cone analysis under permissible input stimulus
Supports root cause analysis to diagnose unreachables Merge/Diff with simulation code coverage to find holes Constructs Analyzed - Conditional branch blocks . - Prpoerties(assert and cover) - FSM transitions

Identify potential FSM deadlock conditions Performs guided symbolic path enumeration of FSM states for deep sequential analysis

 

 

Insight - X-state verification

	Reset sequence Verification - Current design methodologies tend not to reset all registers - X's in uninitialized registers create nondeterminism that cannot be accurately simulsted because of X-pessimism and X-optimism issues. - Find all registers that are 0/1 in logic simulation but can actually be X
		Scalable solution use design and time partitioning

	Time partioning creates interval checkpoints
Assume register e and g are uninitialized. In logic simulation, g will always be 0 because of X-optimism. Realistically g can be 0 or 1.

Low Power Verification

- Verify no X's propagate from powered down blocks to powered blocks
- Verify retention and isolation assertions
- Run symbolic simulation through the valid power state transition
- Provides counterexamples to debug each X condition
- Identify repair solutions for missing use of retention registers, power-on reset,
or isolation cells.
- UPF and CPF support planned