difference between formal and functional verification

  • Thread starter parag_paul@hotmail.com
  • Start date
P

parag_paul@hotmail.com

Guest
Sorry for a dumbo.
But I am a s/w guy since I am working on the compiler basics of a
simulator, I keep hearing about the functional and formal
verification . What is the difference between the two.
Can somebody please explain to me ?


Also . what are cycle based semantics. What can be other semantics
that are used by the verification tools?
 
On Mar 6, 2:49 pm, "parag_p...@hotmail.com" <parag_p...@hotmail.com>
wrote:
Sorry for a dumbo.
But I am a s/w guy since I am working on the compiler basics of a
simulator, I keep hearing about the functional and formal
verification . What is the difference between the two.
Can somebody please explain to me ?

Also . what are cycle based semantics. What can be other semantics
that are used by the verification tools?
Click to expand...

Functional (dynamic) verification requires user-defined stimulus to
check design properties. Since user-defined stimulus may not check the
property competely, there is remaining risk that property fails for
the some other valid, but not executed stimulus. In few words, dynamic
verification starts from stimulus, trying to prove design properties.
Formal model checking takes the opposite direction. It starts from
formalized design properties, looking for valid stimulus which "fail"
these properties. These stimulus are called "counter examples", and
usually formal tool stops upon finding the first one which fail the
property. In a case formal engine cannot find counter example for the
property, the property is declared as "passed" and there is a
guarantee that it is implemented prorerly for all possible sets of
valid stimulus.
Formal tools suffer from "state explosion" problem, working on designs
with limited amount of state variables. They are very useful for block-
level verification, especially for verification of control logic such
as arbiters, buffer control logic, control state machines etc.

Regards,
-Alex
 
As mentioned in the previous post the functional verification requires set
of test vectors.
The test vectors are usually written directly in HDL or other verification
languages.
Verification engineers do not write simple binary sequences. Testbenches
usually
contains procedures or other high level constructs, which finally produce
the binary sequences
applied to the tested unit. You must write all legal test vectors to cover
entire
design functionality. Otherwise the design is not fully tested. It is not
trivial task and usually
designs are not 100% covered. Constrained random verification is recently
popular.
It allows to achieve higher coverage because stimulus can be pseudo-randomly
generated.
You can find more about constrained random verification on:
http://www.pulselogic.com.pl/en/index.html (See New Technologies section)

Formal verification is a different approach. You do not write any test
vectors here.
Formal verification is divided into two areas:

- Equivalence checking - this solution allows to compare two implementation
of a design and detect differences. For example, you have design written in
VHDL
and Verilog and you can perform equivalence checking to verify if the two
implementations
are the same. You can also compare netlist with RTL description etc.

- Assertions checking - You can write assertions in HDL code. Formal
verification tools detects automatically assertions (properties), which fail
during design operations. You are not running simulation. Format
verification tool checks all possible states and transitions in the design
and detects conditions causing assertions to fail.
Unroftuanlly, you must define here the possible states for design inputs and
it is not a trivial task.
You can find a little bit more information under the above link in Assertion
Based Verification section.

Best Regards,
Slawek





<parag_paul@hotmail.com> wrote in message
news:1173210567.420760.138910@t69g2000cwt.googlegroups.com...
Sorry for a dumbo.
But I am a s/w guy since I am working on the compiler basics of a
simulator, I keep hearing about the functional and formal
verification . What is the difference between the two.
Can somebody please explain to me ?


Also . what are cycle based semantics. What can be other semantics
that are used by the verification tools?
Click to expand...
 
"Slawek" <news@pulselogic.com.pl> writes:

Formal verification is divided into two areas:

- Equivalence checking - this solution allows to compare two implementation
....
- Assertions checking - You can write assertions in HDL code. Formal
Click to expand...
Formal verification precede assertions based methodologies. There are
tools which can check that a design behave according to a formal
specification. ACL2 is such a tool and have been used by e.g. AMD and
Motorola to prove that a given design is correct. You can find more
information about ACL2 at URL:

