Version abc50729

Makefile

+
+CC   := gcc
+CXX  := g++ 
+LD   := g++
+CP   := cp
+
+PROG := abc
+
+MODULES := src/base/abc src/base/cmd src/base/io src/base/main \
+           src/bdd/cudd src/bdd/epd src/bdd/mtr src/bdd/parse \
+           src/map/fpga src/map/mapper src/map/mio src/map/super \
+           src/misc/extra src/misc/st src/misc/util src/misc/vec \
+           src/sat/asat src/sat/fraig src/sat/msat \
+           src/seq \
+           src/sop/ft src/sop/mvc
+
+default: $(PROG)
+
+CFLAGS   += -Wall -Wno-unused-function -g -O $(patsubst %, -I%, $(MODULES)) 
+CXXFLAGS += $(CFLAGS) 
+
+LIBS := 
+SRC  := 
+GARBAGE := core core.* *.stackdump ./tags $(PROG)
+
+.PHONY: tags clean docs
+
+include $(patsubst %, %/module.make, $(MODULES))
+
+OBJ := \
+	$(patsubst %.cc, %.o, $(filter %.cc, $(SRC))) \
+	$(patsubst %.c, %.o,  $(filter %.c, $(SRC)))  \
+	$(patsubst %.y, %.o,  $(filter %.y, $(SRC))) 
+
+DEP := $(OBJ:.o=.d)
+
+# implicit rules
+
+%.d: %.c
+	./depends.sh $(CC) `dirname $*.c` $(CFLAGS) $*.c > $@
+
+%.d: %.cc
+	./depends.sh $(CXX) `dirname $*.cc` $(CXXFLAGS) $(CFLAGS) $*.cc > $@
+
+-include $(DEP)
+
+# Actual targets
+
+depend: $(DEP)
+
+clean: 
+	rm -rf $(PROG) $(OBJ) $(GARBAGE) $(OBJ:.o=.d) 
+
+tags:
+	ctags -R .
+
+$(PROG): $(OBJ)
+	$(LD) -o $@ $^ $(LIBS)
+
+docs:
+	doxygen doxygen.conf
+

abc.dsw

+Microsoft Developer Studio Workspace File, Format Version 6.00
+# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
+
+###############################################################################
+
+Project: "abc"=.\abc.dsp - Package Owner=<4>
+
+Package=<5>
+{{{
+}}}
+
+Package=<4>
+{{{
+}}}
+
+###############################################################################
+
+Global:
+
+Package=<5>
+{{{
+}}}
+
+Package=<3>
+{{{
+}}}
+
+###############################################################################
+

abc.rc

+alias b balance
+alias clp collapse
+alias f fraig
+alias fs fraig_sweep
+alias pf print_factor
+alias pfan print_fanio
+alias pio print_io
+alias ps print_stats 
+alias q quit
+alias r read
+alias rl read_blif
+alias rb read_bench
+alias rv read_verilog
+alias rsup read_super
+alias rlib read_library
+alias sa set autoexec ps
+alias so source -x
+alias st strash
+alias u undo
+alias wb write_blif
+alias wg write_gate
+alias wl write_blif
+alias cnf   "st; renode -c; write_cnf"
+alias prove "st; renode -c; sat"
+alias opt   "st; b; renode; sop; ps"
+alias opts  "st; b; renode; sop; st; b; ps"

depends.sh

+#!/bin/sh
+#echo "## Got: $*"
+CC="$1"
+DIR="$2"
+shift 2
+case "$DIR" in
+    "" | ".")
+    $CC -MM -MG "$@" | sed -e 's@^\(.*\)\.o:@\1.d \1.o:@'
+    ;;
+    *)
+    $CC -MM -MG "$@" | sed -e "s@^\(.*\)\.o:@$DIR/\1.d $DIR/\1.o:@"
+    ;;
+esac

src/base/abc/abcCollapse.c

+/**CFile****************************************************************
+
+  FileName    [abcCollapse.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Collapsing the network into two-levels.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcCollapse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk );
+static DdNode *    Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
+static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
+static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collapses the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew;
+    DdManager * dd;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // perform FPGA mapping
+    dd = Abc_NtkGlobalBdds( pNtk );    
+    if ( dd == NULL )
+        return NULL;
+    if ( fVerbose )
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+/*
+    {
+        Abc_Obj_t * pNode;
+        int i;
+        Abc_NtkForEachPo( pNtk, pNode, i )
+        {
+            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
+            pNode->pNext = NULL;
+        }
+        Abc_NtkForEachLatch( pNtk, pNode, i )
+        {
+            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
+            pNode->pNext = NULL;
+        }
+    }
+    Extra_StopManager( dd );
+    return NULL;
+*/
+
+    // transform the result of mapping into a BDD network
+    pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk );
+    if ( pNtkNew == NULL )
+    {
+        Cudd_Quit( dd );
+        return NULL;
+    }
+    Extra_StopManager( dd );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkCollapse: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives global BDDs for the node function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    DdNode * bFunc;
+    DdManager * dd;
+    int i;
+
+    // start the manager
+    dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+
+    // set the elementary variables
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; 
+    // assign the constant node BDD
+    pNode = Abc_AigConst1( pNtk->pManFunc );
+    pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
+
+    // construct the BDDs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+        if ( bFunc == NULL )
+        {
+            printf( "Constructing global BDDs timed out.\n" );
+            Extra_ProgressBarStop( pProgress );
+            Cudd_Quit( dd );
+            return NULL;
+        }
+        bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
+        pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // derefence the intermediate BDDs
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy ) 
+            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
+    Abc_NtkCleanCopy( pNtk );
+    // reorder one more time
+    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 0 );
+    return dd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the global BDD of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
+{
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( Cudd_ReadKeys(dd) > 500000 )
+        return NULL;
+    // if the result is available return
+    if ( pNode->pCopy )
+        return (DdNode *)pNode->pCopy;
+    // compute the result for both branches
+    bFunc0 = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); 
+    if ( bFunc0 == NULL )
+        return NULL;
+    Cudd_Ref( bFunc0 );
+    bFunc1 = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); 
+    if ( bFunc1 == NULL )
+        return NULL;
+    Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+    // get the final result
+    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // set the result
+    assert( pNode->pCopy == NULL );
+    pNode->pCopy = (Abc_Obj_t *)bFunc;
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network with the given global BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int i;
+    // start the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    // make sure the new manager has the same number of inputs
+    Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
+    // process the POs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+        // deref the BDD of the PO
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
+        pNode->pNext = NULL;
+    }
+    Extra_ProgressBarStop( pProgress );
+    // transfer the names
+    Abc_NtkDupNameArrays( pNtk, pNtkNew );
+    Abc_ManTimeDup( pNtk, pNtkNew );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network with the given global BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc )
+{
+    Abc_Obj_t * pNodeNew, * pTemp;
+    int i;
+    // create a new node
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    // add the fanins in the order, in which they appear in the reordered manager
+    Abc_NtkForEachCi( pNtkNew, pTemp, i )
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) );
+    // transfer the function
+    pNodeNew->pData = Extra_TransferLevelByLevel( dd, pNtkNew->pManFunc, bFunc );  Cudd_Ref( pNodeNew->pData );
+    return pNodeNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcDsd.c

