Mathematical approch to verify a FSM

Academy Home

Academy Login

The Verification Academy requires Javascript. Please enable Javascript in your browser or switch to a browser that supports Javascript in order to view this site.

Mathematical approch to verify a FSM

2 posts / 0 new

Last post

February 9, 2012 - 5:40am

Nag

Offline

Academy Total Access User

Joined: 09/12/2011

Posts: 5

Mathematical approch to verify a FSM

Is there any mathematical approch to verify a 3 level FSM. Suggest any mathematical approch if you have worked on it to verify a FSM.

February 26, 2012 - 3:08am

Ajeetha Kumari CVC

Offline

Academy Forum User

Joined: 09/19/2011

Posts: 63

Re: Mathematical approch to verify a FSM

Write a bunch of assertions describing the "characteristics" of the FSM in say PSL/SVA and then provide RTL + properties to a formal verifier (model checker - MC). MC is the "mathematical engine" that you are looking for. Severak commerical MCs exist:

1 0-in from Mentor
2. IFV: from Cadence
3. Magellan from SNPS
4. Jaspergold from Jasper
5. Panda from SparkEDA

HTH
Ajeetha, CVC
www.cvcblr.com/blog

__________________

Ajeetha Kumari, CVC Pvt Ltd.
http://www.cvcblr.com
* A Pragmatic Approach to VMM Adoption http://www.systemverilog.us/
* SystemVerilog Assertions Handbook
* Using PSL/Sugar