Yu Hu, 09/07/2007

========================================================================================

/// RTL Synthesizer project

* Handle logic shifter with constant number of shifting bits.
  The following source files are updated for this purpose:
  oagFpgaRtlGraph.cpp/.h oagFpgaSynthesis.cpp/.h
  oagFpgaVerilogSynthesis.cpp, oagFpgaModuleCompiler.cpp

* |TEST_XST| "logical_shifters_1.v", "logical_shifters_2.v" and
  "logical_shifters_3.v" are synthesized and verified.

* |TODO| The non-constant number of shifting bits is not supported.

* |TEST_XST| "register_1.v" to "register_5.v" are synthesized and verified.

* |TEST_XST| "shift_register_1.v" to "shift_register_8.v" (expect for
        * "shift_register_2.v") are synthesized and verified.

* |TODO| "shift_registers_2.v" is synthesized but failed to be verified.
  The reason is that there support for negative-edge clock is problematic.

* |TEST_XST| "state_machines_1.v" to "state_machines_3.v" are synthesized
  and verified.

* |TODO| "dynamic_shift_registers_1" can't be synthesized, the reason is that
  "ERROR: Net data , bit index is not a constant".

* Summary of the categories of Xilinx benchmarks that have been synthesized and verified:

  + arithemtic operations: adders, multipilers, dividers
  + control units: different descriptions of multiplexers
  + registers: synchroneous and asynchroneous DFFs
  + latches: different Verilog styles that will infer a latch
  + counters: combinations of sequential and arithemtic elements
  + decoders and encoders: complicate combinational circuits with control units
  + shifters: combinational and sequential shifters
  + state_machines: complex combinational and sequential elements.

* Summary of circuits that can't be handled at present:
  
  + registers with negative clock triggers 
  + dynamtic_shift_registers: the bit index of a net is not a constant

========================================================================================

/// SAT Boolean matching project 

* Implementation issues for further improving SAT encoding efficiency:

  1. CNFs are divided into two parts: CNFs dependent to output and the rest
  2. generate CNFs not dependent on output once
  3. for each permutation, calculate the truth table after permutation and update the 
     CNFs dependent on output (by miniSAT's parameter assumption capability). 
     basically, for a 9-input PLB, 512 clauses need to be updated for each permutation

* Long-term research directions (in the same order as listed below):

  1. update the current single-output SAT Boolean matcher to handle multiple-output PLBs. 
     The updating should be straightforward. The possible problems are 

     i) the functional symmetries for multiple-output Boolean functions may not as 
        significant as single-output ones, 
     ii) the symmetry calculation time for multiple-output function will be longer which 
        may reduce the speedup of our symmetry-aware approach. 
        But let's wait for the experimental results.

  2. apply the SAT base Boolean matcher to perform resynthesis (post-mapping optimization). 
     The following steps are needed.
      2.1. look for frequently-existing sub-circuit patterns in the mapped circuits in a 
           training set, and design proper multiple-output PLBs as the library for resynthesis
      2.2. perform the resynthesis by sliding-window like fashion, i.e., 
           for a sub-circuit (sub-graph), test if it can be implemented by a PLB in the library 
           to reduce the logic area (LUT#). One key point is to find a way to efficiently decide 
           which sub-circuits have the most potential to be reduced.
      2.3. compare the effectiveness of the single-output based resynthesis and the multiple-output 
           based one.