research-article

Stimulus generation for constrained random simulation

Authors:

Nathan Kitchen,

Andreas KuehlmannAuthors Info & Claims

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

Pages 258 - 265

Published: 05 November 2007 Publication History

Abstract

Constrained random simulation is the main workhorse in today's hardware verification flows. It requires the random generation of input stimuli that obey a set of declaratively specified input constraints, which are then applied to validate given design properties by simulation. The efficiency of the overall flow depends critically on (1) the performance of the constraint solver and (2) the distribution of the generated solutions. In this paper we discuss the overall problem of efficient constraint solving for stimulus generation for mixed Boolean/integer variable domains and propose a new hybrid solver based on Markov-chain Monte Carlo methods with good performance and distribution.

References

[1]

T. Grötker, S. Liao, G. Martin, and S. Swan, System Design with SystemC. Boston: Kluwer Academic, 2002.

Digital Library

[2]

S. Sutherland, S. Davidmann, and P. Flake, SystemVerilog for Design: A guide to using SystemVerilog for hardware design and modeling. Norwell, MA, USA: Kluwer Academic, 2003.

Digital Library

[3]

S. Iman and S. Joshi, The e Hardware Verification Language. Norwell, MA, USA: Kluwer Academic, 2004.

[4]

J. Yuan, K. Shultz, C. Pixley, H. Miller, and A. Aziz, "Modeling design constraints and biasing in simulation using BDDs," in Digest Tech. Papers IEEE/ACM Int'l Conf. Computer-Aided Design, pp. 584--589, Nov. 1999.

Digital Library

[5]

J. Yuan, A. Aziz, C. Pixley, and K. Albin, "Simplifying Boolean constraint solving for random simulation-vector generation," IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 23, pp. 412--420, Mar. 2004.

Digital Library

[6]

J. H. Kukula and T. R. Shiple, "Building circuits from relations," in Proc. 12th Int'l Conf. Computer-Aided Verif. (CAV), pp. 113--123, Springer-Verlag, 2000.

Digital Library

[7]

M. A. Iyer, "RACE: A word-level ATPG-based constraints solver system for smart random simulation," in IEEE International Test Conference (ITC), (Charlotte, NC, United States), pp. 299--308, Sept. 2003.

[8]

M. Davis and H. Putnam, "A computing procedure for quantification theory," J. ACM, vol. 7, pp. 201--215, 1960.

Digital Library

[9]

M. Davis, G. Logemann, and D. Loveland, "A machine program for theorem proving," Comms. ACM, vol. 5, pp. 394--397, July 1962.

Digital Library

[10]

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an efficient SAT solver," in Proc. 38th ACM/IEEE Design Automation Conf., pp. 530--535, June 2001.

Digital Library

[11]

W. Wei, J. Erenrich, and B. Selman, "Towards efficient sampling: Exploiting random walk strategies," in Proc. Nat'l Conf. Artificial Intelligence, pp. 670--676, Jul. 2004.

Digital Library

[12]

N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller, "Equations of state calculations by fast computing machines," J. Chem. Phys., vol. 21, pp. 1087--1092, June 1953.

[13]

B. Selman, H. A. Kautz, and B. Cohen, "Local search strategies for satisfiability testing," in Proc. 2nd DIMACS Challenge on Cliques, Coloring, and Satisfiability (M. Trick and D. S. Johnson, eds.), (Providence RI), 1993.

[14]

R. Dechter, K. Kask, E. Bin, and R. Emek, "Generating random solutions for constraint satisfaction problems," in 18th Nat'l Conf. Artificial Intelligence (AAAI02), pp. 15--21, July 2002.

Digital Library

[15]

V. Gogate and R. Dechter, "A new algorithm for sampling CSP solutions uniformly at random," tech. rep., School of Information and Computer Science, University of California, Irvine, May 2006.

[16]

