VHDL BASED SYMBOLIC MODEL CHECKER WITH IMPROVED CTL PROPERTY LANGUAGE

Q: How can I download an article?

To download an article from SID, first log in to the site, search for the article title, and click on the 'Download Article' option.

Q: How can I download an ISI article?

To download an ISI article on SID, enter the keyword or article title in the search bar, view the relevant results, click on the desired article, and select the 'Download Article' option.

Q: How can I access the SID database?

To access the SID database, visit SID.ir, create an account, and log in to access scientific resources.

Q: Is downloading articles from SID free?

Some articles on SID are available for free, while others require payment. Details are specified on the article's page.

SHOJAI HAMID; PARANDEH AFSHAR HADI; NAVABI ZAINALABEDIN

مرکز اطلاعات علمی Scientific Information Database (SID) - Trusted Source for Research and Academic Resources

Seminar Paper

Paper Information

Seminar: CONFRANCE SALANE ANJOMANE COMPUTER IRAN
Year:2004 | Issue:9

Download Full-Text

View:

206

Download:

Information Seminar Paper

Title

VHDL BASED SYMBOLIC MODEL CHECKER WITH IMPROVED CTL PROPERTY LANGUAGE

Author(s)

SHOJAI HAMID | PARANDEH AFSHAR HADI | NAVABI ZAINALABEDIN

Keywords

VHDL

VERIFICATION

MODEL CHECKING

FSM

BDD

MDD

CTL

IMAGE COMPUTATION

REACHABILITY ANALYSIS

COVERAGE

Abstract

MOST EXISTING VERIFICATION TOOLS SUFFER FROM HAVING A STANDARD LANGUAGE FOR DESIGN SPECIFICATION. ALTHOUGH MOST OF THESE TOOLS SUPPORT STANDARD HARDWARE DESCRIPTION LANGUAGES, BUT THE SUBSET OF THE HDL THEY SUPPORT IS VERY LIMITED. IN THIS PAPER WE INTRODUCE A VERIFICATION TOOL, WHICH DOES NOT HAVE THESE LIMITATIONS. WE USE SYMBOLIC MODEL CHECKING TO VERIFY A VHDL DESIGN. A DATA FLOW GRAPH (DFG) IS EXTRACTED FROM THE VHDL CODE, WHICH HAS BEEN FULLY IMPLEMENTED IN OBJECT ORIENTED FORMAT IN C++ AND COVERS ABOUT 90% OF THE SYNTHESIZABLE SUBSET OF VHDL. WE USE REDUCED ORDERED BINARY DECISION DIAGRAMS TO REPRESENT FSM DESCRIPTION OF A SYSTEM IN TERMS OF TRANSITION RELATIONS. THE CONVERSION OF DFG TO BDDS IS DONE INSIDE THE DFG CLASSES. FOR THE PROPERTY LANGUAGE, WE HAVE USED CTL WITH EXTENSIONS TO INCLUDE EVENT SEQUENCE STRUCTURES AND WORD-LEVEL PROPERTIES. FOR THESE EXTENSIONS, WE HAVE IMPLEMENTED A MULTI-VALUED DECISION DIAGRAM (MDD) PACKAGE OVER AN EXISTING BDD PACKAGE. THE COMPLETE PACKAGE IS PUT INTO A USER-FRIENDLY ENVIRONMENT FOR AUTOMATIC VERIFICATION OF FSMS. WE HAVE COMPARED OUR RESULTS WITH VIS AND SMV TOOLS.

Cites

No record.

References

No record.

Cite

APA: Copy

SHOJAI, HAMID, PARANDEH AFSHAR, HADI, & NAVABI, ZAINALABEDIN. (2004). VHDL BASED SYMBOLIC MODEL CHECKER WITH IMPROVED CTL PROPERTY LANGUAGE. Confrance Salane Anjomane Computer Iran. SID. https://sid.ir/paper/905884/en

Vancouver: Copy

SHOJAI HAMID, PARANDEH AFSHAR HADI, NAVABI ZAINALABEDIN. VHDL BASED SYMBOLIC MODEL CHECKER WITH IMPROVED CTL PROPERTY LANGUAGE. 2004. Available from: https://sid.ir/paper/905884/en

IEEE: Copy

HAMID SHOJAI, HADI PARANDEH AFSHAR, and ZAINALABEDIN NAVABI, “VHDL BASED SYMBOLIC MODEL CHECKER WITH IMPROVED CTL PROPERTY LANGUAGE,” presented at the Confrance Salane Anjomane Computer Iran. 2004, [Online]. Available: https://sid.ir/paper/905884/en

Related Journal Papers

No record.

Related Seminar Papers

No record.

Related Plans

No record.

Recommended Workshops