The package "symsim" is a symbolic simiulator. With symbols assigned on the inputs, it simulates 
the combinational circuits or sequential circuits with limited timeframe extention. It can be 
used in the equivalence checking or property checking.

==============================================================================================
Installation: 
%gzip -dc symsim.tar.gz | tar xvf -
There are two directories: ./symsim stores the source code and ./testcase stores the testcases.

To compile the source code, please go to the directory ./symsim.
The CUDD package is needed to compile the source code. Please modify the Makefile by typing 
the correct path of installed cudd package and then type
%make 

==============================================================================================         
Netlist file:

The circuit should be described in the FL netlist format for the software to be applicable. 
The netlist is described as: 

Syntax : gID gate_type fanin_num fanin1 fanin2... fanout
Example: g1 OR 2 fanin1 fanin2 fanout

==============================================================================================
Assertion file (optional):

The assertion is used to specify the symbols assigned on the input ports. It is described as: 

Syntax : Portname is Symbolname from start_timeframe to end_timeframe
Example: y is y[2] from t1 to t10
         x is T    from t1 to t10
T and F are researved symbolnames representing function one and zero.

If no assertion file is given, symbolic simulator will assign all the primary input ports with 
different symbols at each timeframe. 

==============================================================================================
Usage:  symsim [options]
         -g .fl         (read in circuit netlist)
         -a .ci         (read in assertion)
         -t timeframe   (timeframes extention for sequential circuits)
         -ord           (run symbolic simulator without partition)
         -tp            (run symbolic simulator with 2-tuple list partition)
         -log .log      (log file)
         
==============================================================================================
Testcases:

FPADD (floating point adder)
%symsim -g ../testcase/FPadd/fadd.syn -a testcase/FPadd/fadd.ci -ord
%symsim -g ../testcase/FPadd/fadd.syn -a testcase/FPadd/fadd.ci -tp

HWB (hidden weighted bit circuit)
%symsim -g ../testcase/HWB/hwb_51_syn.fl -ord 
simulate circuit using ordinary(non-partition) symbolic simulation.
%symsim -g ../testcase/HWB/hwb_51_syn.fl -tp
simulate circuit using partitioned symbolic simulation.
%symsim -g ../testcase/HWB/hwb_51_syn.fl -ord -g_rev ../testcase/HWB/hwb_51_syn.fl -tp_rev
simulate the two circuits using ordinary and partitioned symbolic simulation separately and 
do equivalence checking for the results.

GCD (Greatest common divisor)
%symsim -g ../testcase/GCD/gcd_syn.fl -a ../testcase/GCD/gcd_syn.ci -tp

Demo (Extended Finite Satate Machine circuit)
%symsim -g ../testcasee/Demo/demo_syn.fl -t 7 -tp

Fancy (Extended Finite Satate Machine circuit)
%symsim -g ../testcasee/Fancy/fancy_syn.fl -t 2 -tp

Diffeq (HLSW92)
%symsim -g ../testcasee/Diffeq/diffeq_dw_syn_gtech.fl -t 3 -tp

Am2910 (HLSW92)
%symsim -g ../testcasee/Am2910/m2910_dw_syn_gtech.fl -t 2 -tp

==============================================================================================
Prepare the testcases:

The testcase (RTL netlist) is synthesized from the VHDL design descriptions using synthesis tool
(design_analyzer). The RTL netlist is mapped using the gtech library and translated into .fl format.

In each testcase directory, The VHDL design descriptions are located in the directory ./rtl_design. 
The RTL netlist in verilog format is located in ./netlist_verilog, it has been translated into .fl 
format for simulation.

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