A. Chandra, V. Iyengar, D. Jameson, R. Jawalekar, I. Nair, B. Rosen, M. Mullen, J. Yoon, R. Armoni, D. Geist, and Y. Wolfsthal, "AVPGEN--- a test generator for architectural verification," IEEE Trans. Very Large Scale Integration, vol. 3, no. 2, pp. 188--200, 1995.

Digital Library

[17]

K. Shimizu and D. L. Dill, "Deriving a simulation input generator and a coverage metric from a formal specification," in Proc. 39th Design Automation Conf., (New Orleans, LA, United States), pp. 801--806, Jun 2002.

Digital Library

[18]

W. K. Hastings, "Monte Carlo sampling methods using Markov chains and their applications," Biometrika, vol. 57, pp. 97--109, 1970.

[19]

S. Geman and D. Geman, "Stochastic relaxation, Gibbs distributions, and the Bayesian restoration of images," IEEE Trans. Pattern Analysis and Machine Intelligence, vol. 6, pp. 721--741, Nov. 1984.

Digital Library

[20]

A. E. Gelfand and A. F. M. Smith, "Sampling-based approaches to calculating marginal densities," J. Amer. Statist. Assoc., vol. 85, no. 410, pp. 398--409, 1990.

[21]

P.-H. Ho, T. Shiple, K. Harer, J. Kukula, R. Damiano, V. Bertacco, J. Taylor, and J. Long, "Smart simulation using collaborative formal and simulation engines," in Digest Tech. Papers IEEE/ACM Int'l Conf. Computer-Aided Design, pp. 120--126, Nov. 2000.

Digital Library

[22]

S. Shyam and V. Bertacco, "Distance-guided hybrid verification with GUIDO," in Design Automation and Test in Europe, Mar. 2006.

Digital Library

[23]

R. E. Bryant, "Graph-based algorithms for Boolean function manipulation," IEEE Trans. Computers, vol. 35, pp. 677--691, Aug. 1986.

Digital Library

[24]

"Property specification language, reference manual, version 1.1," Accellera Organization, June 2004.

[25]

Z. Xiu, D. A. Papa, P. Chong, C. Albrecht, A. Kuehlmann, R. A. Rutenbar, and I. L. Markov, "Early research experience with OpenAccess Gear: An open source development environment for physical design," in Proc. ACM Int'l Symp. Phys. Design (ISPD), pp. 94--100, Apr. 2005.

Digital Library

[26]

F. Somenzi, CUDD: CU Decision Diagram Package, Release 2.4.0. University of Colorado at Boulder, 2005.

[27]

N. Eén and N. Sörensson, "An extensible SAT-solver," in Proc. 6th Int'l Conf. Theory & Appl. Satisfiability Testing (SAT), pp. 502--518, May 2003.

Cited By

Xu JLiu YHe SLin HZhou YWang CCalandrino JTroncoso C(2023)MorFuzzProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620311(1307-1324)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620311
Wang ZNie PMiao XChen YWan CBu LZhao JJust RFraser G(2023)GenCoG: A DSL-Based Approach to Generating Computation Graphs for TVM TestingProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598105(904-916)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598105
Basset NDang TGigler FMateis CNičković DArun-Kumar SMery DSaha IZhang L(2021)Sampling of shape expressions with ShapExProceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3487212.3487350(118-125)Online publication date: 20-Nov-2021
https://dl.acm.org/doi/10.1145/3487212.3487350
Show More Cited By

Recommendations

Self-adjusting constrained random stimulus generation using splitting evenness evaluation and XOR constraints
ASP-DAC '09: Proceedings of the 2009 Asia and South Pacific Design Automation Conference

Constrained random stimulus generation plays significant roles in hardware verification nowadays, and the quality of the generated stimuli is key to the efficiency of the test process. In this work, we present a linear dynamic method to guide random ...
Automatic constraint generation for guided random simulation
ASPDAC '10: Proceedings of the 2010 Asia and South Pacific Design Automation Conference