+/**CFile****************************************************************
+
+  FileName    [abcDsd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Decomposes the network using disjoint-support decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Decomposes the network using disjoint-support decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcFanio.c

+/**CFile****************************************************************
+
+  FileName    [abcFanio.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Various procedures to connect fanins/fanouts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcFanio.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
+{
+    Abc_Obj_t * pFaninR = Abc_ObjRegular(pFanin);
+    assert( !Abc_ObjIsComplement(pObj) );
+    assert( pObj->pNtk == pFaninR->pNtk );
+    assert( pObj->Id >= 0 && pFaninR->Id >= 0 );
+    assert( pObj->Id    < (1<<21)-1 );  // created but forgot to add it to the network?
+    assert( pFaninR->Id < (1<<21)-1 );  // created but forgot to add it to the network?
+    Vec_FanPush( pObj->pNtk->pMmStep, &pObj->vFanins,     Vec_Int2Fan(pFaninR->Id) );
+    Vec_FanPush( pObj->pNtk->pMmStep, &pFaninR->vFanouts, Vec_Int2Fan(pObj->Id)   );
+    if ( Abc_ObjIsComplement(pFanin) )
+        Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Destroys fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
+{
+    assert( !Abc_ObjIsComplement(pObj) );
+    assert( !Abc_ObjIsComplement(pFanin) );
+    assert( pObj->pNtk == pFanin->pNtk );
+    assert( pObj->Id >= 0 && pFanin->Id >= 0 );
+    assert( pObj->Id   < (1<<21)-1 );  // created but forgot to add it to the network?
+    assert( pFanin->Id < (1<<21)-1 );  // created but forgot to add it to the network?
+    if ( !Vec_FanDeleteEntry( &pObj->vFanins, pFanin->Id ) )
+    {
+        printf( "The obj %d is not found among the fanins of obj %d ...\n", pFanin->Id, pObj->Id );
+        return;
+    }
+    if ( !Vec_FanDeleteEntry( &pFanin->vFanouts, pObj->Id ) )
+    {
+        printf( "The obj %d is not found among the fanouts of obj %d ...\n", pObj->Id, pFanin->Id );
+        return;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces a fanin of the node.]
+
+  Description [The node is pObj. An old fanin of this node (pFaninOld) has to be
+  replaced by a new fanin (pFaninNew). Assumes that the node and the old fanin 
+  are not complemented. The new fanin can be complemented. In this case, the
+  polarity of the new fanin will change, compared to the polarity of the old fanin.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew )
+{
+    Abc_Obj_t * pFaninNewR = Abc_ObjRegular(pFaninNew);
+    int iFanin, fCompl;
+    assert( !Abc_ObjIsComplement(pObj) );
+    assert( !Abc_ObjIsComplement(pFaninOld) );
+    assert( pFaninOld != pFaninNewR );
+    assert( pObj->pNtk == pFaninOld->pNtk );
+    assert( pObj->pNtk == pFaninNewR->pNtk );
+    if ( (iFanin = Vec_FanFindEntry( &pObj->vFanins, pFaninOld->Id )) == -1 )
+    {
+        printf( "Fanin node %d is not among the fanins of node %d...\n", pFaninOld->Id, pObj->Id );
+        return;
+    }
+    // remember the polarity of the old fanin
+    fCompl = Abc_ObjFaninC(pObj, iFanin);
+    // replace the old fanin entry by the new fanin entry (removes polarity)
+    Vec_FanWriteEntry( &pObj->vFanins, iFanin, Vec_Int2Fan(pFaninNewR->Id) );
+    // set the polarity of the new fanin
+    if ( fCompl ^ Abc_ObjIsComplement(pFaninNew) )
+        Abc_ObjSetFaninC( pObj, iFanin );
+    // update the fanout of the fanin
+    if ( !Vec_FanDeleteEntry( &pFaninOld->vFanouts, pObj->Id ) )
+    {
+        printf( "The node %d is not among the fanouts of its old fanin %d...\n", pObj->Id, pFaninOld->Id );
+        return;
+    }
+    Vec_FanPush( pObj->pNtk->pMmStep, &pFaninNewR->vFanouts, Vec_Int2Fan(pObj->Id) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers fanout from the old node to the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
+{
+    Vec_Ptr_t * vFanouts = pNodeFrom->pNtk->vPtrTemp;
+    int nFanoutsOld, i;
+    assert( !Abc_ObjIsComplement(pNodeFrom) );
+    assert( !Abc_ObjIsComplement(pNodeTo) );
+    assert( Abc_ObjIsNode(pNodeFrom) );
+    assert( Abc_ObjIsNode(pNodeTo) );
+    assert( pNodeFrom->pNtk == pNodeTo->pNtk );
+    assert( pNodeFrom != pNodeTo );
+    assert( Abc_ObjFanoutNum(pNodeFrom) > 0 );
+    // get the fanouts of the old node
+    nFanoutsOld = Abc_ObjFanoutNum(pNodeTo);
+    Abc_NodeCollectFanouts( pNodeFrom, vFanouts );
+    // patch the fanin of each of them
+    for ( i = 0; i < vFanouts->nSize; i++ )
+        Abc_ObjPatchFanin( vFanouts->pArray[i], pNodeFrom, pNodeTo );
+    assert( Abc_ObjFanoutNum(pNodeFrom) == 0 );
+    assert( Abc_ObjFanoutNum(pNodeTo) == nFanoutsOld + vFanouts->nSize );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces the node by a new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjReplace( Abc_Obj_t * pNodeOld, Abc_Obj_t * pNodeNew )
+{
+    assert( !Abc_ObjIsComplement(pNodeOld) );
+    assert( !Abc_ObjIsComplement(pNodeNew) );
+    assert( Abc_ObjIsNode(pNodeOld) );
+    assert( Abc_ObjIsNode(pNodeNew) );
+    assert( pNodeOld->pNtk == pNodeNew->pNtk );
+    assert( pNodeOld != pNodeNew );
+    assert( Abc_ObjFanoutNum(pNodeOld) > 0 );
+    assert( Abc_ObjFanoutNum(pNodeNew) == 0 );
+    // transfer the fanouts to the old node
+    Abc_ObjTransferFanout( pNodeOld, pNodeNew );
+    // remove the old node
+    Abc_NtkDeleteObj( pNodeOld );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcFpga.c

+/**CFile****************************************************************
+
+  FileName    [abcFpga.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcFpga.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fpgaInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose );
+static Abc_Ntk_t *  Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk );
+static Abc_Obj_t *  Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNodeFpga );
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the FPGA mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew;
+    Fpga_Man_t * pMan;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // print a warning about choice nodes
+    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+        printf( "Performing FPGA mapping with choices.\n" );
+
+    // perform FPGA mapping
+    pMan = Abc_NtkToFpga( pNtk, fRecovery, fVerbose );    
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Fpga_Mapping( pMan ) )
+    {
+        Fpga_ManFree( pMan );
+        return NULL;
+    }
+
+    // transform the result of mapping into a BDD network
+    pNtkNew = Abc_NtkFromFpga( pMan, pNtk );
+    if ( pNtkNew == NULL )
+        return NULL;
+    Fpga_ManFree( pMan );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkFpga: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Load the network into FPGA manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
+{
+    Fpga_Man_t * pMan;
+    ProgressBar * pProgress;
+    Fpga_Node_t * pNodeFpga;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode, * pFanin, * pPrev;
+    int i;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // start the mapping manager and set its parameters
+    pMan = Fpga_ManCreate( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk), Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk), fVerbose );
+    if ( pMan == NULL )
+        return NULL;
+    Fpga_ManSetAreaRecovery( pMan, fRecovery );
+    Fpga_ManSetOutputNames( pMan, (char **)pNtk->vNamesPo->pArray );
+    Fpga_ManSetInputArrivals( pMan, Abc_NtkGetCiArrivalFloats(pNtk) );
+
+    // create PIs and remember them in the old nodes
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)Fpga_ManReadInputs(pMan)[i];
+
+    // load the AIG into the mapper
+    vNodes = Abc_AigDfs( pNtk );
+    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+    for ( i = 0; i < vNodes->nSize; i++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        // consider the case of a constant
+        pNode = vNodes->pArray[i];
+        if ( Abc_NodeIsConst(pNode) )
+        {
+            Abc_AigConst1(pNtk->pManFunc)->pCopy = (Abc_Obj_t *)Fpga_ManReadConst1(pMan);
+            continue;
+        }
+        // add the node to the mapper
+        pNodeFpga = Fpga_NodeAnd( pMan, 
+            Fpga_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
+            Fpga_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
+        assert( pNode->pCopy == NULL );
+        // remember the node
+        pNode->pCopy = (Abc_Obj_t *)pNodeFpga;
+        // set up the choice node
+        if ( Abc_NodeIsChoice( pNode ) )
+            for ( pPrev = pNode, pFanin = pNode->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+            {
+                Fpga_NodeSetNextE( (Fpga_Node_t *)pPrev->pCopy, (Fpga_Node_t *)pFanin->pCopy );
+                Fpga_NodeSetRepr( (Fpga_Node_t *)pFanin->pCopy, (Fpga_Node_t *)pNode->pCopy );
+            }
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+
+    // set the primary outputs without copying the phase
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Fpga_ManReadOutputs(pMan)[i] = (Fpga_Node_t *)Abc_ObjFanin0(pNode)->pCopy;
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int i, nDupGates;
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    // make the mapper point to the new network
+    Fpga_CutsCleanSign( pMan );
+    Fpga_ManCleanData0( pMan );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy );
+    // set the constant node
+    if ( Abc_ObjFanoutNum( Abc_AigConst1(pNtk->pManFunc) ) > 0 )
+        Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) );
+    // process the nodes in topological order
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNodeNew = Abc_NodeFromFpga_rec( pNtkNew, Fpga_ManReadOutputs(pMan)[i] );
+        assert( !Abc_ObjIsComplement(pNodeNew) );
+        Abc_ObjFanin0(pNode)->pCopy = pNodeNew;
+    }
+    Extra_ProgressBarStop( pProgress );
+    // finalize the new network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    // decouple the PO driver nodes to reduce the number of levels
+    nDupGates = Abc_NtkLogicMakeSimplePos( pNtkNew );
+    if ( nDupGates && Fpga_ManReadVerbose(pMan) )
+        printf( "Duplicated %d gates to decouple the PO drivers.\n", nDupGates );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive one node after FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeFromFpga_rec( Abc_Ntk_t * pNtkNew, Fpga_Node_t * pNodeFpga )
+{
+    Fpga_Cut_t * pCutBest;
+    Fpga_Node_t ** ppLeaves; 
+    Abc_Obj_t * pNodeNew;
+    int i, nLeaves;
+    assert( !Fpga_IsComplement(pNodeFpga) );
+    // return if the result if known
+    pNodeNew = (Abc_Obj_t *)Fpga_NodeReadData0( pNodeFpga );
+    if ( pNodeNew )
+        return pNodeNew;
+    assert( Fpga_NodeIsAnd(pNodeFpga) );
+    // get the parameters of the best cut
+    pCutBest = Fpga_NodeReadCutBest( pNodeFpga );
+    ppLeaves = Fpga_CutReadLeaves( pCutBest );
+    nLeaves  = Fpga_CutReadLeavesNum( pCutBest ); 
+    // create a new node 
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    for ( i = 0; i < nLeaves; i++ )
+        Abc_ObjAddFanin( pNodeNew, Abc_NodeFromFpga_rec(pNtkNew, ppLeaves[i]) );
+    // derive the function of this node
+    pNodeNew->pData = Fpga_TruthsCutBdd( pNtkNew->pManFunc, pCutBest );   Cudd_Ref( pNodeNew->pData );
+    Fpga_NodeSetData0( pNodeFpga, (char *)pNodeNew );
+    return pNodeNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcInt.h

+/**CFile****************************************************************
+
+  FileName    [abcInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __ABC_INT_H__
+#define __ABC_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFITIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
+

src/base/abc/abcLatch.c

+/**CFile****************************************************************
+
+  FileName    [abcLatch.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures working with latches.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcLatch.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks whether the network is combinational.]
+
+  Description [The network is combinational if it has no latches.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkIsComb( Abc_Ntk_t * pNtk )
+{
+    return pNtk->vLatches->nSize == 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the network combinational.]
+
+  Description [If the network is sequential, the latches are disconnected,
+  while the latch inputs and outputs are added to the PIs and POs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch, * pNet;
+    int i;
+
+    if ( !Abc_NtkIsNetlist(pNtk) )
+        return 0;
+
+    // skip if the network is already combinational
+    if ( Abc_NtkIsComb( pNtk ) )
+        return 0;
+
+    // save the number of PIs/POs
+    assert( pNtk->nPisOld == 0 );
+    assert( pNtk->nPosOld == 0 );
+    pNtk->nPisOld = pNtk->vPis->nSize;
+    pNtk->nPosOld = pNtk->vPos->nSize;
+    if ( Abc_NtkIsNetlist(pNtk) )
+    {
+        // go through the latches
+        // - disconnect LO/LI nets from latches
+        // - add them to the PI/PO lists
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+        {
+            // process the input of the latch
+            pNet = Abc_ObjFanin0( pLatch );
+            assert( Abc_ObjIsLi( pNet ) );
+            if ( !Vec_FanDeleteEntry( &pNet->vFanouts, pLatch->Id ) )
+            {
+                printf( "Abc_NtkMakeComb: The latch is not found among the fanouts of the fanin net...\n" );
+                return 0;
+            }
+            if ( !Abc_ObjIsPo( pNet ) )
+                Abc_NtkMarkNetPo( pNet );
+
+            // process the output of the latch
+            pNet = Abc_ObjFanout0( pLatch );
+            assert( Abc_ObjIsLo( pNet ) );
+            if ( !Vec_FanDeleteEntry( &pNet->vFanins, pLatch->Id ) )
+            {
+                printf( "Abc_NtkMakeComb: The latch is not found among the fanins of the fanout net...\n" );
+                return 0;
+            }
+            assert( !Abc_ObjIsPi( pNet ) );
+            Abc_NtkMarkNetPi( pNet );
+        }
+    }
+    else
+    {
+        assert( 0 );
+/*
+        // go through the latches and add them to PIs and POs
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+        {
+//            pLatch->Type = ABC_OBJ_TYPE_NODE;
+            Vec_PtrPush( pNtk->vPis, pLatch );
+            Vec_PtrPush( pNtk->vPos, pLatch );
+            // add the names of the latches to the names of the PIs
+            Vec_PtrPush( pNtk->vNamesPi, pNtk->vNamesLatch->pArray[i] );
+        }
+*/
+    }
+    // save the latches in the backup place
+    pNtk->vLatches2 = pNtk->vLatches;
+    pNtk->vLatches  = Vec_PtrAlloc( 0 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes the network sequential again.]
+
+  Description [If the network was made combinational by disconnecting 
+  latches, this procedure makes it sequential again.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkMakeSeq( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch, * pNet;
+    int i;
+
+    if ( !Abc_NtkIsNetlist(pNtk) )
+        return 0;
+
+    // skip if the network has no latches
+    if ( pNtk->vLatches2 == NULL || pNtk->vLatches2->nSize == 0 )
+        return 0;
+    // move the latches from the backup place
+    Vec_PtrFree( pNtk->vLatches );
+    pNtk->vLatches = pNtk->vLatches2;
+    pNtk->vLatches2 = NULL;
+    if ( Abc_NtkIsNetlist(pNtk) )
+    {
+        // go through the latches and connect the LI/LO nets back to the latches
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+        {
+            // process the input of the latch
+            pNet = Abc_ObjFanin0( pLatch );
+            assert( Abc_ObjIsLi( pNet ) );
+            Vec_FanPush( pNtk->pMmStep, &pNet->vFanouts, Vec_Int2Fan(pLatch->Id) );
+            // process the output of the latch
+            pNet = Abc_ObjFanout0( pLatch );
+            assert( Abc_ObjIsLo( pNet ) );
+            Vec_FanPush( pNtk->pMmStep, &pNet->vFanins, Vec_Int2Fan(pLatch->Id) );
+        }
+        // clean the PI/PO attributes of the former latch variables
+        for ( i = pNtk->nPisOld; i < pNtk->vPis->nSize; i++ )
+            Abc_ObjUnsetSubtype( Abc_NtkPi(pNtk, i), ABC_OBJ_SUBTYPE_PI );
+        for ( i = pNtk->nPosOld; i < pNtk->vPos->nSize; i++ )
+            Abc_ObjUnsetSubtype( Abc_NtkPo(pNtk, i), ABC_OBJ_SUBTYPE_PO );
+    }
+    else
+    {
+        assert( 0 );
+//        Vec_PtrShrink( pNtk->vNamesPi, pNtk->nPisOld );
+    }
+    // remove the nodes from the PI/PO lists
+    Vec_PtrShrink( pNtk->vPis, pNtk->nPisOld );
+    Vec_PtrShrink( pNtk->vPos, pNtk->nPosOld );
+    pNtk->nPis = pNtk->vPis->nSize;
+    pNtk->nPos = pNtk->vPos->nSize;
+    pNtk->nPisOld = 0;
+    pNtk->nPosOld = 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if latches form self-loop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkLatchIsSelfFeed_rec( Abc_Obj_t * pLatch, Abc_Obj_t * pLatchRoot )
+{
+    Abc_Obj_t * pFanin;
+    assert( Abc_ObjIsLatch(pLatch) );
+    if ( pLatch == pLatchRoot )
+        return 1;
+    pFanin = Abc_ObjFanin0(pLatch);
+    if ( !Abc_ObjIsLatch(pFanin) )
+        return 0;
+    return Abc_NtkLatchIsSelfFeed_rec( pFanin, pLatch );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if latches form self-loop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch )
+{
+    Abc_Obj_t * pFanin;
+    assert( Abc_ObjIsLatch(pLatch) );
+    pFanin = Abc_ObjFanin0(pLatch);
+    if ( !Abc_ObjIsLatch(pFanin) )
+        return 0;
+    return Abc_NtkLatchIsSelfFeed_rec( pFanin, pLatch );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if latches form self-loop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i, Counter;
+    Counter = 0;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Counter += Abc_NtkLatchIsSelfFeed( pLatch );
+    return Counter;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcMinBase.c

+/**CFile****************************************************************
+
+  FileName    [abcMinBase.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Makes nodes of the network minimum base.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcMinBase.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Makes nodes minimum base.]
+
+  Description [Returns the number of changed nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, Counter;
+    assert( Abc_NtkIsLogicBdd(pNtk) );
+    Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Counter += Abc_NodeMinimumBase( pNode );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Makes one node minimum base.]
+
+  Description [Returns 1 if the node is changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
+{
+    Vec_Str_t * vSupport = pNode->pNtk->vStrTemp;
+    Vec_Ptr_t * vFanins = pNode->pNtk->vPtrTemp;
+    DdNode * bTemp;
+    int i, nVars;
+
+    assert( Abc_NtkIsLogicBdd(pNode->pNtk) );
+    assert( Abc_ObjIsNode(pNode) );
+
+    // compute support
+    nVars = Abc_NodeSupport( Cudd_Regular(pNode->pData), vSupport, Abc_ObjFaninNum(pNode) );
+    if ( nVars == Abc_ObjFaninNum(pNode) )
+        return 0;
+
+    // remove unused fanins
+    Abc_NodeCollectFanins( pNode, vFanins );
+    for ( i = 0; i < vFanins->nSize; i++ )
+        if ( vSupport->pArray[i] == 0 )
+            Abc_ObjDeleteFanin( pNode, vFanins->pArray[i] );
+    assert( nVars == Abc_ObjFaninNum(pNode) );
+
+    // update the function of the node
+    pNode->pData = Extra_bddRemapUp( pNode->pNtk->pManFunc, bTemp = pNode->pData );   Cudd_Ref( pNode->pData );
+    Cudd_RecursiveDeref( pNode->pNtk->pManFunc, bTemp );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes support of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSupport_rec( DdNode * bFunc, Vec_Str_t * vSupport )
+{
+    if ( cuddIsConstant(bFunc) || Cudd_IsComplement(bFunc->next) )
+        return;
+    vSupport->pArray[ bFunc->index ] = 1;
+    Abc_NodeSupport_rec( cuddT(bFunc), vSupport );
+    Abc_NodeSupport_rec( Cudd_Regular(cuddE(bFunc)), vSupport );
+    bFunc->next = Cudd_Not(bFunc->next);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes support of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSupportClear_rec( DdNode * bFunc )
+{
+    if ( !Cudd_IsComplement(bFunc->next) )
+        return;
+    bFunc->next = Cudd_Regular(bFunc->next);
+    if ( cuddIsConstant(bFunc) )
+        return;
+    Abc_NodeSupportClear_rec( cuddT(bFunc) );
+    Abc_NodeSupportClear_rec( Cudd_Regular(cuddE(bFunc)) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes support of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars )
+{
+    int Counter, i;
+    // compute the support by marking the BDD
+    Vec_StrFill( vSupport, nVars, 0 );
+    Abc_NodeSupport_rec( bFunc, vSupport );
+    // clear the marak
+    Abc_NodeSupportClear_rec( bFunc );
+    // get the number of support variables
+    Counter = 0;
+    for ( i = 0; i < nVars; i++ )
+        Counter += vSupport->pArray[i];
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcNetlist.c

+/**CFile****************************************************************
+
+  FileName    [abcNetlist.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Transforms netlist into a logic network and vice versa.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcNetlist.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transform the netlist into a logic network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkLogic( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC_SOP );
+    // duplicate the name and the spec
+    pNtkNew->pName = util_strsav(pNtk->pName);
+    pNtkNew->pSpec = util_strsav(pNtk->pSpec);
+    // clean the copy field
+    Abc_NtkCleanCopy( pNtk );
+    // create the PIs and point to them from the nets
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkCreateTermPi( pNtkNew );
+    // create the latches and point to them from the latch fanout nets
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj);
+    // duplicate the nodes and point to them from the fanout nets
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj);
+    // reconnect the internal nodes in the new network
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+    // create and connect the POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), Abc_ObjFanin0(pObj)->pCopy );
+    // connect the latches
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+    // add the latches to the PI/PO arrays to make them look at CIs/COs
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Vec_PtrPush( pNtkNew->vPis, pObj->pCopy );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Vec_PtrPush( pNtkNew->vPos, pObj->pCopy );
+    // transfer the names
+    Abc_NtkCreateNameArrays( pNtk, pNtkNew );
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkLogic( pNtk->pExdc );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkLogic(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcPrint.c

+/**CFile****************************************************************
+
+  FileName    [abcPrint.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Printing statistics.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcPrint.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "ft.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Print the vital stats of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    fprintf( pFile, "%-15s:",       pNtk->pName );
+    fprintf( pFile, "  i/o = %3d/%3d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
+    fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
+
+    if ( Abc_NtkIsNetlist(pNtk) )
+    {
+        fprintf( pFile, "  net = %5d", Abc_NtkNetNum(pNtk) );
+        fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
+    }
+    else if ( Abc_NtkIsAig(pNtk) )
+        fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
+    else 
+        fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
+
+    if ( Abc_NtkIsLogicSop(pNtk) )   
+    {
+        fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
+//        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
+        fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
+    }
+    else if ( Abc_NtkIsLogicBdd(pNtk) )
+        fprintf( pFile, "  bdd = %5d",  Abc_NtkGetBddNodeNum(pNtk) );
+    else if ( Abc_NtkIsLogicMap(pNtk) )
+    {
+        fprintf( pFile, "  area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
+        fprintf( pFile, "  delay = %5.2f", Abc_NtkDelayTrace(pNtk) );
+    }
+    fprintf( pFile, "  lev = %2d", Abc_NtkGetLevelNum(pNtk) );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints PIs/POs and LIs/LOs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNet, * pLatch;
+    int i;
+
+    if ( Abc_NtkIsNetlist(pNtk) )
+    {
+        fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );    
+        Abc_NtkForEachPi( pNtk, pNet, i )
+            fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        fprintf( pFile, "\n" );   
+    
+        fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );    
+        Abc_NtkForEachPo( pNtk, pNet, i )
+            fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        fprintf( pFile, "\n" );    
+  
+        fprintf( pFile, "Latches (%d):  ", Abc_NtkLatchNum(pNtk) );  
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+            fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, "\n" );   
+    }
+    else
+    {
+        fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );    
+        Abc_NtkForEachPi( pNtk, pNet, i )
+            fprintf( pFile, " %s", pNtk->vNamesPi->pArray[i] );
+        fprintf( pFile, "\n" );   
+    
+        fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );    
+        Abc_NtkForEachPo( pNtk, pNet, i )
+            fprintf( pFile, " %s", pNtk->vNamesPo->pArray[i] );
+        fprintf( pFile, "\n" );    
+  
+        fprintf( pFile, "Latches (%d):  ", Abc_NtkLatchNum(pNtk) );  
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+            fprintf( pFile, " %s", pNtk->vNamesLatch->pArray[i] );
+        fprintf( pFile, "\n" );   
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the distribution of fanins/fanouts in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, k, nFanins, nFanouts;
+    Vec_Int_t * vFanins, * vFanouts;
+    int nOldSize, nNewSize;
+
+    vFanins  = Vec_IntAlloc( 0 );
+    vFanouts = Vec_IntAlloc( 0 );
+    Vec_IntFill( vFanins,  100, 0 );
+    Vec_IntFill( vFanouts, 100, 0 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Abc_ObjFaninNum(pNode);
+        if ( Abc_NtkIsNetlist(pNtk) )
+            nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
+        else
+            nFanouts = Abc_ObjFanoutNum(pNode);
+        if ( nFanins > vFanins->nSize || nFanouts > vFanouts->nSize )
+        {
+            nOldSize = vFanins->nSize;
+            nNewSize = ABC_MAX(nFanins, nFanouts) + 10;
+            Vec_IntGrow( vFanins,  nNewSize  );
+            Vec_IntGrow( vFanouts, nNewSize );
+            for ( k = nOldSize; k < nNewSize; k++ )
+            {
+                Vec_IntPush( vFanins,  0  );
+                Vec_IntPush( vFanouts, 0 );
+            }
+        }
+        vFanins->pArray[nFanins]++;
+        vFanouts->pArray[nFanouts]++;
+    }
+    fprintf( pFile, "The distribution of fanins and fanouts in the network:\n" );
+    fprintf( pFile, "  Number   Nodes with fanin  Nodes with fanout\n" );
+    for ( k = 0; k < vFanins->nSize; k++ )
+    {
+        if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 )
+            continue;
+        fprintf( pFile, "%5d : ", k );
+        if ( vFanins->pArray[k] == 0 )
+            fprintf( pFile, "              " );
+        else
+            fprintf( pFile, "%12d  ", vFanins->pArray[k] );
+        fprintf( pFile, "    " );
+        if ( vFanouts->pArray[k] == 0 )
+            fprintf( pFile, "              " );
+        else
+            fprintf( pFile, "%12d  ", vFanouts->pArray[k] );
+        fprintf( pFile, "\n" );
+    }
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vFanouts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the fanins/fanouts of a node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pNode2;
+    int i;
+    if ( Abc_ObjIsPo(pNode) )
+        pNode = Abc_ObjFanin0(pNode);
+
+    fprintf( pFile, "Fanins (%d): ", Abc_ObjFaninNum(pNode) );    
+    Abc_ObjForEachFanin( pNode, pNode2, i )
+    {
+        pNode2->pCopy = NULL;
+        fprintf( pFile, " %s", Abc_ObjName(pNode2) );
+    }
+    fprintf( pFile, "\n" ); 
+    
+    fprintf( pFile, "\n" );    
+    fprintf( pFile, "Fanouts (%d): ", Abc_ObjFaninNum(pNode) );    
+    Abc_ObjForEachFanout( pNode, pNode2, i )
+    {
+        pNode2->pCopy = NULL;
+        fprintf( pFile, " %s", Abc_ObjName(pNode2) );
+    }
+    fprintf( pFile, "\n" );   
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the factored form of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    assert( Abc_NtkIsNetlist(pNtk) || Abc_NtkIsLogicSop(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Abc_NodePrintFactor( pFile, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the factored form of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
+{
+    Vec_Int_t * vFactor;
+    if ( Abc_ObjIsPo(pNode) )
+        pNode = Abc_ObjFanin0(pNode);
+    if ( Abc_ObjIsPi(pNode) )
+    {
+        printf( "Skipping the PI node.\n" );
+        return;
+    }
+    if ( Abc_ObjIsLatch(pNode) )
+    {
+        printf( "Skipping the latch.\n" );
+        return;
+    }
+    assert( Abc_ObjIsNode(pNode) );
+    vFactor = Ft_Factor( pNode->pData );
+    pNode->pCopy = NULL;
+    Ft_FactorPrint( stdout, vFactor, NULL, Abc_ObjName(pNode) );
+    Vec_IntFree( vFactor );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcRefs.c

+/**CFile****************************************************************
+
+  FileName    [abcRefs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Reference counting of the nodes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRefs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure returns the size of the MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMffcSize( Abc_Obj_t * pNode )
+{
+    int nConeSize1, nConeSize2;
+    assert( !Abc_ObjIsComplement( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) );
+    nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0 ); // dereference
+    nConeSize2 = Abc_NodeRefDeref( pNode, 0, 1 ); // reference
+    assert( nConeSize1 == nConeSize2 );
+    assert( nConeSize1 > 0 );
+    return nConeSize1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure returns the size of the MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeMffcRemove( Abc_Obj_t * pNode )
+{
+    assert( !Abc_ObjIsComplement( pNode ) );
+    assert( Abc_ObjIsNode( pNode ) );
+    return Abc_NodeRefDeref( pNode, 1, 0 ); // dereference
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References/references the node and returns MFFC size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference )
+{
+    Abc_Obj_t * pNode0, * pNode1;
+    int Counter;
+    if ( Abc_ObjIsPi(pNode) || Abc_ObjIsLatch(pNode) )
+        return 0;
+    pNode0 = Abc_ObjFanin( pNode, 0 );
+    pNode1 = Abc_ObjFanin( pNode, 1 );
+    Counter = 1;
+    if ( fReference )
+    {
+        if ( pNode0->vFanouts.nSize++ == 0 )
+        {
+            Counter += Abc_NodeRefDeref( pNode0, fFanouts, fReference );
+            if ( fFanouts )  
+                Abc_ObjAddFanin( pNode, pNode0 );
+        }
+        if ( pNode1->vFanouts.nSize++ == 0 )
+        {
+            Counter += Abc_NodeRefDeref( pNode1, fFanouts, fReference );
+            if ( fFanouts )  
+                Abc_ObjAddFanin( pNode, pNode1 );
+        }
+    }
+    else
+    {
+        assert( pNode0->vFanouts.nSize > 0 );
+        assert( pNode1->vFanouts.nSize > 0 );
+        if ( --pNode0->vFanouts.nSize == 0 )
+        {
+            Counter += Abc_NodeRefDeref( pNode0, fFanouts, fReference );
+            if ( fFanouts )  
+                Abc_ObjDeleteFanin( pNode, pNode0 );
+        }
+        if ( --pNode1->vFanouts.nSize == 0 )
+        {
+            Counter += Abc_NodeRefDeref( pNode1, fFanouts, fReference );
+            if ( fFanouts )  
+                Abc_ObjDeleteFanin( pNode, pNode1 );
+        }
+    }
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcSat.c

+/**CFile****************************************************************
+
+  FileName    [abcSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures to solve the miter using the internal SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Attempts to solve the miter using an internal SAT solver.]
+
+  Description [Returns 1 if the miter is SAT.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    solver * pSat;
+    lbool   status;
+    int clk;
+
+    assert( Abc_NtkIsLogicBdd(pNtk) );
+    assert( Abc_NtkLatchNum(pNtk) == 0 );
+
+    if ( Abc_NtkPoNum(pNtk) > 1 )
+        fprintf( stdout, "Warning: The miter has more than 1 output. SAT will try to prove all of them.\n" );
+
+    // load clauses into the solver
+    clk = clock();
+    pSat = Abc_NtkMiterSatCreate( pNtk );
+//    printf( "Created SAT problem with %d variable and %d clauses.   ", 
+//        solver_nvars(pSat), solver_nclauses(pSat) );
+//    PRT( "Time", clock() - clk );
+
+    // simplify the problem
+    clk = clock();
+    status = solver_simplify(pSat);
+//    printf( "Simplified the problem to %d variables and %d clauses. ", 
+//        solver_nvars(pSat), solver_nclauses(pSat) );
+//    PRT( "Time", clock() - clk );
+    if ( status == l_False )
+    {
+        solver_delete( pSat );
+        printf( "The problem is UNSAT after simplification.\n" );
+        return 0;
+    }
+
+    // solve the miter
+    clk = clock();
+    if ( fVerbose )
+        pSat->verbosity = 1;
+    status = solver_solve( pSat, NULL, NULL );
+//    if ( fVerbose )
+//    {
+    printf( "The problem is %5s. ", (status == l_True)? "SAT" : "UNSAT" );
+    PRT( "SAT solver time", clock() - clk );
+//    }
+    // free the solver
+    solver_delete( pSat );
+    return status == l_True;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
+{
+    solver * pSat;
+    Extra_MmFlex_t * pMmFlex;
+    Abc_Obj_t * pNode;
+    Vec_Str_t * vCube;
+    Vec_Int_t * vVars;
+    char * pSop0, * pSop1;
+    int i;
+
+    assert( Abc_NtkIsLogicBdd(pNtk) );
+
+    // start the data structures
+    pSat    = solver_new();
+    pMmFlex = Extra_MmFlexStart();
+    vCube   = Vec_StrAlloc( 100 );
+    vVars   = Vec_IntAlloc( 100 );
+
+    // add clauses for each internal nodes
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // derive SOPs for both phases of the node
+        Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
+        // add the clauses to the solver
+        Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
+    }
+    // add clauses for each PO
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        Abc_NodeAddClausesTop( pSat, pNode, vVars );
+
+    // delete
+    Vec_StrFree( vCube );
+    Vec_IntFree( vVars );
+    Extra_MmFlexStop( pMmFlex, 0 );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses for the internal node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+{
+    Abc_Obj_t * pFanin;
+    int i, c, nFanins;
+    char * pCube;
+
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
+ 
+    // add clauses for the negative phase
+    for ( c = 0; ; c++ )
+    {
+        // get the cube
+        pCube = pSop0 + c * (nFanins + 3);
+        if ( *pCube == 0 )
+            break;
+        // add the clause
+        vVars->nSize = 0;
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            if ( pCube[i] == '0' )
+                Vec_IntPush( vVars, toLit(pFanin->Id) );
+            else if ( pCube[i] == '1' )
+                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        }
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    }
+
+    // add clauses for the positive phase
+    for ( c = 0; ; c++ )
+    {
+        // get the cube
+        pCube = pSop1 + c * (nFanins + 3);
+        if ( *pCube == 0 )
+            break;
+        // add the clause
+        vVars->nSize = 0;
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            if ( pCube[i] == '0' )
+                Vec_IntPush( vVars, toLit(pFanin->Id) );
+            else if ( pCube[i] == '1' )
+                Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        }
+        Vec_IntPush( vVars, toLit(pNode->Id) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds clauses for the PO node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+{
+    Abc_Obj_t * pFanin;
+
+    pFanin = Abc_ObjFanin0(pNode);
+    if ( Abc_ObjFaninC0(pNode) )
+    {
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, toLit(pFanin->Id) );
+        Vec_IntPush( vVars, toLit(pNode->Id) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    }
+    else
+    {
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
+        Vec_IntPush( vVars, toLit(pNode->Id) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+
+        vVars->nSize = 0;
+        Vec_IntPush( vVars, toLit(pFanin->Id) );
+        Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+        solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+    }
+
+    vVars->nSize = 0;
+    Vec_IntPush( vVars, toLit(pNode->Id) );
+    solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcVerify.c

+/**CFile****************************************************************
+
+  FileName    [abcVerify.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Combinational and sequential verification for two networks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcVerify.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies combinational equivalence by brute-force SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    Abc_Ntk_t * pMiter;
+    Abc_Ntk_t * pCnf;
+    int RetValue;
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are not equivalent.\n" );
+        return;
+    }
+    if ( RetValue == 0 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are equivalent after structural hashing.\n" );
+        return;
+    }
+
+    // convert the miter into a CNF
+    pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0 );
+    Abc_NtkDelete( pMiter );
+    if ( pCnf == NULL )
+    {
+        printf( "Renoding for CNF has failed.\n" );
+        return;
+    }
+
+    // solve the CNF using the SAT solver
+    if ( Abc_NtkMiterSat( pCnf, 0 ) )
+        printf( "Networks are not equivalent.\n" );
+    else
+        printf( "Networks are equivalent.\n" );
+    Abc_NtkDelete( pCnf );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies sequential equivalence by fraiging followed by SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pMiter;
+    Abc_Ntk_t * pFraig;
+    int RetValue;
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are not equivalent.\n" );
+        return;
+    }
+    if ( RetValue == 0 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are equivalent after structural hashing.\n" );
+        return;
+    }
+
+    // convert the miter into a FRAIG
+    Fraig_ParamsSetDefault( &Params );
+    pFraig = Abc_NtkFraig( pMiter, &Params, 0 );
+    Abc_NtkDelete( pMiter );
+    if ( pFraig == NULL )
+    {
+        printf( "Fraiging has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pFraig );
+    Abc_NtkDelete( pFraig );
+    if ( RetValue == 0 )
+    {
+        printf( "Networks are equivalent after fraiging.\n" );
+        return;
+    }
+    printf( "Networks are not equivalent.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies sequential equivalence by brute-force SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
+{
+    Abc_Ntk_t * pMiter;
+    Abc_Ntk_t * pFrames;
+    Abc_Ntk_t * pCnf;
+    int RetValue;
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are not equivalent.\n" );
+        return;
+    }
+    if ( RetValue == 0 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are equivalent after structural hashing.\n" );
+        return;
+    }
+
+    // create the timeframes
+    pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
+    Abc_NtkDelete( pMiter );
+    if ( pFrames == NULL )
+    {
+        printf( "Frames computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pFrames );
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pFrames );
+        printf( "Networks are not equivalent.\n" );
+        return;
+    }
+    if ( RetValue == 0 )
+    {
+        Abc_NtkDelete( pFrames );
+        printf( "Networks are equivalent after framing.\n" );
+        return;
+    }
+
+    // convert the miter into a CNF
+    pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0 );
+    Abc_NtkDelete( pFrames );
+    if ( pCnf == NULL )
+    {
+        printf( "Renoding for CNF has failed.\n" );
+        return;
+    }
+
+    // solve the CNF using the SAT solver
+    if ( Abc_NtkMiterSat( pCnf, 0 ) )
+        printf( "Networks are not equivalent.\n" );
+    else
+        printf( "Networks are equivalent.\n" );
+    Abc_NtkDelete( pCnf );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies combinational equivalence by fraiging followed by SAT]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames )
+{
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pMiter;
+    Abc_Ntk_t * pFraig;
+    Abc_Ntk_t * pFrames;
+    int RetValue;
+
+    // get the miter of the two networks
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 );
+    if ( pMiter == NULL )
+    {
+        printf( "Miter computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pMiter );
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are not equivalent.\n" );
+        return;
+    }
+    if ( RetValue == 0 )
+    {
+        Abc_NtkDelete( pMiter );
+        printf( "Networks are equivalent after structural hashing.\n" );
+        return;
+    }
+
+    // create the timeframes
+    pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
+    Abc_NtkDelete( pMiter );
+    if ( pFrames == NULL )
+    {
+        printf( "Frames computation has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pFrames );
+    if ( RetValue == 1 )
+    {
+        Abc_NtkDelete( pFrames );
+        printf( "Networks are not equivalent.\n" );
+        return;
+    }
+    if ( RetValue == 0 )
+    {
+        Abc_NtkDelete( pFrames );
+        printf( "Networks are equivalent after framing.\n" );
+        return;
+    }
+
+    // convert the miter into a FRAIG
+    Fraig_ParamsSetDefault( &Params );
+    pFraig = Abc_NtkFraig( pMiter, &Params, 0 );
+    Abc_NtkDelete( pFrames );
+    if ( pFraig == NULL )
+    {
+        printf( "Fraiging has failed.\n" );
+        return;
+    }
+    RetValue = Abc_NtkMiterIsConstant( pFraig );
+    Abc_NtkDelete( pFraig );
+    if ( RetValue == 0 )
+    {
+        printf( "Networks are equivalent after fraiging.\n" );
+        return;
+    }
+    printf( "Networks are not equivalent.\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/module.make

+SRC +=    src/base/abc/abc.c \
+    src/base/abc/abcAig.c \
+    src/base/abc/abcAttach.c \
+    src/base/abc/abcCheck.c \
+    src/base/abc/abcCollapse.c \
+    src/base/abc/abcCreate.c \
+    src/base/abc/abcDfs.c \
+    src/base/abc/abcDsd.c \
+    src/base/abc/abcFanio.c \
+    src/base/abc/abcFpga.c \
+    src/base/abc/abcFraig.c \
+    src/base/abc/abcFunc.c \
+    src/base/abc/abcLatch.c \
+    src/base/abc/abcMap.c \
+    src/base/abc/abcMinBase.c \
+    src/base/abc/abcMiter.c \
+    src/base/abc/abcNames.c \
+    src/base/abc/abcNetlist.c \
+    src/base/abc/abcPrint.c \
+    src/base/abc/abcRefs.c \
+    src/base/abc/abcRenode.c \
+    src/base/abc/abcSat.c \
+    src/base/abc/abcSop.c \
+    src/base/abc/abcStrash.c \
+    src/base/abc/abcSweep.c \
+    src/base/abc/abcTiming.c \
+    src/base/abc/abcUtil.c \
+    src/base/abc/abcVerify.c 

src/base/cmd/cmd.h

+/**CFile****************************************************************
+
+  FileName    [cmd.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [External declarations of the command package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cmd.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CMD_H__
+#define __CMD_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct MvCommand    Abc_Command;  // one command
+typedef struct MvAlias      Abc_Alias;    // one alias
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFITIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cmd.c ===========================================================*/
+extern void        Cmd_Init();
+extern void        Cmd_End();
+/*=== cmdApi.c ========================================================*/
+extern void        Cmd_CommandAdd( Abc_Frame_t * pAbc, char * sGroup, char * sName, void * pFunc, int fChanges );
+extern int         Cmd_CommandExecute( Abc_Frame_t * pAbc, char * sCommand );
+/*=== cmdFlag.c ========================================================*/
+extern char *      Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag );
+extern void        Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, char * key );
+extern void        Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value );
+/*=== cmdHist.c ========================================================*/
+extern void          Cmd_HistoryAddCommand( Abc_Frame_t * pAbc, char * command );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+

