seq_sat logo  
 Sequential Circuit SAT solver 
About
Seq_SAT  is a tool for sequential circuit SAT problems. Given a sequential circuit and an initial state,  it finds an ordered sequence of input vectors to satisfy the desired objective or proves no such sequence exists. The input file format is ISCAS'89 bench format (example).  The output is the results of justifying each output of the circuit to be 1.

For questions about Seq_SAT, contact Feng Lu or Tim Cheng.

News
06/09/2005: The source code of Seq_SAT evaluation version is released.  

 


Documentation

The following papers describe some of the technical details about the ideas behind the tool.
  • F. Lu, L.-C. Wang, K.-T. Cheng, J. Moondanos and Z. Hanna, "A Signal Correlation Guided Circuit-SAT Solver". In Journal of Universal Computer Science, vol. 10, no. 12, 1629-1654, 2004. (pdf)
  • F. Lu, M. K. Iyer, G. Parthasarathy and K.-T. Cheng, "An Efficient Sequential SAT Solver With Improved Search Strategies". In Proc. Design, Automation & Test in Europe , pp. 1102-1107, Mar. 7-11, 2005. (pdf)

 

Download

This research was sponsored by the Gigascale Systems Research Center (GSRC), the Semiconductor Research Corporation (SRC), the National Science Foundation (NSF) under grant no. CCR-0096383, Intel Corporation, and California MICRO program.