Formal Verification beginner seeking suggestions.

[JianR]

Hello.

I'm in a study phase of a thesis covering development of a formal verification IP, whereas I only have experience within Simulation based verification since before. I have read a book by Foster/Krolnik/Lacey on "Assertion based design", which covers Formal verification but more on a theoretical level.

I somewhat understand the principle of extracting a FSM from a synthesizable RTL, for which properties (DUT intentions) and their respective assertions (actions for violation of said intentions) through Model Checking (Kripke, fixed-point equations) ... but this is all so theoretical for me. I haven't seen a book yet which gives a more practical example of formal verification (like code segments); I'm not sure how formal verification in practice is performed in industry.


So my questions I was hoping someone with experience could help me with:

• How do you learn formal verification?
• Is it tool dependent, depending if you use IFV, Formality, Conformal etc?
• Do they all share the same "language"; if you know Conformal, would you be able to use IFV right away?

Any answer shredding some clarity over my thoughts are greatly appreciated!

/JianR

 

[raghavathej]

Hi there,

1. Learn formal verification say Equivalence Checking starting from small HDL programs. Always prefer to work on one tool at a time. (Quality, not Quantity matters).
Per se, Start over with Cadence Conformal.

2. Equivalence Checking verifies the equivalence between two views say - RTL vs Netlist , RTL1 vs RTL2 , Netlist1 vs Netlist2. It is tool independent until you are using same RTL Code, Technology Library and Any 1 synthesis tool for all Formal Tools.

3. There is nothing like language, the commands will vary between different Vendors/Tools. If you know how to show equivalence, in say Conformal, definitely, same thought process can be used in solving it in other Tool.

Is this info sufficient ?. Let me know if you want to know more.

 

[JianR]

Thank you for your reply raghavathej! It did indeed help me get some clarifications over the subject!