src/base/cmd/cmdAlias.c

+/**CFile****************************************************************
+
+  FileName    [cmdAlias.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures dealing with aliases in the command package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cmdAlias.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cmdInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CmdCommandAliasAdd( Abc_Frame_t * pAbc, char * sName, int argc, char ** argv )
+{
+    Abc_Alias * pAlias;
+    int fStatus, i;
+
+    pAlias = ALLOC(Abc_Alias, 1);
+    pAlias->sName = util_strsav(sName);
+    pAlias->argc = argc;
+    pAlias->argv = ALLOC(char *, pAlias->argc);
+    for(i = 0; i < argc; i++) 
+        pAlias->argv[i] = util_strsav(argv[i]);
+    fStatus = st_insert( pAbc->tAliases, pAlias->sName, (char *) pAlias );
+    assert(!fStatus);  
+}
+
+/**Function********************************************************************
+
+  Synopsis    [required]
+
+  Description [optional]
+
+  SideEffects [required]
+
+  SeeAlso     [optional]
+
+******************************************************************************/
+void CmdCommandAliasPrint( Abc_Frame_t * pAbc, Abc_Alias * pAlias )
+{
+    int i;
+    fprintf(pAbc->Out, "%s\t", pAlias->sName);
+    for(i = 0; i < pAlias->argc; i++) 
+        fprintf( pAbc->Out, " %s", pAlias->argv[i] );
+    fprintf( pAbc->Out, "\n" );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [required]
+
+  Description [optional]
+
+  SideEffects [required]
+
+  SeeAlso     [optional]
+
+******************************************************************************/
+char * CmdCommandAliasLookup( Abc_Frame_t * pAbc, char * sCommand )
+{
+  Abc_Alias * pAlias;
+  char * value;
+  if (!st_lookup( pAbc->tAliases, sCommand, &value)) 
+    return sCommand;
+  pAlias = (Abc_Alias *) value;
+  return pAlias->argv[0];
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void CmdCommandAliasFree( Abc_Alias * pAlias )
+{
+    CmdFreeArgv( pAlias->argc, pAlias->argv );
+    FREE(pAlias->sName);    
+    FREE(pAlias);
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/cmd/cmdApi.c

+/**CFile****************************************************************
+
+  FileName    [cmdApi.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [External procedures of the command package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cmdApi.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+#include "cmdInt.h"
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cmd_CommandAdd( Abc_Frame_t * pAbc, char * sGroup, char * sName, void * pFunc, int fChanges )
+{
+    char * key, * value;
+    Abc_Command * pCommand;
+    int fStatus;
+
+    key = sName;
+    if ( st_delete( pAbc->tCommands, &key, &value ) ) 
+    {
+        // delete existing definition for this command 
+        fprintf( pAbc->Err, "Cmd warning: redefining '%s'\n", sName );
+        CmdCommandFree( (Abc_Command *)value );
+    }
+
+    // create the new command
+    pCommand = ALLOC( Abc_Command, 1 );
+    pCommand->sName   = util_strsav( sName );
+    pCommand->sGroup  = util_strsav( sGroup );
+    pCommand->pFunc   = pFunc;
+    pCommand->fChange = fChanges;
+    fStatus = st_insert( pAbc->tCommands, sName, (char *)pCommand );
+    assert( !fStatus );  // the command should not be in the table
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cmd_CommandExecute( Abc_Frame_t * pAbc, char * sCommand )
+{
+    int fStatus = 0, argc, loop;
+    char * sCommandNext, **argv;
+
+    if ( !pAbc->fAutoexac ) 
+        Cmd_HistoryAddCommand(pAbc, sCommand);
+    sCommandNext = sCommand;
+    do 
+    {
+           sCommandNext = CmdSplitLine( pAbc, sCommandNext, &argc, &argv );
+        loop = 0;
+        fStatus = CmdApplyAlias( pAbc, &argc, &argv, &loop );
+        if ( fStatus == 0 ) 
+            fStatus = CmdCommandDispatch( pAbc, argc, argv );
+           CmdFreeArgv( argc, argv );
+    } 
+    while ( fStatus == 0 && *sCommandNext != '\0' );
+    return fStatus;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/cmd/cmdFlag.c

+/**CFile****************************************************************
+
+  FileName    [cmdFlag.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures working with flags.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cmdFlag.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function********************************************************************
+
+  Synopsis    [Looks up value of flag in table of named values.]
+
+  Description [The command parser maintains a table of named values.  These
+  are manipulated using the 'set' and 'unset' commands.  The value of the
+  named flag is returned, or NIL(char) is returned if the flag has not been
+  set.]
+
+  SideEffects []
+
+******************************************************************************/
+char * Cmd_FlagReadByName( Abc_Frame_t * pAbc, char * flag )
+{
+  char *value;
+
+  if (st_lookup(pAbc->tFlags, flag, &value)) {
+    return value;
+  }
+  else {
+    return NIL(char);
+  }
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Updates a set value by calling instead of set command.]
+
+  Description [Updates a set value by calling instead of set command.]
+
+  SideEffects []
+
+******************************************************************************/
+void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value )
+{
+  char *oldValue, *newValue;
+
+  if (!key)
+    return;
+  if (value)
+    newValue = util_strsav(value);
+  else
+    newValue = util_strsav("");
+
+  if (st_delete(pAbc->tFlags, &key, &oldValue))
+    FREE(oldValue);
+
+  st_insert(pAbc->tFlags, key, newValue);
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Deletes a set value by calling instead of unset command.]
+
+  Description [Deletes a set value by calling instead of unset command.]
+
+  SideEffects []
+
+******************************************************************************/
+void Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, char * key )
+{
+  char *value;
+
+  if (!key)
+    return;
+
+  if (st_delete(pAbc->tFlags, &key, &value)) {
+    FREE(key);
+    FREE(value);
+  }
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/cmd/cmdHist.c

+/**CFile****************************************************************
+
+  FileName    [cmdHist.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures working with history.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cmdHist.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+#include "cmd.h"
+#include "cmdInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cmd_HistoryAddCommand(    Abc_Frame_t * p, char * command )
+{
+    char Buffer[500];
+    strcpy( Buffer, command );
+    if ( command[strlen(command)-1] != '\n' )
+        strcat( Buffer, "\n" );
+    Vec_PtrPush( p->aHistory, util_strsav(Buffer) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////

src/base/cmd/cmdInt.h

+/**CFile****************************************************************
+
+  FileName    [cmdInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Internal declarations of the command package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cmdInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CMD_INT_H__
+#define __CMD_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "mainInt.h"
+#include "cmd.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+struct MvCommand
+{
+    char *        sName;       // the command name  
+    char *        sGroup;      // the group name  
+    void *        pFunc;       // the function to execute the command 
+    int           fChange;     // set to 1 to mark that the network is changed
+};
+
+struct MvAlias
+{
+    char *        sName;       // the alias name
+    int           argc;        // the number of alias parts
+    char **       argv;        // the alias parts
+};
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFITIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cmdAlias.c =============-========================================*/
+extern void       CmdCommandAliasAdd( Abc_Frame_t * pAbc, char * sName, int argc, char ** argv );
+extern void       CmdCommandAliasPrint( Abc_Frame_t * pAbc, Abc_Alias * pAlias );
+extern char *     CmdCommandAliasLookup( Abc_Frame_t * pAbc, char * sCommand );
+extern void       CmdCommandAliasFree( Abc_Alias * p );
+/*=== cmdUtils.c =======================================================*/
+extern int        CmdCommandDispatch( Abc_Frame_t * pAbc, int  argc, char ** argv );
+extern char *     CmdSplitLine( Abc_Frame_t * pAbc, char * sCommand, int * argc, char *** argv );
+extern int        CmdApplyAlias( Abc_Frame_t * pAbc, int * argc, char *** argv, int * loop );
+extern char *     CmdHistorySubstitution( Abc_Frame_t * pAbc, char * line, int * changed );
+extern FILE *     CmdFileOpen( Abc_Frame_t * pAbc, char * sFileName, char * sMode, char ** pFileNameReal, int silent );
+extern void       CmdFreeArgv( int argc, char ** argv );
+extern void       CmdCommandFree( Abc_Command * pCommand );
+extern void       CmdCommandPrint( Abc_Frame_t * pAbc, bool fPrintAll );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+

src/base/cmd/module.make

+SRC +=  src/base/cmd/cmd.c \
+    src/base/cmd/cmdAlias.c \
+    src/base/cmd/cmdApi.c \
+    src/base/cmd/cmdFlag.c \
+    src/base/cmd/cmdHist.c \
+    src/base/cmd/cmdUtils.c

src/base/io/io.h

+/**CFile****************************************************************
+
+  FileName    [io.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: io.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __IO_H__
+#define __IO_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+#define  IO_WRITE_LINE_LENGTH    78    // the output line length
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== abcRead.c ==========================================================*/
+extern Abc_Ntk_t *        Io_Read( char * pFileName, int fCheck );
+/*=== abcReadBlif.c ==========================================================*/
+extern Abc_Ntk_t *        Io_ReadBlif( char * pFileName, int fCheck );
+/*=== abcReadBench.c ==========================================================*/
+extern Abc_Ntk_t *        Io_ReadBench( char * pFileName, int fCheck );
+/*=== abcReadVerilog.c ==========================================================*/
+extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
+extern void               Io_ReadSetNonDrivenNets( Abc_Ntk_t * pNet );
+/*=== abcWriteBlif.c ==========================================================*/
+extern void               Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName );
+extern void               Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
+/*=== abcWriteBlifLogic.c ==========================================================*/
+extern void               Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
+/*=== abcWriteBench.c ==========================================================*/
+extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteGate.c ==========================================================*/
+extern int                Io_WriteGate( Abc_Ntk_t * pNtk, char * FileName );
+/*=== abcWriteCnf.c ==========================================================*/
+extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+

src/base/io/ioInt.h

+/**CFile****************************************************************
+
+  FileName    [ioInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __IO_INT_H__
+#define __IO_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFITIONS                             ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+

src/base/io/ioRead.c

+/**CFile****************************************************************
+
+  FileName    [ioRead.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedure to read network from file.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioRead.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Read the network from a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_Read( char * pFileName, int fCheck )
+{
+    Abc_Ntk_t * pNtk, * pTemp;
+    // set the new network
+    if ( Extra_FileNameCheckExtension( pFileName, "blif" ) )
+        pNtk = Io_ReadBlif( pFileName, fCheck );
+    else if ( Extra_FileNameCheckExtension( pFileName, "v" ) )
+        pNtk = Io_ReadVerilog( pFileName, fCheck );
+    else if ( Extra_FileNameCheckExtension( pFileName, "bench" ) )
+        pNtk = Io_ReadBench( pFileName, fCheck );
+    else 
+    {
+        fprintf( stderr, "Unknown file format\n" );
+        return NULL;
+    }
+    if ( pNtk == NULL )
+        return NULL;
+    pNtk = Abc_NtkLogic( pTemp = pNtk );
+    Abc_NtkDelete( pTemp );
+    if ( pNtk == NULL )
+    {
+        fprintf( stdout, "Converting to logic network after reading has failed.\n" );
+        return NULL;
+    }
+    return pNtk;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+

src/base/io/ioReadBench.c

+/**CFile****************************************************************
+
+  FileName    [ioReadBench.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to read BENCH files.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioReadBench.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Read the network from BENCH file.]
+
+  Description [Currently works only for the miter cone.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck )
+{
+    Extra_FileReader_t * p;
+    Abc_Ntk_t * pNtk;
+
+    // start the file
+    p = Extra_FileReaderAlloc( pFileName, "#", "\n", " \t\r,()=" );
+    if ( p == NULL )
+        return NULL;
+
+    // read the network
+    pNtk = Io_ReadBenchNetwork( p );
+    Extra_FileReaderFree( p );
+    if ( pNtk == NULL )
+        return NULL;
+
+    // make sure that everything is okay with the network structure
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Io_ReadBench: The network check has failed.\n" );
+        Abc_NtkDelete( pNtk );
+        return NULL;
+    }
+    return pNtk;
+}
+/**Function*************************************************************
+
+  Synopsis    [Read the network from BENCH file.]
+
+  Description [Currently works only for the miter cone.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
+{
+    ProgressBar * pProgress;
+    Vec_Ptr_t * vTokens;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNet, * pLatch, * pNode;
+    Vec_Str_t * vString;
+    char * pType;
+    int SymbolIn, SymbolOut, i, iLine;
+    
+    // allocate the empty network
+    pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST );
+
+    // set the specs
+    pNtk->pName = util_strsav( Extra_FileReaderGetFileName(p) );
+    pNtk->pSpec = util_strsav( Extra_FileReaderGetFileName(p) );
+
+    // go through the lines of the file
+    vString = Vec_StrAlloc( 100 );
+    pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p) );
+    for ( iLine = 0; vTokens = Extra_FileReaderGetTokens(p); iLine++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p), NULL );
+
+        if ( vTokens->nSize == 1 )
+        {
+            printf( "%s: Wrong input file format.\n", Extra_FileReaderGetFileName(p) );
+            Abc_NtkDelete( pNtk );
+            return NULL;
+        }
+
+        // get the type of the line
+        if ( strncmp( vTokens->pArray[0], "INPUT", 5 ) == 0 )
+        {
+            pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
+            if ( Abc_ObjIsPi(pNet) )
+                printf( "Warning: PI net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
+            else
+                Abc_NtkMarkNetPi( pNet );
+        }
+        else if ( strncmp( vTokens->pArray[0], "OUTPUT", 5 ) == 0 )
+        {
+            pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[1] );
+            if ( Abc_ObjIsPo(pNet) )
+                printf( "Warning: PO net \"%s\" appears twice in the list.\n", vTokens->pArray[1] );
+            else
+                Abc_NtkMarkNetPo( pNet );
+        }
+        else 
+        {
+            // get the node name and the node type
+            pType = vTokens->pArray[1];
+            if ( strcmp(pType, "DFF") == 0 )
+            {
+                // create a new node and add it to the network
+                pLatch = Abc_NtkCreateLatch( pNtk );
+                // create the LO (PI)
+                pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[0] );
+                Abc_ObjAddFanin( pNet, pLatch );
+                Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LO );
+                // save the LI (PO)
+                pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[2] );
+                Abc_ObjAddFanin( pLatch, pNet );
+                Abc_ObjSetSubtype( pNet, ABC_OBJ_SUBTYPE_LI );
+            }
+            else
+            {
+                // create a new node and add it to the network
+                pNode = Abc_NtkCreateNode( pNtk );
+                // get the input symbol to be inserted
+                if ( !strncmp(pType, "BUF", 3) || !strcmp(pType, "AND") || !strcmp(pType, "NAND") )
+                    SymbolIn = '1';
+                else if ( !strncmp(pType, "NOT", 3) || !strcmp(pType, "OR") || !strcmp(pType, "NOR") )
+                    SymbolIn = '0';
+                else if ( !strcmp(pType, "XOR") || !strcmp(pType, "NXOR") )
+                    SymbolIn = '*';
+                else
+                {
+                    printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
+                    Abc_NtkDelete( pNtk );
+                    return NULL;
+                }
+                // get the output symbol
+                if ( !strcmp(pType, "NAND") || !strcmp(pType, "OR") || !strcmp(pType, "NXOR") )
+                    SymbolOut = '0';
+                else
+                    SymbolOut = '1';
+
+                // add the fanout net
+                pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[0] );
+                Abc_ObjAddFanin( pNet, pNode );
+                // add the fanin nets
+                for ( i = 2; i < vTokens->nSize; i++ )
+                {
+                    pNet = Abc_NtkFindOrCreateNet( pNtk, vTokens->pArray[i] );
+                    Abc_ObjAddFanin( pNode, pNet );
+                }
+                if ( SymbolIn != '*' )
+                {
+                    // fill in the function
+                    Vec_StrFill( vString, vTokens->nSize - 2, (char)SymbolIn );
+                    Vec_StrPush( vString, ' ' );
+                    Vec_StrPush( vString, (char)SymbolOut );
+                    Vec_StrPush( vString, '\n' );
+                    Vec_StrPush( vString, '\0' );
+                    Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, vString->pArray) );
+                }
+                else
+                { // write XOR/NXOR gates
+                    assert( i == 4 );
+                    if ( SymbolOut == '1' )
+                        Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "01 1\n10 1\n") );
+                    else
+                        Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "00 1\n11 1\n") );
+                }
+            }
+        }
+    }
+    Extra_ProgressBarStop( pProgress );
+    // check if constant have been added
+    if ( pNet = Abc_NtkFindNet( pNtk, "vdd" ) )
+    {
+        // create the constant 1 node
+        pNode = Abc_NtkCreateNode( pNtk );
+        Abc_ObjAddFanin( pNet, pNode );
+        Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 1\n") );
+    }
+    if ( pNet = Abc_NtkFindNet( pNtk, "gnd" ) )
+    {
+        // create the constant 1 node
+        pNode = Abc_NtkCreateNode( pNtk );
+        Abc_ObjAddFanin( pNet, pNode );
+        Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, " 0\n") );
+    }
+
+    Io_ReadSetNonDrivenNets( pNtk );
+    Vec_StrFree( vString );
+    return pNtk;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+

src/base/io/ioWriteBench.c

+/**CFile****************************************************************
+
+  FileName    [ioWriteBench.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write the network in BENCH format.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteBench.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int    Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static int    Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode );
+static char * Io_BenchNodeName( Abc_Obj_t * pObj, int fPhase );
+static char * Io_BenchNodeNameInv( Abc_Obj_t * pObj );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the network in BENCH format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteBench( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    Abc_Ntk_t * pExdc;
+    FILE * pFile;
+    assert( Abc_NtkIsAig(pNtk) );
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteBench(): Cannot open the output file.\n" );
+        return 0;
+    }
+    fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pSpec, Extra_TimeStamp() );
+    // write the network
+    Io_WriteBenchOne( pFile, pNtk );
+    // write EXDC network if it exists
+    pExdc = Abc_NtkExdc( pNtk );
+    if ( pExdc )
+    {
+        printf( "Io_WriteBench: EXDC is not written (warning).\n" );
+//        fprintf( pFile, "\n" );
+//        fprintf( pFile, ".exdc\n" );
+//        Io_LogicWriteOne( pFile, pExdc );
+    }
+    // finalize the file
+    fclose( pFile );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the network in BENCH format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteBenchOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    int i;
+
+    assert( Abc_NtkIsLogicSop(pNtk) || Abc_NtkIsAig(pNtk) );
+
+    // write the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pNode, i )
+        fprintf( pFile, "INPUT(%s)\n", Abc_NtkNamePi(pNtk,i) );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        fprintf( pFile, "OUTPUT(%s)\n", Abc_NtkNamePo(pNtk,i) );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        fprintf( pFile, "%-11s = DFF(%s)\n", 
+            Abc_NtkNameLatch(pNtk,i), Abc_NtkNameLatchInput(pNtk,i) );
+
+    // set the node names 
+    Abc_NtkCleanCopy( pNtk );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)Abc_NtkNameCi(pNtk,i);
+
+    // write intervers for COs appearing in negative polarity
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        if ( Abc_AigNodeIsUsedCompl(pNode) )
+            fprintf( pFile, "%-11s = NOT(%s)\n", 
+                Io_BenchNodeNameInv(pNode), 
+                Abc_NtkNameCi(pNtk,i) );
+    }
+
+    // write internal nodes
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        Io_WriteBenchOneNode( pFile, pNode );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // write buffers for CO
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        fprintf( pFile, "%-11s = BUFF(%s)\n", 
+            (i < Abc_NtkPoNum(pNtk))? Abc_NtkNamePo(pNtk,i) : 
+                Abc_NtkNameLatchInput( pNtk, i-Abc_NtkPoNum(pNtk) ), 
+            Io_BenchNodeName( Abc_ObjFanin0(pNode), !Abc_ObjFaninC0(pNode) ) );
+    }
+    Abc_NtkCleanCopy( pNtk );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the network in BENCH format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteBenchOneNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+    assert( Abc_ObjIsNode(pNode) );
+    // write the AND gate
+    fprintf( pFile, "%-11s",       Io_BenchNodeName( pNode, 1 ) );
+    fprintf( pFile, " = AND(%s, ", Io_BenchNodeName( Abc_ObjFanin0(pNode), !Abc_ObjFaninC0(pNode) ) ); 
+    fprintf( pFile, "%s)\n",       Io_BenchNodeName( Abc_ObjFanin1(pNode), !Abc_ObjFaninC1(pNode) ) );
+
+    // write the inverter if necessary
+    if ( Abc_AigNodeIsUsedCompl(pNode) )
+    {
+        fprintf( pFile, "%-11s = NOT(",   Io_BenchNodeName( pNode, 0 ) );
+        fprintf( pFile, "%s)\n",          Io_BenchNodeName( pNode, 1 ) );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the name of an internal AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_BenchNodeName( Abc_Obj_t * pObj, int fPhase )
+{
+    static char Buffer[500];
+    if ( pObj->pCopy ) // PIs and latches
+    {
+        sprintf( Buffer, "%s%s", (char *)pObj->pCopy, (fPhase? "":"_c") );
+        return Buffer;
+    }
+    assert( Abc_ObjIsNode(pObj) );
+    if ( Abc_NodeIsConst(pObj) ) // constant node
+    {
+        if ( fPhase )
+            sprintf( Buffer, "%s", "vdd" );
+        else
+            sprintf( Buffer, "%s", "gnd" );
+        return Buffer;
+    }
+    // internal nodes
+    sprintf( Buffer, "%s%s", Abc_ObjName(pObj), (fPhase? "":"_c") );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the name of an internal AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_BenchNodeNameInv( Abc_Obj_t * pObj )
+{
+    static char Buffer[500];
+    sprintf( Buffer, "%s%s", Abc_ObjName(pObj), "_c" );
+    return Buffer;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/io/ioWriteBlif.c

+/**CFile****************************************************************
+
+  FileName    [ioWriteBlif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write BLIF files.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteBlif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk );
+static void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode );
+static void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write the network into a BLIF file with the given name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteBlif( Abc_Ntk_t * pNtk, char * FileName )
+{
+    Abc_Ntk_t * pExdc;
+    FILE * pFile;
+    assert( Abc_NtkIsNetlist(pNtk) );
+    pFile = fopen( FileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteBlif(): Cannot open the output file.\n" );
+        return;
+    }
+    // write the model name
+    fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
+    // write the network
+    Io_NtkWriteOne( pFile, pNtk );
+    // write EXDC network if it exists
+    pExdc = Abc_NtkExdc( pNtk );
+    if ( pExdc )
+    {
+        fprintf( pFile, "\n" );
+        fprintf( pFile, ".exdc\n" );
+        Io_NtkWriteOne( pFile, pExdc );
+    }
+    // finalize the file
+    fprintf( pFile, ".end\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write one network.]
+
+  Description [Writes a network composed of PIs, POs, internal nodes,
+  and latches. The following rules are used to print the names of 
+  internal nodes:
+  ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode, * pLatch;
+    int i;
+
+    // write the PIs
+    fprintf( pFile, ".inputs" );
+    Io_NtkWritePis( pFile, pNtk );
+    fprintf( pFile, "\n" );
+
+    // write the POs
+    fprintf( pFile, ".outputs" );
+    Io_NtkWritePos( pFile, pNtk );
+    fprintf( pFile, "\n" );
+
+    // write the timing info
+    Io_WriteTimingInfo( pFile, pNtk );
+
+    // write the latches
+    if ( !Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pFile, "\n" );
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+            Io_NtkWriteLatch( pFile, pLatch );
+        fprintf( pFile, "\n" );
+    }
+
+    // write each internal node
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Io_NtkWriteNode( pFile, pNode );
+    }
+    Extra_ProgressBarStop( pProgress );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary input list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = 7;
+    NameCounter = 0;
+    Abc_NtkForEachPi( pNtk, pNet, i )
+    {
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \\\n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary input list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = 8;
+    NameCounter = 0;
+    Abc_NtkForEachPo( pNtk, pNet, i )
+    {
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \\\n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Write the latch into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteLatch( FILE * pFile, Abc_Obj_t * pLatch )
+{
+    Abc_Obj_t * pNetLi, * pNetLo;
+    int Reset;
+    pNetLi = Abc_ObjFanin0( pLatch );
+    pNetLo = Abc_ObjFanout0( pLatch );
+    Reset  = (int)Abc_ObjData( pLatch );
+    // write the latch line
+    fprintf( pFile, ".latch" );
+    fprintf( pFile, " %10s",      Abc_ObjName(pNetLi) );
+    fprintf( pFile, " %10s",      Abc_ObjName(pNetLo) );
+    fprintf( pFile, "  %d\n",   Reset );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Write the node into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode )
+{
+    // write the .names line
+    fprintf( pFile, ".names" );
+    Io_NtkWriteNodeFanins( pFile, pNode );
+    fprintf( pFile, "\n" );
+    // write the cubes
+    fprintf( pFile, "%s", Abc_ObjData(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary input list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    char * pName;
+    int i;
+
+    LineLength  = 6;
+    NameCounter = 0;
+    Abc_ObjForEachFanin( pNode, pNet, i )
+    {
+        // get the fanin name
+        pName = Abc_ObjName(pNet);
+        // get the line length after the fanin name is written
+        AddedLength = strlen(pName) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \\\n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", pName );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+
+    // get the output name
+    pName = Abc_ObjName(Abc_ObjFanout0(pNode));
+    // get the line length after the output name is written
+    AddedLength = strlen(pName) + 1;
+    if ( NameCounter && LineLength + AddedLength > 75 )
+    { // write the line extender
+        fprintf( pFile, " \\\n" );
+        // reset the line length
+        LineLength  = 0;
+        NameCounter = 0;
+    }
+    fprintf( pFile, " %s", pName );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the timing info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    Abc_Time_t * pTime, * pTimeDef;
+    int i;
+
+    if ( pNtk->pManTime == NULL )
+        return;
+
+    pTimeDef = Abc_NtkReadDefaultArrival( pNtk );
+    fprintf( pFile, ".default_input_arrival %g %g\n", pTimeDef->Rise, pTimeDef->Fall );
+    Abc_NtkForEachPi( pNtk, pNode, i )
+    {
+        pTime = Abc_NodeReadArrival(pNode);
+        if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
+            continue;
+        fprintf( pFile, ".input_arrival %s %g %g\n", Abc_NtkNamePi(pNtk,i), pTime->Rise, pTime->Fall );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/io/ioWriteCnf.c

+/**CFile****************************************************************
+
+  FileName    [ioWriteCnf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to CNF of the miter cone.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Io_WriteCnfInt( FILE * pFile, Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write the miter cone into a CNF file for the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    solver * pSat;
+    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    {
+        fprintf( stdout, "Io_WriteCnf(): Currently can process logic networks with BDDs.\n" );
+        return 0;
+    }
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter (the network with one PO).\n" );
+        return 0;
+    }
+    if ( Abc_NtkLatchNum(pNtk) != 0 )
+    {
+        fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter for combinational circuits.\n" );
+        return 0;
+    }
+    // create solver with clauses
+    pSat = Abc_NtkMiterSatCreate( pNtk );
+    // write the clauses
+    Asat_SolverWriteDimacs( pSat, pFileName );
+    // free the solver
+    solver_delete( pSat );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/io/ioWriteGate.c

+/**CFile****************************************************************
+
+  FileName    [ioWriteGate.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write the mapped network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ioWriteGate.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "io.h"
+#include "main.h"
+#include "mio.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void   Io_WriteGateOne( FILE * pFile, Abc_Ntk_t * pNtk );
+static void   Io_WriteGatePis( FILE * pFile, Abc_Ntk_t * pNtk );
+static void   Io_WriteGatePos( FILE * pFile, Abc_Ntk_t * pNtk );
+static void   Io_WriteGateNode( FILE * pFile, Abc_Obj_t * pNode, Mio_Gate_t * pGate );
+static char * Io_ReadNodeName( Abc_Obj_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes mapped network into a BLIF file compatible with SIS.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Io_WriteGate( Abc_Ntk_t * pNtk, char * pFileName )
+{
+    Abc_Ntk_t * pExdc;
+    FILE * pFile;
+
+    assert( Abc_NtkIsLogicMap(pNtk) );
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Io_WriteGate(): Cannot open the output file.\n" );
+        return 0;
+    }
+    // write the model name
+    fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
+    // write the network
+    Io_WriteGateOne( pFile, pNtk );
+    // write EXDC network if it exists
+    pExdc = Abc_NtkExdc( pNtk );
+    if ( pExdc )
+        printf( "Io_WriteGate: EXDC is not written (warning).\n" );
+    // finalize the file
+    fprintf( pFile, ".end\n" );
+    fclose( pFile );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write one network.]
+
+  Description [Writes a network composed of PIs, POs, internal nodes,
+  and latches. The following rules are used to print the names of 
+  internal nodes: ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteGateOne( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode, * pLatch;
+    int i;
+
+    assert( Abc_NtkIsLogicMap(pNtk) );
+    assert( Abc_NtkLogicHasSimplePos(pNtk) );
+
+    // write the PIs
+    fprintf( pFile, ".inputs" );
+    Io_WriteGatePis( pFile, pNtk );
+    fprintf( pFile, "\n" );
+
+    // write the POs
+    fprintf( pFile, ".outputs" );
+    Io_WriteGatePos( pFile, pNtk );
+    fprintf( pFile, "\n" );
+
+    // write the timing info
+    Io_WriteTimingInfo( pFile, pNtk );
+
+    // write the latches
+    if ( Abc_NtkLatchNum(pNtk) )
+    {
+        fprintf( pFile, "\n" );
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+            fprintf( pFile, ".latch %s %s  %d\n", 
+                Abc_NtkNameLatchInput(pNtk,i), Abc_NtkNameLatch(pNtk,i), (int)pLatch->pData );
+        fprintf( pFile, "\n" );
+    }
+    // set the node names
+    Abc_NtkLogicTransferNames( pNtk );
+    // write internal nodes
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Io_WriteGateNode( pFile, pNode, pNode->pData );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkCleanCopy( pNtk );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary input list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteGatePis( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    char * pName;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = 7;
+    NameCounter = 0;
+    Abc_NtkForEachPi( pNtk, pNode, i )
+    {
+        pName = pNtk->vNamesPi->pArray[i];
+        // get the line length after this name is written
+        AddedLength = strlen(pName) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \\\n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", pName );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the primary input list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteGatePos( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    char * pName;
+    int i;
+
+    LineLength  = 8;
+    NameCounter = 0;
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        pName = pNtk->vNamesPo->pArray[i];
+        // get the line length after this name is written
+        AddedLength = strlen(pName) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \\\n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", pName );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Write the node into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteGateNode( FILE * pFile, Abc_Obj_t * pNode, Mio_Gate_t * pGate )
+{
+    Mio_Pin_t * pGatePin;
+    int i;
+    // do not write the buffer whose input and output have the same name
+    if ( Abc_ObjFaninNum(pNode) == 1 && Abc_ObjFanin0(pNode)->pCopy && pNode->pCopy )
+        if ( strcmp( (char*)Abc_ObjFanin0(pNode)->pCopy, (char*)pNode->pCopy ) == 0 )
+            return;
+    // write the node
+    fprintf( pFile, ".gate %s ", Mio_GateReadName(pGate) );
+    for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ )
+        fprintf( pFile, "%s=%s ", Mio_PinReadName(pGatePin), Io_ReadNodeName( Abc_ObjFanin(pNode,i) ) );
+    assert ( i == Abc_ObjFaninNum(pNode) );
+    fprintf( pFile, "%s=%s\n", Mio_GateReadOutName(pGate), Io_ReadNodeName(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the name of the node to write.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Io_ReadNodeName( Abc_Obj_t * pNode )
+{
+    if ( pNode->pCopy )
+        return (char *)pNode->pCopy;
+    return Abc_ObjName(pNode);
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/io/module.make

+SRC +=  src/base/io/io.c \
+    src/base/io/ioRead.c \
+    src/base/io/ioReadBench.c \
+    src/base/io/ioReadBlif.c \
+    src/base/io/ioReadVerilog.c \
+    src/base/io/ioWriteBench.c \
+    src/base/io/ioWriteBlif.c \
+    src/base/io/ioWriteBlifLogic.c \
+    src/base/io/ioWriteCnf.c \
+    src/base/io/ioWriteGate.c

src/base/main/main.c

+/**CFile****************************************************************
+
+  FileName    [main.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The main package.]
+
+  Synopsis    [Here everything starts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mainInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int TypeCheck( Abc_Frame_t * pAbc, char * s);
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [The main() procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int main( int argc, char * argv[] )
+{
+    Abc_Frame_t * pAbc;
+    char sCommandUsr[500], sCommandTmp[100], sReadCmd[20], sWriteCmd[20], c;
+    char * sCommand, * sOutFile, * sInFile;
+    int  fStatus = 0;
+    bool fBatch, fInitSource, fInitRead, fFinalWrite;
+    
+    // added to detect memory leaks:
+#ifdef _DEBUG
+    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
+#endif
+
+    // get global frame (singleton pattern)
+    // will be initialized on first call
+    pAbc = Abc_FrameGetGlobalFrame();
+
+    // default options
+    fBatch = 0;
+    fInitSource = 1;
+    fInitRead   = 0;
+    fFinalWrite = 0;
+    sInFile = sOutFile = NULL;
+    sprintf( sReadCmd,  "read_blif_mv"  );
+    sprintf( sWriteCmd, "write_blif_mv" );
+    
+    util_getopt_reset();
+    while ((c = util_getopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) {
+        switch(c) {
+            case 'c':
+                strcpy( sCommandUsr, util_optarg );
+                fBatch = 1;
+                break;
+                
+            case 'f':
+                sprintf(sCommandUsr, "source %s", util_optarg);
+                fBatch = 1;
+                break;
+
+            case 'F':
+                sprintf(sCommandUsr, "source -x %s", util_optarg);
+                fBatch = 1;
+                break;
+                
+            case 'h':
+                goto usage;
+                break;
+                
+            case 'o':
+                sOutFile = util_optarg;
+                fFinalWrite = 1;
+                break;
+                
+            case 's':
+                fInitSource = 0;
+                break;
+                
+            case 't':
+                if ( TypeCheck( pAbc, util_optarg ) )
+                {
+                    if ( !strcmp(util_optarg, "none") == 0 )
+                    {
+                        fInitRead = 1;
+                        sprintf( sReadCmd, "read_%s", util_optarg );
+                    }
+                }
+                else {
+                    goto usage;
+                }
+                fBatch = 1;
+                break;
+                
+            case 'T':
+                if ( TypeCheck( pAbc, util_optarg ) )
+                {
+                    if (!strcmp(util_optarg, "none") == 0)
+                    {
+                        fFinalWrite = 1;
+                        sprintf( sWriteCmd, "write_%s", util_optarg);
+                    }
+                }
+                else {
+                    goto usage;
+                }
+                fBatch = 1;
+                break;
+                
+            case 'x':
+                fFinalWrite = 0;
+                fInitRead   = 0;
+                fBatch = 1;
+                break;
+                
+            default:
+                goto usage;
+        }
+    }
+    
+    if ( fBatch )
+    {
+        pAbc->fBatchMode = 1;
+
+        if (argc - util_optind == 0)
+        {
+            sInFile = NULL;
+        }
+        else if (argc - util_optind == 1)
+        {
+            fInitRead = 1;
+            sInFile = argv[util_optind];
+        }
+        else
+        {
+            Abc_UtilsPrintUsage( pAbc, argv[0] );
+        }
+        
+        // source the resource file
+        if ( fInitSource )
+        {
+            Abc_UtilsSource( pAbc );
+        }
+        
+        fStatus = 0;
+        if ( fInitRead && sInFile )
+        {
+            sprintf( sCommandTmp, "%s %s", sReadCmd, sInFile );
+            fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
+        }
+        
+        if ( fStatus == 0 )
+        {
+            /* cmd line contains `source <file>' */
+            fStatus = Cmd_CommandExecute( pAbc, sCommandUsr );
+            if ( (fStatus == 0 || fStatus == -1) && fFinalWrite && sOutFile )
+            {
+                sprintf( sCommandTmp, "%s %s", sWriteCmd, sOutFile );
+                fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
+            }
+        }
+        
+    }
+    else
+    {
+        // start interactive mode
+        // print the hello line
+        Abc_UtilsPrintHello( pAbc );
+        
+        // source the resource file
+        if ( fInitSource )
+        {
+            Abc_UtilsSource( pAbc );
+        }
+                
+        // execute commands given by the user
+        while ( !feof(stdin) )
+        {
+            // print command line prompt and
+            // get the command from the user
+            sCommand = Abc_UtilsGetUsersInput( pAbc );
+            
+            // execute the user's command
+            fStatus = Cmd_CommandExecute( pAbc, sCommand );
+            
+            // stop if the user quitted or an error occurred
+            if ( fStatus == -1 || fStatus == -2 )
+                break;
+        }
+    }
+    
+    // if the memory should be freed, quit packages
+    if ( fStatus == -2 ) 
+    {
+        // perform uninitializations
+        Abc_FrameEnd( pAbc );
+        // stop the framework
+        Abc_FrameDeallocate( pAbc );
+    }
+    return 0;
+
+usage:
+    Abc_UtilsPrintHello( pAbc );
+    Abc_UtilsPrintUsage( pAbc, argv[0] );
+    return 1;
+}
+
+
+/**Function********************************************************************
+
+  Synopsis    [Returns 1 if s is a file type recognized, else returns 0.]
+
+  Description [Returns 1 if s is a file type recognized by VIS, else returns
+  0. Recognized types are "blif", "blif_mv", "blif_mvs", and "none".]
+
+  SideEffects []
+
+******************************************************************************/
+static int
+TypeCheck(
+    Abc_Frame_t * pAbc,
+    char       * s)
+{
+    if (strcmp(s, "blif") == 0) {
+        return 1;
+    }
+    else if (strcmp(s, "blif_mv") == 0) {
+        return 1;
+    }
+    else if (strcmp(s, "blif_mvs") == 0) {
+        return 1;
+    }
+    else if (strcmp(s, "none") == 0) {
+        return 1;
+    }
+    else {
+        fprintf( pAbc->Err, "unknown type %s\n", s );
+        return 0;
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+