Directed automated symbolic verification of formal properties with local variables

Das, Sourasis ; Dasgupta, Pallab ; Banerjee, Ansuman ; Das, Partha Pratim (2009) Directed automated symbolic verification of formal properties with local variables In: TENCON 2009 - 2009 IEEE Region 10 Conference, 23-26 January 2009, Singapore.

Full text not available from this repository.

Official URL:

Related URL:


This paper describes a methodology for checking formal properties with local variables expressed in SystemVerilog assertions. Given a behavioral design in SystemVerilog and a property with local variables, the technique uses automated directed searching to reveal all possible control-paths of the given design and tests the satisfaction of the property symbolically in the corresponding data-path operations for each of the control-paths. The advantage is twofold. First, any corner-case data-dependent bugs will eventually get caught due to use of symbolic satisfaction of the property, which otherwise is very likely to be missed if concrete value satisfaction is used as done by traditional simulation based verification. Second, using automated alternative path exploration performs best to identify a buggy data-path since every data-path is verified exactly once, whereas some datapath often gets either repeated or missed in simulation based verification.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Automatic Control; Control Systems; Computational Modeling; Automatic Testing; System Testing; Cost Accounting; Computer Bugs; Concrete; Discrete Event Simulation; Logic
ID Code:101670
Deposited On:12 Dec 2016 09:57
Last Modified:12 Dec 2016 09:57

Repository Staff Only: item control page