TG-Pro - A SAT-based ATPG System

SAT-based Test pattern Generation with efficient fault Propagation constraints

System Description

TG-Pro is a SAT-based model and system for ATPG of digital combinational systems. Compared to other models, the main innovation of TG-Pro is its compact representation. Whereas existing models use 3 variables per circuit node, TG-Pro uses only two variables per circuit node. The differences in the model allow very significant savings in problem instance representation, which are often reflected in the performance of the ATPG system.


7/Jun/2011: New wiki page published for TG-Pro. 27/May/2011: first public release of TG-Pro Version 2.0.


For research and teaching purposes only.

TG-Pro is available as an executable in the following platforms:


README file for TG-Pro.

Recent publications describing the models and algorithms in TG-Pro include:


Example Usage

Show manual:

  ./tgpro -h

Default mode:

  ./tgpro c1908.bench

Tool Demo

  • Basic execution of the tool (video)
  • Run the experiments shown in the PoS'2011 paper (video, associated package, and output)
  • Evaluation of the SAT-based models for ATPG (addressed in the HLDVT'2009 paper) (video)
  • Show the detailed result of each fault (addressed in the HLDVT'2009 paper) (video)


  • Benchmarks and scripts used in PoS'2011 and JSAT paper (submitted).
  • ISCAS85 (in ISCAS89 format) and ISCAS85_fault_list copyright by F. Brglez and H. Fujiwara, A neutral list of 10 combinational benchmark circuits and a target translator in FORTRAN, in International Symposium on Circuits and Systems, June 1985, pp. 695–698.
  • ISCAS89 and ISCAS89_fault_list copyright by F. Brglez, D. Bryan, and K. Kozminski : Combinational profiles of sequential benchmark circuits, in International Symposium on Circuits and Systems, May 1989, pp. 1929–1934.
  • ITC99 (second edition) and ITC99_fault_list copyright by CAD Group, Politecnico di Torino. Available:
  • Circuit CNF benchmarks from TG-Pro copyright by Huan Chen and Joao Marques-Silva. TG-Pro converts ISCAS85 and ISCAS89 benchmark circuits in .bench format to DIMACS CNF files. The sequential circuits are converted into combinational circuits. No constraint of ATPG problems are added to these benchmarks, only the original circuits are converted.



The developement of TG-Pro was partially supported by

European Commission FP7 and Science Foundation Ireland

Wiki Status

Under construction

Last update: 4 May 2013