what is formal verification

[zhangpengyu]

Hi
guys!

What is formal verification? What does it use to do?Generally,what tools can use? Is it necessary to write testbenches in formal verification?Is formal verification don't want to simulation?
Thanks!


zhpy

 

[AlexWan]

What is formal verification? What does it use to do?Generally,what tools can use? Is it necessary to write testbenches in formal verification?Is formal verification don't want to simulation?

pls refer
<<Verilog® HDL: A Guide to Digital Design and Synthesis, Second Edition>> By Samir Palnitkar

15.3 Formal Verification
A well-known white-box approach is formal verification, in which mathematical techniques are used to prove an assertion or a property of the design. The property to be proven may be related to the chip's overall functional specification, or it may represent internal design behavior. Detailed knowledge of the behavior of design structures is often required to specify useful properties that are worth proving. Thus, one can prove the correctness of a design without doing simulations. Another application of formal verification is to prove that the architectural specifications of a design are sound before starting with the RTL implementation.

.....

 

[wadaye]

Hi :

Formal verification proves mathematically that two designs have the

same functionality. Your design could be rtl/gates/layout, and you don't

need ant vectors. You can use formal tool to confirm you function if you

changed your netlist. But you still need simulate the RTL to verify the

function first, and use this as golden to do formal.

Cadence have a formal tool named Conf0rmal LEC/LTX, syn0psys

have a tool named f0rmality, and ment0r have a tool named f0rmal pro.

wang1

 

[bluegge]

snps 's tool Formality suport it...

 

[seasonyangd]

I thin LEC is used more often.

 

[tom123]

1) formal verification is using mathematical principle to

verify the equivalence between RTL and gate level netlist.

(RTL and RTL, gate level netlist and gate level netlist).

2) we can use verplex, as well as tools from synopsys.

3) only need writing scripts in formal verifications.

4) formal verification can in stead of post-sim.

Hi
guys!

What is formal verification? What does it use to do?Generally,what tools can use? Is it necessary to write testbenches in formal verification?Is formal verification don't want to simulation?
Thanks!


zhpy

 

[Mohamed.Madbouly]

Formal verification should be done in different levels.

(1) System Level --> It depends on how the Designers write there system level design, you can use MATLAB code if they use MATLAB. You can use SystemC if the designers uses SystemC better uses VERA as this supported from synopsys to integrate SystemC with VERA.

(2) RTL level --> better to use VERA or Specman.

(3) Physical design --> Most of people uses formality tool of synopsys.

For case 1 and 2, you need to generate test vectors and test benches.

 

[srik_naidu]

hi,
formally verification needs to verify the written properties(specifications).
using psl/sugar,vera we can write properties.

with regards,
srik.

 

[Arnold]

Both model/property checking and equivalence checking are formal verification technologies.

As I know, both lec and formality is equivalence checking tool. Which tools are used for model/property checking? Thanks

 

[justin999]

formality

Added after 37 seconds:

it is a tool of synopsys

 

[silencer3]

conformal LEC is alos a good tool.

 

[amaccormack]

There are two types of formal analysis done on digital designs:

1. Equivalence checking

This is used to compare two representations of a design, typically RTL vs schematic, but also RTL vs RTL and schematic vs schematic to do a "diff". The main tools in the area are Synopsys Formality and Verplex LEC, now part of Cadence.

2. Model checking

This is where a set of properties, specified in a language like PSL or SVA, are formally analyzed to see if they are always true for a design. This can exhaustively prove if a property is correct, but does tend to suffer from state-space explosion: the time to analyse a design is dependednt on the amoutn of state, exponentially, so a design with 101 flip-flops takes twice as long to analyze as one with 100.

Many tools can automatically infer properties to check from your RTL: for example, impossible to reach states in an FSM, full_case/parallel_case correctness, etc.

Some tools, such a 0-in (now owned by Mentor) use simulation runs to reduce the state space required to search, speeding up analysis.

Other tools in the area are the free SMV: **broken link removed**

Cadence Staticcheck and Verplex Blacktie are being merged, I believe
Synopsys Ketchum
Real Intent
Veritable
Axiom (formerly @HDL)
Averant
IBM Rulebase

google for the above, or look at John Cooley's deepchip.com website where there have been a few user experiences listed.

 

[zhaoyimiao]

formal verification may induce "false path" so maybe not 100% safe.

 

[spauls]

Formal verification cant find your functional bug.

 

[sivashankar]

No test vector needed for formal verification .So verification time is less

 

[yuenkit]

formality do formal verification check.

Synopsys has 2 static verification software:
1. PrimeTime - for Static Timing Check
2. Formality - for Static Function Check

Formality only check for function equivalant to the original design. So it is fast.

 

[tigerajs]

Hi
guys!

What is formal verification? What does it use to do?Generally,what tools can use? Is it necessary to write testbenches in formal verification?Is formal verification don't want to simulation?
Thanks!


zhpy

you can use formality, it is better to do simulation again

 

[vizpal]

What about Formal Verification in the Front Front end side...???

 

[shavakmm]

there is a series of article on formal verification in below website. Pleae visit:

https://asic-soc.blogspot.com/2007/10/introduction-to-formal-verification.html

rgds
murali