Shobha Vasudevan

Automatic assertion/property generation in hardware and software

• Generating Concise Assertions with Complete Coverage. Joint work with Lingyi Liu and Chen Hsuan Lin. To appear in Great Lakes Symposium on VLSI (GLSVLSI)

• Mining Hardware Assertions With Guidance From Static Analysis. Joint work with Samuel Hertz and David Sheridan. To appear in IEEE Trans. on CAD of Integrated Circuits and Systems (IEEE TCAD)

• Word Level Feature Discovery to Enhance Quality of Assertion Mining. Joint work with Lingyi Liu and Chen-Hsuan Lin. ICCAD 2012.

• GoldMine: Automatic Assertion Generation Using Data Mining and Static Analysis, Joint work with David Sheridan, David Tcheng, Sanjay Patel, Bill Tuohy and Daniel Johnson. In DATE 2010..

• Automatic generation of assertions from system level design using data mining. Joint work with Lingyi Liu, David Sheridan and Viraj Athavale. MEMOCODE 2011.

• PRECIS: Inferring Invariants using Program Path Guided Clustering. Joint work with Parth Sagdeo, Viraj Athavale and Sumant Kowshik. ASE 2011 .

• Signature Pattern Covering via Local Greedy Algorithm and Pattern Shrink. Joint work with Hyungsul Kim, David Sheridan, Sungjin Im, Tarek Abdelzaher and Jiawei Han. 2011 IEEE International Conference on Data Mining (ICDM)

Variation analysis (timing/process/ageing) in RTL using formal probabilistic and statistical methods

• Early prediction of NBTI effects using RTL source code analysis Joint work with Jayanand Asok Kumar, Ken Butler, Hee-Soo Kim. To appear in Design Automation Conference DAC 2012

• Formal performance analysis for faulty MIMO hardware. Joint work with Jayanand Asok Kumar. To appear in IEEE Transactions on Very Large Scale Integration Systems


• Verifying Dynamic Power Management Schemes Using Statistical Model Checking. Joint work with Jayanand Asok Kumar. Asia and South Pacific Design Automation Conference ASP-DAC 2012


• Variation-Conscious Formal Timing Verification in RTL. Joint work with Jayanand Asok Kumar. VLSI Design 2011. UIUC technical report on SHARPE. .


• Statistical Guarantees of Performance for MIMO Designs, Joint work with Jayanand Asok Kumar. In DSN 2010. .
• A Scalable Approach for Throughput Estimation of Timing Speculation Designs , Joint work with Viraj Athavale and Jayanand Asok Kumar. MWSCAS 2010.

Analog verification

• Goal-Oriented Test Generation for Analog Circuits. Joint work with Adel Ahmadyan and Jayanand Asok Kumar.Design Automation Conference DAC 2012

• Reachability Analysis of Nonlinear Analysis through Iterative Reachable Set Reduction. Joint work with Seyed Nematollah Ahmadyan.Design Automation and Test in Europe DATE 2013

• Runtime Verification of Nonlinear Analog Circuits Using Incremental Time-Augmented RRT Algorithm. Joint work with Seyed Nematollah Ahmadyan and Jayanand Asok Kumar.Design Automation and Test in Europe DATE 2013


• . Rapidly-Exploring Random Forests: Algorithms and Applications in Verification of Analog Circuits. Joint work with Seyed Nematollah Ahmadyan. Frontiers in Analog CAD FAC 2013



Scaling probabilistic model checking

• Scaling Probabilistic Timing Verification of Hardware Using Abstractions in Design Source Code. Joint work with Jayanand Asok Kumar and Lingyi Liu. To appear in FMCAD 2011.


• Automatic compositional reasoning for probabilistic model checking of hardware designs , Joint work with Jayanand Asok Kumar QEST 2010. .



Design validation, Coverage analysis and Test generation

• "Evaluating Code Coverage of Assertions by Static Analysis of RTL,"Coordinated Science Laboratory technical report UILU-ENG-11-2209 (CRHC-11-07), University of Illinois at Urbana-Champaign, October 2011. Joint work with Viraj Athavale, Sam Hertz


• Using Static Analysis for Coverage Extraction from Emulation/Prototyping Platforms. Joint work with Viraj Athavale, Samuel Hertz and Darshan Jetley. CODES+ISSS 2012.


• A Technique for Test Coverage Closure Using GoldMine Joint work with Lingyi Liu, David Sheridan and William Tuohy. To appear in IEEE Transactions on COMPUTER-AIDED DESIGN of Integrated Circuits and Systems


• Efficient Validation Input Generation in RTL by Hybridized Source Code Analysis. Joint work with Lingyi Liu. Design Automation and Test Conference (DATE) 2011. CSL Tech report here


• Towards Coverage Closure: Using GoldMine Assertions for Generating Design Validation Stimulus. Joint work with David Sheridan, Lingyi Liu and William Tuohy. DATE 2011. UIUC tech report on this work can be found here


• STAR: Generating input vectors for design validation by static analysis of RTL, Joint work with Lingyi Liu. Invited paper in HLDVT 2009.


• Automated Mapping of Pre-Computed Module-Level Test Sequences to Processor Instructions, Joint work with Sankar Gurumurthy and Jacob Abraham, International Test Conference (ITC) 2005


• Automated functional propagation of module level test reponses, Joint work with Sankar Gurumurthy and Jacob Abraham, International Test Conference (ITC) 2006



Static analysis methods to scale hardware verification

• Scaling RTL Property Checking Using Feasible Path Analysis and Decomposition. Joint work with Lingyi Liu. To appear in Great Lakes Symposium on VLSI (GLSVLSI)


• High Level Static Analysis of System Descriptions for Taming Verification Complexity, PhD Thesis, The University of Texas at Austin


• Efficient Model Checking of hardware using Conditioned Slicing, Joint work with Allen Emerson and Jacob Abraham, AVOCS 2004. ENTCS proceedings of AVOCS 2004.


• Static Program Transformation for Efficient Software Model Checking, Joint work with Jacob Abraham, book chapter in IFIP Congress Topical Sessions 2004


• Efficient Microprocessor Verification using Antecedent Conditioned Slicing, Joint work with Vinod Viswanath and Jacob Abraham, VLSI Design 2007


• Microprocessor Verification using RT-Level Static Analysis Techniques, Submitted to IEEE Transactions on VLSI. This paper contains a revised antecedent conditioned slicing algorithm.


• Improved Verification of Hardware Designs through Antecedent Conditioned Slicing, Joint work with Allen Emerson and Jacob Abraham, In International Journal on Software Tools for Technology Transfer (STTT), Feb 2007. Some notes on the implementation of the algorithm by Dr. Emerson.



System level/RTL equivalence checking

• Automatic Verification of Arithmetic Circuits using Stepwise Refinement of Term Rewriting Systems, Joint work with Vinod Viswanath, Robert Sumners and Jacob Abraham, IEEE Transactions on Computers


• Automatic Verification of Arithmetic circuits in RTL using Term Rewriting Systems, Master's thesis


• Sequential Equivalence Checking between System Level and RTL Descriptions, Design Automation for Embedded Systems, Springer US, 26.11.2008, vol. 12, no. 4, pp. 377-396


• Automatic Decomposition for Sequential Equivalence Checking of System Level and RTL Descriptions, Joint work with Vinod Viswanath, Jacob Abraham and Jiajin Tu, MEMOCODE 2006


• Sequential Equivalence Checking of System Level and RTL Descriptions using Effective Compare Points, in ACISC 2006