http://www.cs.utexas.edu/users/moore/acl2/

Petter

--
A: Because it messes up the order in which people normally read text.
Q: Why is top-posting such a bad thing?
A: Top-posting.
Q: What is the most annoying thing on usenet and in e-mail?
 
On Mar 8, 12:10 am, Petter Gustad <newsmailco...@gustad.com> wrote:
"Slawek" <n...@pulselogic.com.pl> writes:
Formal verification is divided into two areas:

- Equivalence checking - this solution allows to compare two implementation
...
- Assertions checking - You can write assertions in HDL code. Formal

Formal verification precede assertions based methodologies. There are
tools which can check that a design behave according to a formal
specification. ACL2 is such a tool and have been used by e.g. AMD and
Motorola to prove that a given design is correct. You can find more
information about ACL2 at URL:

http://www.cs.utexas.edu/users/moore/acl2/

Petter

--
A: Because it messes up the order in which people normally read text.
Q: Why is top-posting such a bad thing?
A: Top-posting.
Q: What is the most annoying thing on usenet and in e-mail?
Click to expand...
Thanks to all of you for the response. I am now clear about it. Also
that I had a second question, about cycle besed semantics


And , is the Synopsys Tool Tetramax supposed to generate patterns for
the same functional verification or formal verification. And what
are patterns as they mean
 
Thanks to all of you for the response. I am now clear about it. Also
that I had a second question, about cycle besed semantics


And , is the Synopsys Tool Tetramax supposed to generate patterns for
the same functional verification or formal verification. And what
are patterns as they mean
Click to expand...

I am not sure what cycle base semantics mean but it must be connected with
cycle based simulation.
Cycle based simulator synchronizes its operations to clocks detected in a
design. It evaluates
the design only while the active edge of a clock occurs. It does not perform
any actions between clock edges.
Even if a signal should change its value between active clock edges the
simulator changes its value at the preceding
or following clock edge. Such simulator has limited accuracy but works much
faster than traditional event based
simulators with full accuracy.

Teramax is a different tool. In my opinion it is neither functional nor
formal verification tool.
Tetramax is an ATPG (Auto Test Pattern Generation) tool. It generates tests
to check an ASIC chip after manufacturing.
Such test simply exercise the circuit to verify if the manufacturing process
went well. I am not an ASIC engineer but
Tertamax uses probably scan chain to apply the test vectors. ASIC chip has
dedicated operation mode where all registers
all connected in a chain and its states can be set or read back using simple
synchronous serial interface. Tetramax uses such
interface to exercise the circuit.


If you want a formal verification tool. You should focus your attention on
Synopsys Formality, Synopsys Magellan
or similar tools from other vendors.

Best Regards,
Slawek
 
On Mar 8, 6:08 am, "parag_p...@hotmail.com" <parag_p...@hotmail.com>
wrote:
On Mar 8, 12:10 am, Petter Gustad <newsmailco...@gustad.com> wrote:



"Slawek" <n...@pulselogic.com.pl> writes:
Formal verification is divided into two areas:

- Equivalence checking - this solution allows to compare two implementation
...
- Assertions checking - You can write assertions in HDL code. Formal

Formal verification precede assertions based methodologies. There are
tools which can check that a design behave according to a formal
specification. ACL2 is such a tool and have been used by e.g. AMD and
Motorola to prove that a given design is correct. You can find more
information about ACL2 at URL:

http://www.cs.utexas.edu/users/moore/acl2/

Petter

--
A: Because it messes up the order in which people normally read text.
Q: Why is top-posting such a bad thing?
A: Top-posting.
Q: What is the most annoying thing on usenet and in e-mail?

Thanks to all of you for the response. I am now clear about it. Also
that I had a second question, about cycle besed semantics

And , is the Synopsys Tool Tetramax supposed to generate patterns for
the same functional verification or formal verification. And what
are patterns as they mean
Click to expand...
Its better if you really browsed through a book on ASIC design flow.

rgds,
neo
 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top