fold_unfold.c

Go to the documentation of this file.

extern "C" {

#include "tarski.h"

extern F
build_fold_unfold_wrapper();

F 
build_fold_unfold_check()
{
  F fold_neq_unfold = build_fold_unfold_wrapper();
  Fnode *bmc_problem = node_tfe(fold_neq_unfold.raw, 10);
  Net_t *neq_net;
  //neq_net = Net_CreateFromFormula(fold_neq_unfold.raw);
  neq_net = Net_CreateFromFormula(bmc_problem);
  
  Net_DoBryantReduction(neq_net);
  Net_t *bry_neq_net = Net_CreateFromFormula(array_fetch(Fnode *, neq_net->formulas, 0));

  //st_table *processedTable = st_init_table( (int (*)() ) st_ptrcmp, (int (*)() ) st_ptrhash );
  //Net_PrintFormula(neq_net, array_fetch(Fnode *, neq_net->formulas,0),  processedTable);
  //Net_PrintVHDL(neq_net, stdout, 4);
  Net_PrintVHDL(bry_neq_net, 4, "fold_unfold.vhdl", "fold_unfold");
  return fold_neq_unfold;  
}

F 
build_fold_unfold_wrapper()
{
  
  F oscillator = br("oscillator");
  F next_oscillator = !oscillator;
  oscillator << (FALSE() % next_oscillator);

  F xdata1 = si("xdata1");
  F xdata2 = si("xdata2");
  F xdata3 = si("xdata3");
  F xdata4 = si("xdata4");
  
  F fold_xdata_reg1 = sr("fold_xdata_reg1");
  F fold_xdata_reg2 = sr("fold_xdata_reg2");
  F fold_xdata_reg3 = sr("fold_xdata_reg3");
  F fold_xdata_reg4 = sr("fold_xdata_reg4");
  
  fold_xdata_reg1 << (xdata1 % fold_xdata_reg2);
  fold_xdata_reg2 << (xdata2 % fold_xdata_reg3);
  fold_xdata_reg3 << (xdata3 % fold_xdata_reg4);
  fold_xdata_reg4 << (xdata4 % fold_xdata_reg4);

  F ydata_n_minus_1 = si("ydata_n_minus_1");
  F ydata_n_minus_2 = si("ydata_n_minus_2");
  F ydata_n_minus_3 = si("ydata_n_minus_3");

  F fold_ydata_n_minus_1 = sr("fold_ydata_n_minus_1");
  F fold_ydata_n_minus_2 = sr("fold_ydata_n_minus_2");
  F fold_ydata_n_minus_3 = sr("fold_ydata_n_minus_3");
  
  F adata_reg = sr("adata_reg");
  F bdata_reg = sr("bdata_reg");
  
  F adata = si("adata");
  F bdata = si("bdata");
  
  adata_reg << (adata % adata_reg);
  bdata_reg << (bdata % bdata_reg);
  
  F fold_a_y_minus_2 = uif2("multiply", adata_reg, fold_ydata_n_minus_2);
  
  F fold_b_y_minus_3 = uif2("multiply", bdata_reg, fold_ydata_n_minus_3);
  
  F fold_intermediate_add = uif2("add", fold_a_y_minus_2, fold_b_y_minus_3);

  F fold_ydata = uif2("add", fold_intermediate_add, fold_xdata_reg1);
  
  fold_ydata_n_minus_1 << (ydata_n_minus_1 % fold_ydata);
  fold_ydata_n_minus_2 << (ydata_n_minus_2 % fold_ydata_n_minus_1);
  fold_ydata_n_minus_3 << (ydata_n_minus_3 % fold_ydata_n_minus_2);
  
  // Now we concentrate on unfolding
  
  F unfold_freeze = !oscillator;

  F unfold_xdata_reg1 = sr("unfold_xdata_reg1");
  F unfold_xdata_reg2 = sr("unfold_xdata_reg2");
  F unfold_xdata_reg3 = sr("unfold_xdata_reg3");
  F unfold_xdata_reg4 = sr("unfold_xdata_reg4");
  
  F next_unfold_xdata_reg1 = mux(unfold_freeze,
                                 unfold_xdata_reg1,
                                 unfold_xdata_reg3);
  
  F next_unfold_xdata_reg2 = mux(unfold_freeze,
                                 unfold_xdata_reg2,
                                 unfold_xdata_reg4);
  
  
  F next_unfold_xdata_reg3 = mux(unfold_freeze,
                                 unfold_xdata_reg3,
                                 unfold_xdata_reg4);
  
  F next_unfold_xdata_reg4 = mux(unfold_freeze,
                                 unfold_xdata_reg4,
                                 unfold_xdata_reg4);
  
  unfold_xdata_reg1 << (xdata1 % next_unfold_xdata_reg1);
  unfold_xdata_reg2 << (xdata2 % next_unfold_xdata_reg2);
  unfold_xdata_reg3 << (xdata3 % next_unfold_xdata_reg3);
  unfold_xdata_reg4 << (xdata4 % next_unfold_xdata_reg4);

  F unfold_ydata_n_minus_1 = sr("unfold_ydata_n_minus_1");
  F unfold_ydata_n_minus_2 = sr("unfold_ydata_n_minus_2");
  F unfold_ydata_n_minus_3 = sr("unfold_ydata_n_minus_3");
  
  F unfold_a_y_minus_2 = uif2("multiply", adata_reg, unfold_ydata_n_minus_2);
  F unfold_a_y_minus_1 = uif2("multiply", adata_reg, unfold_ydata_n_minus_1);
  
  F unfold_b_y_minus_3 = uif2("multiply", bdata_reg, unfold_ydata_n_minus_3);
  F unfold_b_y_minus_2 = uif2("multiply", bdata_reg, unfold_ydata_n_minus_2);
  
  F unfold_intermediate_add1 = uif2("add", unfold_a_y_minus_2, unfold_b_y_minus_3);
  F unfold_intermediate_add2 = uif2("add", unfold_a_y_minus_1, unfold_b_y_minus_2);
  
  F unfold_ydata = uif2("add", unfold_intermediate_add1, unfold_xdata_reg1);
  F unfold_ydata_plus_1 = uif2("add", unfold_intermediate_add2, unfold_xdata_reg2);
  
  F next_unfold_ydata_n_minus_1 = mux(unfold_freeze,
                                      unfold_ydata_n_minus_1,
                                      unfold_ydata_plus_1);
  
  F next_unfold_ydata_n_minus_2 = mux(unfold_freeze,
                                      unfold_ydata_n_minus_2,
                                      unfold_ydata);
  
  F next_unfold_ydata_n_minus_3 = mux(unfold_freeze,
                                      unfold_ydata_n_minus_3,
                                      unfold_ydata_n_minus_1);
  
  unfold_ydata_n_minus_1 << (ydata_n_minus_1 % next_unfold_ydata_n_minus_1);
  unfold_ydata_n_minus_2 << (ydata_n_minus_2 % next_unfold_ydata_n_minus_2);
  unfold_ydata_n_minus_3 << (ydata_n_minus_3 % next_unfold_ydata_n_minus_3);
  
  F check_assert = ((!oscillator & !(fold_ydata == unfold_ydata)) | (oscillator & !(fold_ydata == unfold_ydata_plus_1)));
  return check_assert;
}


}

---