In this paper, we proposed an Automatic Target Constraint Generation (ATCG) technique to automatically generate compact and high-quality constraints for the guided random simulation environment. Our objective is to tackle the biggest bottleneck of the ...
Transforming an under-constrained geometric constraint problem into a well-constrained one
SM '03: Proceedings of the eighth ACM symposium on Solid modeling and applications

We present an approach for handling geometric constraint problems with under-constrained configurations. The approach works by completing the given set of constraints with constraints that can be defined either automatically or drawn from an ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '07: Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design

November 2007

933 pages

ISBN:1424413826

General Chair:
Georges Gielen
ESAT-MICAS, Katholieke Univ. Leuven, Leuven, Belgium

Sponsors

CEDA: Council on Electronic Design Automation
SIGDA: ACM Special Interest Group on Design Automation
IEEE CASS/CANDE
IEEE-CS\DATC: IEEE Computer Society

Publisher

IEEE Press

Publication History

Published: 05 November 2007

Check for updates

Qualifiers

Research-article

Conference

ICCAD07

Sponsor:

CEDA
SIGDA
IEEE-CS\DATC

ICCAD07: The International Conference on Computer-Aided Design 2007

November 5 - 8, 2007

California, San Jose

Acceptance Rates

ICCAD '07 Paper Acceptance Rate 139 of 510 submissions, 27%;

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
458
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Xu JLiu YHe SLin HZhou YWang CCalandrino JTroncoso C(2023)MorFuzzProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620311(1307-1324)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620311
Wang ZNie PMiao XChen YWan CBu LZhao JJust RFraser G(2023)GenCoG: A DSL-Based Approach to Generating Computation Graphs for TVM TestingProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598105(904-916)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598105
Basset NDang TGigler FMateis CNičković DArun-Kumar SMery DSaha IZhang L(2021)Sampling of shape expressions with ShapExProceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design10.1145/3487212.3487350(118-125)Online publication date: 20-Nov-2021
https://dl.acm.org/doi/10.1145/3487212.3487350
Dutra RLaeufer KBachrach JSen KChaudron MCrnkovic IChechik MHarman M(2018)Efficient sampling of SAT solutions for testingProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180248(549-559)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180248
Chakraborty SMeel KVardi M(2016)Algorithmic improvements in approximate counting for probabilistic inferenceProceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence10.5555/3061053.3061119(3569-3576)Online publication date: 9-Jul-2016
https://dl.acm.org/doi/10.5555/3061053.3061119
Jain AGupta R(2016)Unified and Modular Modeling and Functional Verification Framework of Real-Time Image Signal ProcessorsVLSI Design10.1155/2016/72834712016(1)Online publication date: 1-Sep-2016
https://dl.acm.org/doi/10.1155/2016/7283471
Chakraborty SFremont DMeel KSeshia SVardi M(2015)On Parallel Scalable Uniform SAT Witness GenerationProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 903510.1007/978-3-662-46681-0_25(304-319)Online publication date: 11-Apr-2015
https://dl.acm.org/doi/10.1007/978-3-662-46681-0_25
Chakraborty SMeel KVardi M(2014)Balancing Scalability and Uniformity in SAT Witness GeneratorProceedings of the 51st Annual Design Automation Conference10.1145/2593069.2593097(1-6)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1145/2593069.2593097
Chakraborty SMeel KVardi M(2013)A Scalable and Nearly Uniform Generator of SAT WitnessesProceedings of the 25th International Conference on Computer Aided Verification - Volume 804410.5555/2958031.2958038(608-623)Online publication date: 13-Jul-2013
https://dl.acm.org/doi/10.5555/2958031.2958038
Kinsman AKo HNicolici N(2013)Hardware-efficient on-chip generation of time-extensive constrained-random sequences for in-system validationProceedings of the 50th Annual Design Automation Conference10.1145/2463209.2488882(1-6)Online publication date: 29-May-2013
https://dl.acm.org/doi/10.1145/2463209.2488882
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten