NDLI: Improving symbolic traversals by means of activity profiles

Content Provider	IEEE Xplore Digital Library
Author	Cabodi, G. Camurati, P. Qner, S.
Copyright Year	1999
Description	Author affiliation: Dipt. di Autom. e Inf., Politecnico di Torino, Italy (Cabodi, G.)
Abstract	Symbolic techniques have undergone major improvements in the last few years. Nevertheless they are still limited by the size of the involved BDDs, and extending their applicability to larger and real circuits is a key issue. Within, this framework, we introduce "activity profiles" as a novel technique to characterize transition relations. In our methodology a learning phase is used to collect activity measures, related to time and space cost, for each BDD node of the transition relation. We use inexpensive reachability analysis as learning technique, and we operate within inner steps of image computations involving the transition relation and state sets. The above informations can be used for several purposes. In particular, we present an application of activity profiles in the field of reachability analysis itself. We propose transition relation subsetting and partial traversals of the state transition graph. We show that a sequence of partial traversals is able to complete a reachability analysis problem with smaller memory requirement and improved time performance.
Starting Page	306
Ending Page	311
File Size	597590
Page Count	6
File Format	PDF
ISBN	1581130929
DOI	10.1109/DAC.1999.781331
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	1999-06-21
Publisher Place	USA
Access Restriction	Subscribed
Rights Holder	Association for Computing Machinery, Inc. (ACM)
Subject Keyword	Reachability analysis Data structures Boolean functions Circuits Binary decision diagrams Costs Formal verification Explosions Hardware Permission
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Biasing symbolic search by means of dynamic activity profiles

Improving symbolic reachability analysis by means of activity profiles

Reachability analysis for formal verification of SystemC

Evolutionary algorithm approach for symbolic FSM traversals

Improving SAT-based bounded model checking by means of BDD-based approximate traversals

Integrating SAT with Multiway Decision Graphs for efficient model checking

Maximality-based symbolic model checking

The use of random simulation in formal verification

Linear Sifting Of Decision Diagrams

Improving symbolic traversals by means of activity profiles

Similar Documents

Biasing symbolic search by means of dynamic activity profiles

Improving symbolic reachability analysis by means of activity profiles

Reachability analysis for formal verification of SystemC

Evolutionary algorithm approach for symbolic FSM traversals

Improving SAT-based bounded model checking by means of BDD-based approximate traversals

Integrating SAT with Multiway Decision Graphs for efficient model checking

Maximality-based symbolic model checking

The use of random simulation in formal verification

Linear Sifting Of Decision Diagrams

Improving symbolic traversals by means of activity profiles