optronic said:Hi,
with Formality you make an equvalence check: Netlist against RTL, based on
formal methods, no assertion here.
The other think is called Static or Dynamic Formal Verification, and here
you need to define assertions (based on properties) that these tools try to formally
proove for the RTL design. Tools are Magellan (synopsys) or 0-in (mentor)
for example.
Assertions are also used in ABV in tools like QuestaSim (mentor)
or VCS (synopsys).
Thanks again, aji_vlsi!aji_vlsi said:Folks,
Under Formal Verification there are few techniques:
1. Equivalence Checking (EC) - tools like LEC, Formality
2. Model Checking (MC) - Magellan, IFV,
3. Hybrid Formal - Magellan, 0-in
4. Theorem Proving - more at research level.
Out of these, MC and Hybrid use SVA/PSL as specification. We showed this with examples in our PSL & SVA books (www.systemverilog.us). I also cover these topics in great detail in our CFV course, see: www.noveldv.com for details.
boardlanguage said:Thanks again, aji_vlsi!aji_vlsi said:Folks,
Under Formal Verification there are few techniques:
1. Equivalence Checking (EC) - tools like LEC, Formality
2. Model Checking (MC) - Magellan, IFV,
3. Hybrid Formal - Magellan, 0-in
4. Theorem Proving - more at research level.
Out of these, MC and Hybrid use SVA/PSL as specification. We showed this with examples in our PSL & SVA books (www.systemverilog.us). I also cover these topics in great detail in our CFV course, see: www.noveldv.com for details.
Are these listed in order of popularity/application-use? (I assume equivalence-checking is the most popular use for Formal Verification.)