Skip to Main Content
 

Global Search Box

 
 
 
 

Files

File List


ucin1022761893.pdf (521.63 KB)

ETD Abstract Container

Abstract Header

APPLICATIONS OF SATISFIABILITY IN SYNTHESIS OF RECONFIGURABLE COMPUTERS

SIVA, SUBRAMANYAN D.
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1022761893

Abstract Details

2002, MS, University of Cincinnati, Engineering : Computer Engineering.
This thesis addresses applications of satisfiability techniques in a reconfigurable computer (RC) synthesis framework. The two areas explored are the interconnect synthesis problem and the verification of synthesized register transfer level (RTL) designs. Traditionally, binary decision diagrams (BDD), an efficient canonical form for boolean expressions, have been applied to these problems. The disadvantage was the need of a good variable ordering to solve the problem efficiently. Most reconfigurable field programmable gate array (FPGA) architectures have programmable interconnection networks that can be reconfigured to implement various interconnection patterns among the FPGA's on the board. Partitioning tools for such architectures must produce the necessary interconnect configuration. This process is called Interconnect Synthesis. In our research, interconnect synthesis is based on a boolean satisfiability solver (SAT) using the Impulse Response technique. An appropriate methodology is needed to hierarchically specify the target interconnection network. An architecture description language called the Performance Description Language (PDL+), is used as the front end tool for modeling reconfigurable processors. These models are then elaborated in a symbolic environment called the Analyzer of Reconfigurable Computer (ARC). Boolean SAT solvers guarantee routing, if one exists. The results of SAT solvers are verified by feeding the obtained values back into the symbolic environment. Interconnect synthesis is performed on Wildforce and Corel RC processors. Grasp, Sato and Chaff solvers have been used. Experimental results show that large interconnect synthesis problems can be solved using SAT solvers and that Chaff has superior performance than the other solvers. In a high-level synthesis (HLS) flow, the behavioral specification in VHDL is subjected to scheduling, binding, interconnect and controller generation to obtain a register-transfer-level (RTL) design. In a successful design methodology, it is essential to verify the RTL design against its original specification. Traditionally, the task of verification is carried by simulation. This process is highly time intensive and it is not feasible to exhaustively simulate a design to guarantee its correctness. Formal verification attempts to establish universal properties about the design, independent of any particular set of inputs. In this thesis, synthesized RTL designs are verified using a SAT solver. This is to check whether the synthesis tool has generated a correct data path and controller. Data path verification is known as the combinational equivalence checking (CEC) problem. Experimental results show that as the bit size increase, the problem becomes hard and the SAT solver execution time is found to be large. It is observed that Chaff is the fastest of the three solvers. Also, the module concept is introduced for data-path verification. Controller verification is based on uninterpreted symbolic simulation procedure. The execution time on the benchmark examples is small.
Dr. Ranga Vemuri (Advisor)
107 p.
satisfiability; reconfigurable-computer; interconnect synthesis; high level synthesis; sat-solver

Recommended Citations

Citations

  • SIVA, S. D. (2002). APPLICATIONS OF SATISFIABILITY IN SYNTHESIS OF RECONFIGURABLE COMPUTERS [Master's thesis, University of Cincinnati]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1022761893

    APA Style (7th edition)

  • SIVA, SUBRAMANYAN. APPLICATIONS OF SATISFIABILITY IN SYNTHESIS OF RECONFIGURABLE COMPUTERS. 2002. University of Cincinnati, Master's thesis. OhioLINK Electronic Theses and Dissertations Center, http://rave.ohiolink.edu/etdc/view?acc_num=ucin1022761893.

    MLA Style (8th edition)

  • SIVA, SUBRAMANYAN. "APPLICATIONS OF SATISFIABILITY IN SYNTHESIS OF RECONFIGURABLE COMPUTERS." Master's thesis, University of Cincinnati, 2002. http://rave.ohiolink.edu/etdc/view?acc_num=ucin1022761893

    Chicago Manual of Style (17th edition)

ucin1022761893
860
© 2002, all rights reserved.
This open access ETD is published by University of Cincinnati and OhioLINK.