Improvements to word-level network package.

10 files changed, 484 insertions, 128 deletions

diff --git a/abclib.dsp b/abclib.dsp
index a4a3365e..a09acc7f 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -747,6 +747,10 @@ SOURCE=.\src\base\wlc\wlc.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\wlc\wlcAbs.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\wlc\wlcBlast.c
 # End Source File
 # Begin Source File
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index c1bda69a..84cc7620 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -1,4 +1,4 @@
-SRC +=    src/base/wlc/wlc.c \
+SRC +=    src/base/wlc/wlcAbs.c \
     src/base/wlc/wlcBlast.c \
     src/base/wlc/wlcCom.c \
     src/base/wlc/wlcNtk.c \
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 26e1c3d5..d94b0e2c 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -138,61 +138,62 @@ struct Wlc_Ntk_t_
     Vec_Int_t              vCopies;            // object first bits
 };
 
-static inline int          Wlc_NtkObjNum( Wlc_Ntk_t * p )                         { return p->iObj - 1;                                                   }
-static inline int          Wlc_NtkObjNumMax( Wlc_Ntk_t * p )                      { return p->iObj;                                                       }
-static inline int          Wlc_NtkPiNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vPis);                                         }
-static inline int          Wlc_NtkPoNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vPos);                                         }
-static inline int          Wlc_NtkCiNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vCis);                                         }
-static inline int          Wlc_NtkCoNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vCos);                                         }
-static inline int          Wlc_NtkFfNum( Wlc_Ntk_t * p )                          { return Vec_IntSize(&p->vCis) - Vec_IntSize(&p->vPis);                 }
-
-static inline Wlc_Obj_t *  Wlc_NtkObj( Wlc_Ntk_t * p, int Id )                    { assert(Id > 0 && Id < p->nObjsAlloc); return p->pObjs + Id;           }
-static inline Wlc_Obj_t *  Wlc_NtkPi( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vPis, i) );                    }
-static inline Wlc_Obj_t *  Wlc_NtkPo( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vPos, i) );                    }
-static inline Wlc_Obj_t *  Wlc_NtkCi( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vCis, i) );                    }
-static inline Wlc_Obj_t *  Wlc_NtkCo( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vCos, i) );                    }
-static inline Wlc_Obj_t *  Wlc_NtkFf( Wlc_Ntk_t * p, int i )                      { return Wlc_NtkObj( p, Vec_IntEntry(&p->vFfs, i) );                    }
-
-static inline int          Wlc_ObjIsPi( Wlc_Obj_t * p )                           { return p->Type == WLC_OBJ_PI;                                         }
-static inline int          Wlc_ObjIsPo( Wlc_Obj_t * p )                           { return p->fIsPo;                                                      }
-static inline int          Wlc_ObjIsCi( Wlc_Obj_t * p )                           { return p->Type == WLC_OBJ_PI || p->Type == WLC_OBJ_FO;                }
-static inline int          Wlc_ObjIsCo( Wlc_Obj_t * p )                           { return p->fIsPo || p->fIsFi;                                          }
-
-static inline int          Wlc_ObjId( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )           { return pObj - p->pObjs;                                               }
-static inline int          Wlc_ObjCiId( Wlc_Obj_t * p )                           { assert( Wlc_ObjIsCi(p) ); return p->Fanins[1];                        }
-static inline int          Wlc_ObjFaninNum( Wlc_Obj_t * p )                       { return p->nFanins;                                                    }
-static inline int          Wlc_ObjHasArray( Wlc_Obj_t * p )                       { return p->nFanins > 2 || p->Type == WLC_OBJ_CONST;                    }
-static inline int *        Wlc_ObjFanins( Wlc_Obj_t * p )                         { return Wlc_ObjHasArray(p) ? p->pFanins[0] : p->Fanins;                }
-static inline int          Wlc_ObjFaninId( Wlc_Obj_t * p, int i )                 { return Wlc_ObjFanins(p)[i];                                           }
-static inline int          Wlc_ObjFaninId0( Wlc_Obj_t * p )                       { return Wlc_ObjFanins(p)[0];                                           }
-static inline int          Wlc_ObjFaninId1( Wlc_Obj_t * p )                       { return Wlc_ObjFanins(p)[1];                                           }
-static inline int          Wlc_ObjFaninId2( Wlc_Obj_t * p )                       { return Wlc_ObjFanins(p)[2];                                           }
-static inline Wlc_Obj_t *  Wlc_ObjFanin( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int i ) { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, i) );                      }
-static inline Wlc_Obj_t *  Wlc_ObjFanin0( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )       { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 0) );                      }
-static inline Wlc_Obj_t *  Wlc_ObjFanin1( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )       { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 1) );                      }
-static inline Wlc_Obj_t *  Wlc_ObjFanin2( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )       { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 2) );                      }
-
-static inline int          Wlc_ObjRange( Wlc_Obj_t * p )                          { return p->End - p->Beg + 1;                                           }
-static inline int          Wlc_ObjRangeEnd( Wlc_Obj_t * p )                       { assert(p->Type == WLC_OBJ_BIT_SELECT); return p->Fanins[1] >> 16;     }
-static inline int          Wlc_ObjRangeBeg( Wlc_Obj_t * p )                       { assert(p->Type == WLC_OBJ_BIT_SELECT); return p->Fanins[1] & 0xFFFF;  }
-static inline int          Wlc_ObjSigned( Wlc_Obj_t * p )                         { return p->Signed;                                                     }
-static inline int          Wlc_ObjSign( Wlc_Obj_t * p )                           { return Abc_Var2Lit( Wlc_ObjRange(p), Wlc_ObjSigned(p) );              }
-static inline int *        Wlc_ObjConstValue( Wlc_Obj_t * p )                     { assert(p->Type == WLC_OBJ_CONST);      return Wlc_ObjFanins(p);       }
-static inline int          Wlc_ObjTableId( Wlc_Obj_t * p )                        { assert(p->Type == WLC_OBJ_TABLE);      return p->Fanins[1];           }
-static inline word *       Wlc_ObjTable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )        { return (word *)Vec_PtrEntry( p->vTables, Wlc_ObjTableId(pObj) );      }
-
-static inline void         Wlc_NtkCleanCopy( Wlc_Ntk_t * p )                      { Vec_IntFill( &p->vCopies, p->nObjsAlloc, 0 );                         }
-static inline int          Wlc_NtkHasCopy( Wlc_Ntk_t * p )                        { return Vec_IntSize( &p->vCopies ) > 0;                                }
-static inline void         Wlc_ObjSetCopy( Wlc_Ntk_t * p, int iObj, int i )       { Vec_IntWriteEntry( &p->vCopies, iObj, i );                            }
-static inline int          Wlc_ObjCopy( Wlc_Ntk_t * p, int iObj )                 { return Vec_IntEntry( &p->vCopies, iObj );                             }
-static inline Wlc_Obj_t *  Wlc_ObjCopyObj(Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj) {return Wlc_NtkObj(pNew, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)));}
-
-static inline void         Wlc_NtkCleanNameId( Wlc_Ntk_t * p )                    { Vec_IntFill( &p->vNameIds, p->nObjsAlloc, 0 );                        }
-static inline int          Wlc_NtkHasNameId( Wlc_Ntk_t * p )                      { return Vec_IntSize( &p->vNameIds ) > 0;                               }
-static inline void         Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i )     { Vec_IntWriteEntry( &p->vNameIds, iObj, i );                           }
-static inline int          Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj )               { return Vec_IntEntry( &p->vNameIds, iObj );                            }
-
-static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )       { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkCoNum(p) - Wlc_NtkCiNum(p) + Wlc_ObjCiId(pObj)); } 
+static inline int          Wlc_NtkObjNum( Wlc_Ntk_t * p )                           { return p->iObj - 1;                                                      }
+static inline int          Wlc_NtkObjNumMax( Wlc_Ntk_t * p )                        { return p->iObj;                                                          }
+static inline int          Wlc_NtkPiNum( Wlc_Ntk_t * p )                            { return Vec_IntSize(&p->vPis);                                            }
+static inline int          Wlc_NtkPoNum( Wlc_Ntk_t * p )                            { return Vec_IntSize(&p->vPos);                                            }
+static inline int          Wlc_NtkCiNum( Wlc_Ntk_t * p )                            { return Vec_IntSize(&p->vCis);                                            }
+static inline int          Wlc_NtkCoNum( Wlc_Ntk_t * p )                            { return Vec_IntSize(&p->vCos);                                            }
+static inline int          Wlc_NtkFfNum( Wlc_Ntk_t * p )                            { return Vec_IntSize(&p->vCis) - Vec_IntSize(&p->vPis);                    }
+
+static inline Wlc_Obj_t *  Wlc_NtkObj( Wlc_Ntk_t * p, int Id )                      { assert(Id > 0 && Id < p->nObjsAlloc); return p->pObjs + Id;              }
+static inline Wlc_Obj_t *  Wlc_NtkPi( Wlc_Ntk_t * p, int i )                        { return Wlc_NtkObj( p, Vec_IntEntry(&p->vPis, i) );                       }
+static inline Wlc_Obj_t *  Wlc_NtkPo( Wlc_Ntk_t * p, int i )                        { return Wlc_NtkObj( p, Vec_IntEntry(&p->vPos, i) );                       }
+static inline Wlc_Obj_t *  Wlc_NtkCi( Wlc_Ntk_t * p, int i )                        { return Wlc_NtkObj( p, Vec_IntEntry(&p->vCis, i) );                       }
+static inline Wlc_Obj_t *  Wlc_NtkCo( Wlc_Ntk_t * p, int i )                        { return Wlc_NtkObj( p, Vec_IntEntry(&p->vCos, i) );                       }
+static inline Wlc_Obj_t *  Wlc_NtkFf( Wlc_Ntk_t * p, int i )                        { return Wlc_NtkObj( p, Vec_IntEntry(&p->vFfs, i) );                       }
+
+static inline int          Wlc_ObjIsPi( Wlc_Obj_t * p )                             { return p->Type == WLC_OBJ_PI;                                            }
+static inline int          Wlc_ObjIsPo( Wlc_Obj_t * p )                             { return p->fIsPo;                                                         }
+static inline int          Wlc_ObjIsCi( Wlc_Obj_t * p )                             { return p->Type == WLC_OBJ_PI || p->Type == WLC_OBJ_FO;                   }
+static inline int          Wlc_ObjIsCo( Wlc_Obj_t * p )                             { return p->fIsPo || p->fIsFi;                                             }
+
+static inline int          Wlc_ObjId( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )             { return pObj - p->pObjs;                                                  }
+static inline int          Wlc_ObjCiId( Wlc_Obj_t * p )                             { assert( Wlc_ObjIsCi(p) ); return p->Fanins[1];                           }
+static inline int          Wlc_ObjFaninNum( Wlc_Obj_t * p )                         { return p->nFanins;                                                       }
+static inline int          Wlc_ObjHasArray( Wlc_Obj_t * p )                         { return p->nFanins > 2 || p->Type == WLC_OBJ_CONST;                       }
+static inline int *        Wlc_ObjFanins( Wlc_Obj_t * p )                           { return Wlc_ObjHasArray(p) ? p->pFanins[0] : p->Fanins;                   }
+static inline int          Wlc_ObjFaninId( Wlc_Obj_t * p, int i )                   { return Wlc_ObjFanins(p)[i];                                              }
+static inline int          Wlc_ObjFaninId0( Wlc_Obj_t * p )                         { return Wlc_ObjFanins(p)[0];                                              }
+static inline int          Wlc_ObjFaninId1( Wlc_Obj_t * p )                         { return Wlc_ObjFanins(p)[1];                                              }
+static inline int          Wlc_ObjFaninId2( Wlc_Obj_t * p )                         { return Wlc_ObjFanins(p)[2];                                              }
+static inline Wlc_Obj_t *  Wlc_ObjFanin( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int i )   { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, i) );                         }
+static inline Wlc_Obj_t *  Wlc_ObjFanin0( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )         { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 0) );                         }
+static inline Wlc_Obj_t *  Wlc_ObjFanin1( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )         { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 1) );                         }
+static inline Wlc_Obj_t *  Wlc_ObjFanin2( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )         { return Wlc_NtkObj( p, Wlc_ObjFaninId(pObj, 2) );                         }
+
+static inline int          Wlc_ObjRange( Wlc_Obj_t * p )                            { return p->End - p->Beg + 1;                                              }
+static inline int          Wlc_ObjRangeEnd( Wlc_Obj_t * p )                         { assert(p->Type == WLC_OBJ_BIT_SELECT); return p->Fanins[1] >> 16;        }
+static inline int          Wlc_ObjRangeBeg( Wlc_Obj_t * p )                         { assert(p->Type == WLC_OBJ_BIT_SELECT); return p->Fanins[1] & 0xFFFF;     }
+static inline int          Wlc_ObjIsSigned( Wlc_Obj_t * p )                         { return p->Signed;                                                        }
+static inline int          Wlc_ObjIsSignedFanin01( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ){ return Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed; }
+static inline int          Wlc_ObjSign( Wlc_Obj_t * p )                             { return Abc_Var2Lit( Wlc_ObjRange(p), Wlc_ObjIsSigned(p) );               }
+static inline int *        Wlc_ObjConstValue( Wlc_Obj_t * p )                       { assert(p->Type == WLC_OBJ_CONST);      return Wlc_ObjFanins(p);          }
+static inline int          Wlc_ObjTableId( Wlc_Obj_t * p )                          { assert(p->Type == WLC_OBJ_TABLE);      return p->Fanins[1];              }
+static inline word *       Wlc_ObjTable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )          { return (word *)Vec_PtrEntry( p->vTables, Wlc_ObjTableId(pObj) );         }
+
+static inline void         Wlc_NtkCleanCopy( Wlc_Ntk_t * p )                        { Vec_IntFill( &p->vCopies, p->nObjsAlloc, 0 );                            }
+static inline int          Wlc_NtkHasCopy( Wlc_Ntk_t * p )                          { return Vec_IntSize( &p->vCopies ) > 0;                                   }
+static inline void         Wlc_ObjSetCopy( Wlc_Ntk_t * p, int iObj, int i )         { Vec_IntWriteEntry( &p->vCopies, iObj, i );                               }
+static inline int          Wlc_ObjCopy( Wlc_Ntk_t * p, int iObj )                   { return Vec_IntEntry( &p->vCopies, iObj );                                }
+static inline Wlc_Obj_t *  Wlc_ObjCopyObj(Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj) {return Wlc_NtkObj(pNew, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)));   }
+
+static inline void         Wlc_NtkCleanNameId( Wlc_Ntk_t * p )                      { Vec_IntFill( &p->vNameIds, p->nObjsAlloc, 0 );                           }
+static inline int          Wlc_NtkHasNameId( Wlc_Ntk_t * p )                        { return Vec_IntSize( &p->vNameIds ) > 0;                                  }
+static inline void         Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i )       { Vec_IntWriteEntry( &p->vNameIds, iObj, i );                              }
+static inline int          Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj )                 { return Vec_IntEntry( &p->vNameIds, iObj );                               }
+
+static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )        { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkCoNum(p) - Wlc_NtkCiNum(p) + Wlc_ObjCiId(pObj)); } 
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -227,11 +228,18 @@ static inline Wlc_Obj_t *  Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== wlcAbs.c ========================================================*/
+extern int            Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
+extern Vec_Int_t *    Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
+extern Vec_Int_t *    Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
+extern Wlc_Ntk_t *    Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
+extern Wlc_Ntk_t *    Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
 /*=== wlcBlast.c ========================================================*/
 extern Gia_Man_t *    Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds );
 /*=== wlcNtk.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_NtkAlloc( char * pName, int nObjsAlloc );
 extern int            Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
+extern int            Wlc_ObjCreate( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg, Vec_Int_t * vFanins );
 extern void           Wlc_ObjSetCi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
 extern void           Wlc_ObjSetCo( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int fFlopInput );
 extern char *         Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
@@ -242,7 +250,6 @@ extern void           Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
 extern void           Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p );
 extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
-extern Vec_Int_t *    Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
 /*=== wlcReadWord.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadVer( char * pFileName );
 /*=== wlcWriteWord.c ========================================================*/
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
new file mode 100644
index 00000000..0ffb887d
--- /dev/null
+++ b/src/base/wlc/wlcAbs.c
@@ -0,0 +1,290 @@
+/**CFile****************************************************************
+
+  FileName    [wlcAbs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Verilog parser.]
+
+  Synopsis    [Abstraction for word-level networks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - August 22, 2014.]
+
+  Revision    [$Id: wlcAbs.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Check if two objects have the same input/output signatures.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )
+{
+    Wlc_Obj_t * pFanin, * pFanin2;  int k;
+    if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
+        return 0;
+    if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
+        return 0;
+    if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
+        return 0;
+    for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
+    {
+        pFanin = Wlc_ObjFanin(p, pObj, k);
+        pFanin2 = Wlc_ObjFanin(p, pObj2, k);
+        if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
+            return 0;
+        if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect IDs of the multipliers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+{
+    Wlc_Obj_t * pObj;  int i;
+    Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+    Wlc_NtkForEachObj( p, pObj, i )
+        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
+            Vec_IntPush( vBoxIds, i );
+    if ( Vec_IntSize( vBoxIds ) > 0 )
+        return vBoxIds;
+    Vec_IntFree( vBoxIds );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns all pairs of uifable multipliers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p )
+{
+    Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
+    Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
+    Wlc_Obj_t * pObj, * pObj2;  int i, k;
+    // iterate through unique pairs
+    Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
+        Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
+        {
+            if ( k == i )  
+                break;
+            if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
+            {
+                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
+                Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
+            }
+        }
+    Vec_IntFree( vMultis );
+    if ( Vec_IntSize( vPairs ) > 0 )
+        return vPairs;
+    Vec_IntFree( vPairs );
+    return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Abstracts nodes by replacing their outputs with new PIs.]
+
+  Description [If array is NULL, abstract all multipliers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
+{
+    Vec_Int_t * vNodes = vNodesInit;
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    int i, k, iObj, iFanin;
+    // get multipliers if not given
+    if ( vNodes == NULL )
+        vNodes = Wlc_NtkCollectMultipliers( p );
+    if ( vNodes == NULL )
+        return NULL;
+    // mark nodes
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
+        pObj->Mark = 1;
+    // iterate through the nodes in the DFS order
+    Wlc_NtkCleanCopy( p );
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Mark ) {
+            // clean
+            pObj->Mark = 0;
+            // add fresh PI with the same number of bits
+            iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
+        }
+        else {
+            // update fanins 
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+            // node to remain
+            iObj = i;
+        }
+        Wlc_ObjSetCopy( p, i, iObj );
+    }
+    // POs do not change in this procedure
+    if ( vNodes != vNodesInit )
+        Vec_IntFree( vNodes );
+    // reconstruct topological order
+    pNew = Wlc_NtkDupDfs( p );
+    Wlc_NtkTransferNames( pNew, p );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds UIF constraints to node pairs and updates POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
+{
+    Vec_Int_t * vPairs = vPairsInit;
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj, * pObj2;
+    Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
+    int i, k, iObj, iObj2, iObjNew, iObjNew2;
+    int iFanin, iFanin2, iFaninNew;
+    // get multiplier pairs if not given
+    if ( vPairs == NULL )
+        vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
+    if ( vPairs == NULL )
+        return NULL;
+    // sanity checks
+    assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
+    // iterate through node pairs
+    vFanins = Vec_IntAlloc( 100 );
+    vCompares = Vec_IntAlloc( 100 );
+    vUifConstrs = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
+    {
+        // get two nodes
+        pObj  = Wlc_NtkObj( p, iObj );
+        pObj2 = Wlc_NtkObj( p, iObj2 );
+        assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
+        // create fanin comparator nodes
+        Vec_IntClear( vCompares );
+        Wlc_ObjForEachFanin( pObj, iFanin, k )
+        {
+            iFanin2 = Wlc_ObjFaninId( pObj2, k );
+            Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
+            iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
+            Vec_IntPush( vCompares, iFaninNew );
+            // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
+            // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+            pObj = Wlc_NtkObj( p, iObj );
+        }
+        // concatenate fanin comparators
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
+        // create reduction-OR node
+        Vec_IntFill( vFanins, 1, iObjNew );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
+        // craete output comparator node
+        Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
+        iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
+        // create implication node (iObjNew is already complemented above)
+        Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
+        // save the constraint
+        Vec_IntPush( vUifConstrs, iObjNew );
+    }
+    // derive the AND of the UIF contraints
+    assert( Vec_IntSize(vUifConstrs) > 0 );
+    if ( Vec_IntSize(vUifConstrs) == 1 )
+        iObjNew = Vec_IntEntry( vUifConstrs, 0 );
+    else
+    {
+        // concatenate
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
+        // create reduction-AND node
+        Vec_IntFill( vFanins, 1, iObjNew );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
+    }
+    // update each PO to point to the new node
+    Wlc_NtkForEachPo( p, pObj, i )
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
+        iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
+        // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to 
+        // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+        pObj = Wlc_NtkObj( p, iObj );
+        // update PO/CO arrays
+        assert( Vec_IntEntry(&p->vPos, i) == iObj );
+        assert( Vec_IntEntry(&p->vCos, i) == iObj );
+        Vec_IntWriteEntry( &p->vPos, i, iObjNew );
+        Vec_IntWriteEntry( &p->vCos, i, iObjNew );
+        // transfer the PO attribute
+        Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
+        assert( pObj->fIsPo );
+        pObj->fIsPo = 0;
+    }
+    // cleanup
+    Vec_IntFree( vUifConstrs );
+    Vec_IntFree( vCompares );
+    Vec_IntFree( vFanins );
+    if ( vPairs != vPairsInit )
+        Vec_IntFree( vPairs );
+    // reconstruct topological order
+    pNew = Wlc_NtkDupDfs( p );
+    Wlc_NtkTransferNames( pNew, p );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 3aadedf2..39356be9 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -476,8 +476,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
             // bit-blast the multiplier in the external manager
             {
                 int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
-                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
-                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+                int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+                int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
                 Wlc_BlastMultiplier( pExtra, pArg0, pArg1, nRange, vTemp2, vRes );
                 Vec_IntShrink( vRes, nRange );
             }
@@ -557,24 +557,24 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
         else if ( pObj->Type == WLC_OBJ_BIT_AND )
         {
             int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
-            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
             for ( k = 0; k < nRange; k++ )
                 Vec_IntPush( vRes, Gia_ManHashAnd(pNew, pArg0[k], pArg1[k]) );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_OR )
         {
             int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
-            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
             for ( k = 0; k < nRange; k++ )
                 Vec_IntPush( vRes, Gia_ManHashOr(pNew, pArg0[k], pArg1[k]) );
         }
         else if ( pObj->Type == WLC_OBJ_BIT_XOR )
         {
             int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
-            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
             for ( k = 0; k < nRange; k++ )
                 Vec_IntPush( vRes, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) );
         }
@@ -637,8 +637,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
         else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU )
         {
             int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 );
-            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
             for ( k = 0; k < nRangeMax; k++ )
                 iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) ); 
             Vec_IntFill( vRes, 1, Abc_LitNotCond(iLit, pObj->Type == WLC_OBJ_COMP_EQU) );
@@ -649,7 +649,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
                   pObj->Type == WLC_OBJ_COMP_MORE || pObj->Type == WLC_OBJ_COMP_LESSEQU )
         {
             int nRangeMax = Abc_MaxInt( nRange0, nRange1 );
-            int fSigned = Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed;
+            int fSigned = Wlc_ObjIsSignedFanin01(p, pObj);
             int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
             int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
             int fSwap  = (pObj->Type == WLC_OBJ_COMP_MORE    || pObj->Type == WLC_OBJ_COMP_LESSEQU);
@@ -673,8 +673,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
         else if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ) 
         {
             int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
-            int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+            int * pArg0 = Wlc_VecLoadFanins( vRes,   pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
             if ( pObj->Type == WLC_OBJ_ARI_ADD )
                 Wlc_BlastAdder( pNew, pArg0, pArg1, nRange ); // result is in pFan0 (vRes)
             else 
@@ -684,15 +684,15 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
         else if ( pObj->Type == WLC_OBJ_ARI_MULTI )
         {
             int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
-            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
-            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed );
+            int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
+            int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, Wlc_ObjIsSignedFanin01(p, pObj) );
             Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRange, vTemp2, vRes );
             Vec_IntShrink( vRes, nRange );
         }
         else if ( pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_MODULUS )
         {
             int nRangeMax = Abc_MaxInt( nRange, Abc_MaxInt(nRange0, nRange1) );
-            int fSigned = Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed;
+            int fSigned = Wlc_ObjIsSignedFanin01(p, pObj);
             int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, fSigned );
             int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, fSigned );
             if ( fSigned )
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 5c786838..85e10511 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -32,6 +32,7 @@ static int  Abc_CommandReadVer  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandWriteVer ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandPs       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int  Abc_CommandBlast    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int  Abc_CommandTest     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )                       { return (Wlc_Ntk_t *)pAbc->pAbcWlc;                      }
 static inline void        Wlc_AbcFreeNtk( Abc_Frame_t * pAbc )                      { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc));  }
@@ -58,6 +59,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Word level", "%write_ver",  Abc_CommandWriteVer,  0 );
     Cmd_CommandAdd( pAbc, "Word level", "%ps",         Abc_CommandPs,        0 );
     Cmd_CommandAdd( pAbc, "Word level", "%blast",      Abc_CommandBlast,     0 );
+    Cmd_CommandAdd( pAbc, "Word level", "%test",       Abc_CommandTest,      0 );
 }
 
 /**Function********************************************************************
@@ -319,6 +321,53 @@ usage:
     return 1;
 }
 
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+    int c, fVerbose  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Abc_CommandBlast(): There is no current design.\n" );
+        return 0;
+    }
+    // transform
+//    pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+    pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+    Wlc_AbcUpdateNtk( pAbc, pNtk );
+    return 0;
+usage:
+    Abc_Print( -2, "usage: %%test [-vh]\n" );
+    Abc_Print( -2, "\t         experiments with word-level networks\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 9f779a2e..4b5ae8b7 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -111,8 +111,19 @@ void Wlc_ObjSetCi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
 {
     assert( Wlc_ObjIsCi(pObj) );
     assert( Wlc_ObjFaninNum(pObj) == 0 );
-    pObj->Fanins[1] = Vec_IntSize(&p->vCis);
-    Vec_IntPush( &p->vCis, Wlc_ObjId(p, pObj) );
+    if ( Wlc_NtkPiNum(p) == Wlc_NtkCiNum(p) || pObj->Type != WLC_OBJ_PI )
+    {
+        pObj->Fanins[1] = Vec_IntSize(&p->vCis);
+        Vec_IntPush( &p->vCis, Wlc_ObjId(p, pObj) );
+    }
+    else // insert in the array of CI at the end of PIs
+    {
+        Wlc_Obj_t * pTemp; int i;
+        Vec_IntInsert( &p->vCis, Wlc_NtkPiNum(p), Wlc_ObjId(p, pObj) );
+        // other CI IDs are invalidated... naive fix!
+        Wlc_NtkForEachCi( p, pTemp, i )
+            pTemp->Fanins[1] = i;
+    }
     if ( pObj->Type == WLC_OBJ_PI )
         Vec_IntPush( &p->vPis, Wlc_ObjId(p, pObj) );
 }
@@ -147,6 +158,12 @@ int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg )
     p->nObjs[Type]++;
     return p->iObj++;
 }
+int Wlc_ObjCreate( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg, Vec_Int_t * vFanins )
+{
+    int iFaninNew = Wlc_ObjAlloc( p, Type, Signed, End, Beg );
+    Wlc_ObjAddFanins( p, Wlc_NtkObj(p, iFaninNew), vFanins );
+    return iFaninNew;
+}
 char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj )
 {
     static char Buffer[100];
@@ -345,9 +362,9 @@ void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type )
             continue;
         printf( "%8d  :",      Counter++ );
         printf( "%8d  :  ",    i );
-        printf( "%3d%s = ",    Wlc_ObjRange(pObj),                   pObj->Signed ? "s" : " " );
-        printf( "%3d%s  %s ",  Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjFanin0(p, pObj)->Signed ? "s" : " ", Wlc_Names[Type] );
-        printf( "%3d%s ",      Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjFanin1(p, pObj)->Signed ? "s" : " " );
+        printf( "%3d%s = ",    Wlc_ObjRange(pObj),                   Wlc_ObjIsSigned(pObj) ? "s" : " " );
+        printf( "%3d%s  %s ",  Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[Type] );
+        printf( "%3d%s ",      Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
         printf( " :    " );
         printf( "%-12s =  ",   Wlc_ObjName(p, i) );
         printf( "%-12s  %s  ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_Names[Type] );
@@ -419,7 +436,7 @@ void Wlc_ObjCollectCopyFanins( Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
 int Wlc_ObjDup( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
 {
     Wlc_Obj_t * pObj = Wlc_NtkObj( p, iObj );
-    int iFaninNew = Wlc_ObjAlloc( pNew, pObj->Type, pObj->Signed, pObj->End, pObj->Beg );
+    int iFaninNew = Wlc_ObjAlloc( pNew, pObj->Type, Wlc_ObjIsSigned(pObj), pObj->End, pObj->Beg );
     Wlc_Obj_t * pObjNew = Wlc_NtkObj(pNew, iFaninNew);
     Wlc_ObjCollectCopyFanins( p, iObj, vFanins );
     Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
@@ -463,7 +480,7 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
     assert( pNew->pManName  == NULL && p->pManName != NULL );
     Wlc_NtkCleanNameId( pNew );
     for ( i = 0; i < p->nObjsAlloc; i++ )
-        if ( Wlc_ObjCopy(p, i) && Wlc_ObjNameId(p, i) )
+        if ( Wlc_ObjCopy(p, i) && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) )
             Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) );
     pNew->pManName = p->pManName; 
     p->pManName = NULL;
@@ -473,30 +490,6 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
     pNew->vTables = p->vTables;      p->vTables = NULL;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Collect IDs of the multipliers.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
-{
-    Wlc_Obj_t * pObj;  int i;
-    Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
-    Wlc_NtkForEachObj( p, pObj, i )
-        if ( pObj->Type == WLC_OBJ_ARI_MULTI )
-            Vec_IntPush( vBoxIds, i );
-    if ( Vec_IntSize( vBoxIds ) > 0 )
-        return vBoxIds;
-    Vec_IntFree( vBoxIds );
-    return NULL;
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 6000549f..ae72a2da 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -862,7 +862,7 @@ startword:
             p->pNtk->pMemTable = p->pMemTable; p->pMemTable = NULL;
             p->pNtk->vTables = p->vTables; p->vTables = NULL;
             // read the argument definitions
-            while ( (pName = Wlc_PrsStrtok( NULL, " (,)" )) )
+            while ( (pName = Wlc_PrsStrtok( NULL, "(,)" )) )
             {
                 pName = Wlc_PrsSkipSpaces( pName );
                 if ( Wlc_PrsStrCmp( pName, "input" ) || Wlc_PrsStrCmp( pName, "output" ) || Wlc_PrsStrCmp( pName, "wire" ) )
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index dbe3d219..aeb59e5d 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -87,7 +87,7 @@ void Wlc_WriteTables( FILE * pFile, Wlc_Ntk_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [This was used to add POs to each node except PIs and MUXes.]
 
   Description []
                
@@ -165,15 +165,13 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
             Wlc_ObjFanin1(p, pObj)->Mark = 1;
     Wlc_NtkForEachObj( p, pObj, i )
     {
-        char * pName  = Wlc_ObjName(p, i);
-        char * pName0 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL;
         int nDigits   = Abc_Base10Log(pObj->End+1) + Abc_Base10Log(pObj->Beg+1);
         if ( pObj->Mark ) 
         {
             pObj->Mark = 0;
             continue;
         }
-        sprintf( Range, "%s[%d:%d]%*s", pObj->Signed ? "signed ":"       ", pObj->End, pObj->Beg, 8-nDigits, "" );
+        sprintf( Range, "%s[%d:%d]%*s", Wlc_ObjIsSigned(pObj) ? "signed ":"       ", pObj->End, pObj->Beg, 8-nDigits, "" );
         fprintf( pFile, "  " );
         if ( pObj->Type == WLC_OBJ_PI )
             fprintf( pFile, "input  " );
@@ -183,7 +181,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
             fprintf( pFile, "       " );
         if ( Wlc_ObjIsCi(pObj) || pObj->fIsPo )
         {
-            fprintf( pFile, "wire %s %s ;\n", Range, pName );
+            fprintf( pFile, "wire %s %s ;\n", Range, Wlc_ObjName(p, i) );
             if ( Wlc_ObjIsCi(pObj) )
                 continue;
             Range[0] = 0;
@@ -197,11 +195,13 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         if ( pObj->Type == WLC_OBJ_TABLE )
         {
             // wire [3:0] s4972; table0 s4972_Index(s4971, s4972);
-            fprintf( pFile, "%s ;              table%d s%d_Index(%s, %s)", pName, Wlc_ObjTableId(pObj), i, pName0, pName );
+            fprintf( pFile, "%s ;              table%d", Wlc_ObjName(p, i), Wlc_ObjTableId(pObj), i );
+            fprintf( pFile, " s%d_Index(%s, ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
+            fprintf( pFile, "%s)",             Wlc_ObjName(p, i) );
         }
         else if ( pObj->Type == WLC_OBJ_CONST )
         {
-            fprintf( pFile, "%-16s = %d\'%sh", pName, Wlc_ObjRange(pObj), pObj->Signed ? "s":"" );
+            fprintf( pFile, "%-16s = %d\'%sh", Wlc_ObjName(p, i), Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" );
             Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pObj), (Wlc_ObjRange(pObj) + 3) / 4 );
         }
         else if ( pObj->Type == WLC_OBJ_ROTATE_R || pObj->Type == WLC_OBJ_ROTATE_L )
@@ -214,13 +214,13 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
             assert( Num0 > 0 && Num0 < Wlc_ObjRange(pObj) );
             fprintf( pFile, "%-16s = ", Wlc_ObjName(p, i) );
             if ( pObj->Type == WLC_OBJ_ROTATE_R )
-                fprintf( pFile, "(%s >> %d) | (%s << %d)", pName0, Num0, pName0, Num1 );
+                fprintf( pFile, "(%s >> %d) | (%s << %d)", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Num0, Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Num1 );
             else
-                fprintf( pFile, "(%s << %d) | (%s >> %d)", pName0, Num0, pName0, Num1 );
+                fprintf( pFile, "(%s << %d) | (%s >> %d)", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Num0, Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Num1 );
         }
         else if ( pObj->Type == WLC_OBJ_MUX && Wlc_ObjFaninNum(pObj) > 3 )
         {
-            fprintf( pFile, "%s ;\n", pName );
+            fprintf( pFile, "%s ;\n", Wlc_ObjName(p, i) );
             fprintf( pFile, "         " );
             fprintf( pFile, "always @( " );
             Wlc_ObjForEachFanin( pObj, iFanin, k )
@@ -234,7 +234,8 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
             {
                 if ( !k ) continue;
                 fprintf( pFile, "               " );
-                fprintf( pFile, "%d : %s = %s ;\n", k-1, pName, Wlc_ObjName(p, Wlc_ObjFaninId(pObj, k)) );
+                fprintf( pFile, "%d : %s = ", k-1, Wlc_ObjName(p, i) );
+                fprintf( pFile, "%s ;\n", Wlc_ObjName(p, Wlc_ObjFaninId(pObj, k)) );
             }
             fprintf( pFile, "             " );
             fprintf( pFile, "endcase\n" );
@@ -244,29 +245,33 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p )
         }
         else
         {
-            fprintf( pFile, "%-16s = ", pName );
+            fprintf( pFile, "%-16s = ", Wlc_ObjName(p, i) );
             if ( pObj->Type == WLC_OBJ_BUF )
-                fprintf( pFile, "%s", pName0 );
+                fprintf( pFile, "%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_MUX )
-                fprintf( pFile, "%s ? %s : %s", pName0, Wlc_ObjName(p, Wlc_ObjFaninId2(pObj)), Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
+            {
+                fprintf( pFile, "%s ? ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
+                fprintf( pFile, "%s : ", Wlc_ObjName(p, Wlc_ObjFaninId2(pObj)) );
+                fprintf( pFile, "%s",    Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
+            }
             else if ( pObj->Type == WLC_OBJ_ARI_MINUS )
-                fprintf( pFile, "-%s", pName0 );
+                fprintf( pFile, "-%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_BIT_NOT )
-                fprintf( pFile, "~%s", pName0 );
+                fprintf( pFile, "~%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_LOGIC_NOT )
-                fprintf( pFile, "!%s", pName0 );
+                fprintf( pFile, "!%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_REDUCT_AND )
-                fprintf( pFile, "&%s", pName0 );
+                fprintf( pFile, "&%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_REDUCT_OR )
-                fprintf( pFile, "|%s", pName0 );
+                fprintf( pFile, "|%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_REDUCT_XOR )
-                fprintf( pFile, "^%s", pName0 );
+                fprintf( pFile, "^%s", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_BIT_SELECT )
-                fprintf( pFile, "%s [%d:%d]", pName0, Wlc_ObjRangeEnd(pObj), Wlc_ObjRangeBeg(pObj) );
+                fprintf( pFile, "%s [%d:%d]", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_ObjRangeEnd(pObj), Wlc_ObjRangeBeg(pObj) );
             else if ( pObj->Type == WLC_OBJ_BIT_SIGNEXT )
-                fprintf( pFile, "{ {%d{%s[%d]}}, %s }", Wlc_ObjRange(pObj) - Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), pName0, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1, pName0 );
+                fprintf( pFile, "{ {%d{%s[%d]}}, %s }", Wlc_ObjRange(pObj) - Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1, Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_BIT_ZEROPAD )
-                fprintf( pFile, "{ {%d{1\'b0}}, %s }", Wlc_ObjRange(pObj) - Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), pName0 );
+                fprintf( pFile, "{ {%d{1\'b0}}, %s }", Wlc_ObjRange(pObj) - Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) );
             else if ( pObj->Type == WLC_OBJ_BIT_CONCAT )
             {
                 fprintf( pFile, "{" );
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index b56d8661..26c67073 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -551,6 +551,14 @@ static inline void Vec_IntFill( Vec_Int_t * p, int nSize, int Fill )
         p->pArray[i] = Fill;
     p->nSize = nSize;
 }
+static inline void Vec_IntFillTwo( Vec_Int_t * p, int nSize, int FillEven, int FillOdd )
+{
+    int i;
+    Vec_IntGrow( p, nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = (i & 1) ? FillOdd : FillEven;
+    p->nSize = nSize;
+}
 
 /**Function*************************************************************