-- Walk in iirs nodes.
-- Copyright (C) 2009 Tristan Gingold
--
-- GHDL is free software; you can redistribute it and/or modify it under
-- the terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 2, or (at your option) any later
-- version.
--
-- GHDL is distributed in the hope that it will be useful, but WITHOUT ANY
-- WARRANTY; without even the implied warranty of MERCHANTABILITY or
-- FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
-- for more details.
--
-- You should have received a copy of the GNU General Public License
-- along with GCC; see the file COPYING. If not, write to the Free
-- Software Foundation, 59 Temple Place - Suite 330, Boston, MA
-- 02111-1307, USA.
with Vhdl.Utils; use Vhdl.Utils;
with Vhdl.Errors; use Vhdl.Errors;
package body Vhdl.Nodes_Walk is
function Walk_Chain (Chain : Iir; Cb : Walk_Cb) return Walk_Status
is
El : Iir;
Status : Walk_Status := Walk_Continue;
begin
El := Chain;
while El /= Null_Iir loop
Status := Cb.all (El);
exit when Status /= Walk_Continue;
El := Get_Chain (El);
end loop;
return Status;
end Walk_Chain;
function Walk_Sequential_Stmt (Stmt : Iir; Cb : Walk_Cb) return Walk_Status;
function Walk_Sequential_Stmt_Chain (Chain : Iir; Cb : Walk_Cb)
return Walk_Status
is
El : Iir;
Status : Walk_Status := Walk_Continue;
begin
El := Chain;
while El /= Null_Iir loop
Status := Cb.all (El);
exit when Status /= Walk_Continue;
Status := Walk_Sequential_Stmt (El, Cb);
exit when Status /= Walk_Continue;
El := Get_Chain (El);
end loop;
return Status;
end Walk_Sequential_Stmt_Chain;
function Walk_Sequential_Stmt (Stmt : Iir; Cb : Walk_Cb) return Walk_Status
is
Status : Walk_Status := Walk_Continue;
Chain : Iir;
begin
case Iir_Kinds_Sequential_Statement (Get_Kind (Stmt)) is
when Iir_Kind_Simple_Signal_Assignment_Statement
| Iir_Kind_Conditional_Signal_Assignment_Statement
| Iir_Kind_Selected_Waveform_Assignment_Statement
| Iir_Kind_Null_Statement
| Iir_Kind_Assertion_Statement
| Iir_Kind_Report_Statement
| Iir_Kind_Wait_Statement
| Iir_Kind_Return_Statement
| Iir_Kind_Procedure_Call_Statement
| Iir_Kind_Next_Statement
| Iir_Kind_Exit_Statement
| Iir_Kind_Variable_Assignment_Statement
| Iir_Kind_Conditional_Variable_Assignment_Statement
| Iir_Kind_Break_Statement =>
null;
when Iir_Kind_For_Loop_Statement
| Iir_Kind_While_Loop_Statement =>
Status := Walk_Sequential_Stmt_Chain
(Get_Sequential_Statement_Chain (Stmt), Cb);
when Iir_Kind_Case_Statement =>
Chain := Get_Case_Statement_Alternative_Chain (Stmt);
while Chain /= Null_Iir loop
Status := Walk_Sequential_Stmt_Chain
(Get_Associated_Chain (Chain), Cb);
exit when Status /= Walk_Continue;
Chain := Get_Chain (Chain);
end loop;
when Iir_Kind_If_Statement =>
Chain := Stmt;
while Chain /= Null_Iir loop
Status := Walk_Sequential_Stmt_Chain
(Get_Sequential_Statement_Chain (Chain), Cb);
exit when Status /= Walk_Continue;
Chain := Get_Else_Clause (Chain);
end loop;
end case;
return Status;
end Walk_Sequential_Stmt;
function Walk_Assignment_Target (Target : Iir; Cb : Walk_Cb)
return Walk_Status
is
Targ : constant Iir := Strip_Reference_Name (Target);
Chain : Iir;
Status : Walk_Status := Walk_Continue;
begin
case Get_Kind (Targ) is
when Iir_Kind_Aggregate =>
Chain := Get_Association_Choices_Chain (Targ);
while Chain /= Null_Iir loop
Status :=
Walk_Assignment_Target (Get_Associated_Expr (Chain), Cbpre { line-height: 125%; margin: 0; }
td.linenos pre { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
span.linenos { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
td.linenos pre.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
span.linenos.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
.highlight .hll { background-color: #ffffcc }
.highlight { background: #ffffff; }
.highlight .c { color: #888888 } /* Comment */
.highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */
.highlight .k { color: #008800; font-weight: bold } /* Keyword */
.highlight .ch { color: #888888 } /* Comment.Hashbang */
.highlight .cm { color: #888888 } /* Comment.Multiline */
.highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */
.highlight .cpf { color: #888888 } /* Comment.PreprocFile */
.highlight .c1 { color: #888888 } /* Comment.Single */
.highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */
.highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */
.highlight .ge { font-style: italic } /* Generic.Emph */
.highlight .gr { color: #aa0000 } /* Generic.Error */
.highlight .gh { color: #333333 } /* Generic.Heading */
.highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */
.highlight .go { color: #888888 } /* Generic.Output */
.highlight .gp { color: #555555 } /* Generic.Prompt */
.highlight .gs { font-weight: bold } /* Generic.Strong */
.highlight .gu { color: #666666 } /* Generic.Subheading */
.highlight .gt { color: #aa0000 } /* Generic.Traceback */
.highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */
.highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */
.highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */
.highlight .kp { color: #008800 } /* Keyword.Pseudo */
.highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */
.highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */
.highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */
.highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */
.highlight .na { color: #336699 } /* Name.Attribute */
.highlight .nb { color: #003388 } /* Name.Builtin */
.highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */
.highlight .no { color: #003366; font-weight: bold } /* Name.Constant */
.highlight .nd { color: #555555 } /* Name.Decorator */
.highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */
.highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */
.highlight .nl { color: #336699; font-style: italic } /* Name.Label */
.highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */
.highlight .py { color: #336699; font-weight: bold } /* Name.Property */
.highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */
.highlight .nv { color: #336699 } /* Name.Variable */
.highlight .ow { color: #008800 } /* Operator.Word */
.highlight .w { color: #bbbbbb } /* Text.Whitespace */
.highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */
.highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */
.highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */
.highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */
.highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */
.highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */
.highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */
.highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */
.highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */
.highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */
.highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */
.highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */
.highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */
.highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */
.highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */
.highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */
.highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */
.highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */
.highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */
.highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */
.highlight .vc { color: #336699 } /* Name.Variable.Class */
.highlight .vg { color: #dd7700 } /* Name.Variable.Global */
.highlight .vi { color: #3333bb } /* Name.Variable.Instance */
.highlight .vm { color: #336699 } /* Name.Variable.Magic */
.highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long *//**CFile****************************************************************
FileName [bdcDec.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [Decomposition procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bdcInt.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Minimizes the support of the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
int v;
clock_t clk = 0; // Suppress "might be used uninitialized"
if ( p->pPars->fVerbose )
clk = clock();
// compute support
pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
Kit_TruthSupport( pIsf->puOff, p->nVars );
// go through the support variables
for ( v = 0; v < p->nVars; v++ )
{
if ( (pIsf->uSupp & (1 << v)) == 0 )
continue;
Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
continue;
// if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
// continue;
// remove the variable
Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
// Kit_TruthExist( pIsf->puOn, p->nVars, v );
// Kit_TruthExist( pIsf->puOff, p->nVars, v );
pIsf->uSupp &= ~(1 << v);
}
if ( p->pPars->fVerbose )
p->timeSupps += clock() - clk;
}
/**Function*************************************************************
Synopsis [Minimizes the support of the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
int v;
clock_t clk = 0; // Suppress "might be used uninitialized"
if ( p->pPars->fVerbose )
clk = clock();
// go through the support variables
pIsf->uSupp = 0;
for ( v = 0; v < p->nVars; v++ )
{
if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) &&
!Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
continue;
if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
{
Kit_TruthExist( pIsf->puOn, p->nVars, v );
Kit_TruthExist( pIsf->puOff, p->nVars, v );
continue;
}
pIsf->uSupp |= (1 << v);
}
if ( p->pPars->fVerbose )
p->timeSupps += clock() - clk;
}
/**Function*************************************************************
Synopsis [Updates the ISF of the right after the left was decompoosed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, Bdc_Fun_t * pFunc0, Bdc_Type_t Type )
{
unsigned * puTruth = p->puTemp1;
// get the truth table of the left branch
if ( Bdc_IsComplement(pFunc0) )
Kit_TruthNot( puTruth, Bdc_Regular(pFunc0)->puFunc, p->nVars );
else
Kit_TruthCopy( puTruth, pFunc0->puFunc, p->nVars );
// split into parts
if ( Type == BDC_TYPE_OR )
{
// Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
// Right.R = bdd_exist( R, setRightRes );
// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V ); Cudd_Ref( pR->Q );
// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
// assert( pR->R != b0 );
// return (int)( pR->Q == b0 );
Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uUniq );
// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
}
else if ( Type == BDC_TYPE_AND )
{
// Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes );
// Right.Q = bdd_exist( Q, setRightRes );
// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
// pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V ); Cudd_Ref( pR->R );
// pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V ); Cudd_Ref( pR->Q );
// assert( pR->Q != b0 );
// return (int)( pR->R == b0 );
Kit_TruthAnd( pIsfR->puOff, pIsf->puOff, puTruth, p->nVars );
Kit_TruthExistSet( pIsfR->puOff, pIsfR->puOff, p->nVars, pIsfL->uUniq );
Kit_TruthExistSet( pIsfR->puOn, pIsf->puOn, p->nVars, pIsfL->uUniq );
// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
return Kit_TruthIsConst0(pIsfR->puOff, p->nVars);
}
return 0;
}
/**Function*************************************************************
Synopsis [Checks existence of OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Bdc_DecomposeGetCost( Bdc_Man_t * p, int nLeftVars, int nRightVars )
{
assert( nLeftVars > 0 );
assert( nRightVars > 0 );
// compute the decomposition coefficient
if ( nLeftVars >= nRightVars )
return BDC_SCALE * (p->nVars * nRightVars + nLeftVars);
else // if ( nLeftVars < nRightVars )
return BDC_SCALE * (p->nVars * nLeftVars + nRightVars);
}
/**Function*************************************************************
Synopsis [Checks existence of weak OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
char pVars[16];
int v, nVars, Beg, End;
assert( pIsfL->uSupp == 0 );
assert( pIsfR->uSupp == 0 );
// fill in the variables
nVars = 0;
for ( v = 0; v < p->nVars; v++ )
if ( pIsf->uSupp & (1 << v) )
pVars[nVars++] = v;
// try variable pairs
for ( Beg = 0; Beg < nVars; Beg++ )
{
Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] );
for ( End = nVars - 1; End > Beg; End-- )
{
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] );
if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
{
pIsfL->uUniq = (1 << pVars[Beg]);
pIsfR->uUniq = (1 << pVars[End]);
return 1;
}
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Checks existence of weak OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
int v, VarCost;
int VarBest = -1; // Suppress "might be used uninitialized"
int Cost, VarCostBest = 0;
for ( v = 0; v < p->nVars; v++ )
{
if ( (pIsf->uSupp & (1 << v)) == 0 )
continue;
// if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
// Exist = Cudd_bddExistAbstract( dd, pF->R, Var ); Cudd_Ref( Exist );
// if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
{
// measure the cost of this variable
// VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
// Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var ); Cudd_Ref( Univ );
// VarCost = Kit_TruthCountOnes( Univ, p->nVars );
// Cudd_RecursiveDeref( dd, Univ );
Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v );
VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars );
if ( VarCost == 0 )
VarCost = 1;
if ( VarCostBest < VarCost )
{
VarCostBest = VarCost;
VarBest = v;
}
}
}
// derive the components for weak-bi-decomposition if the variable is found
if ( VarCostBest )
{
// funQLeftRes = Q & bdd_exist( R, setRightORweak );
// Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest ); Cudd_Ref( Temp );
// pL->Q = Cudd_bddAnd( dd, pF->Q, Temp ); Cudd_Ref( pL->Q );
// Cudd_RecursiveDeref( dd, Temp );
Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest );
Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
// pL->R = pF->R; Cudd_Ref( pL->R );
// pL->V = VarBest; Cudd_Ref( pL->V );
Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
pIsfL->uUniq = (1 << VarBest);
pIsfR->uUniq = 0;
// assert( pL->Q != b0 );
// assert( pL->R != b0 );
// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
// assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
// express cost in percents of the covered boolean space
Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
if ( Cost == 0 )
Cost = 1;
return Cost;
}
return 0;
}
/**Function*************************************************************
Synopsis [Checks existence of OR-bidecomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
unsigned uSupportRem;
int v, nLeftVars = 1, nRightVars = 1;
// clean the var sets
Bdc_IsfStart( p, pIsfL );
Bdc_IsfStart( p, pIsfR );
// check that the support is correct
assert( Kit_TruthSupport(pIsf->puOn, p->nVars) == Kit_TruthSupport(pIsf->puOff, p->nVars) );
assert( pIsf->uSupp == Kit_TruthSupport(pIsf->puOn, p->nVars) );
// find initial variable sets
if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
// prequantify the variables in the offset
Kit_TruthExistSet( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->uUniq );
Kit_TruthExistSet( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->uUniq );
// go through the remaining variables
uSupportRem = pIsf->uSupp & ~pIsfL->uUniq & ~pIsfR->uUniq;
for ( v = 0; v < p->nVars; v++ )
{
if ( (uSupportRem & (1 << v)) == 0 )
continue;
// prequantify this variable
Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v );
if ( nLeftVars < nRightVars )
{
// if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
// if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) )
if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
{
// pL->V &= VarNew;
pIsfL->uUniq |= (1 << v);
nLeftVars++;
Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
}
// else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
{
// pR->V &= VarNew;
pIsfR->uUniq |= (1 << v);
nRightVars++;
Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
}
}
else
{
// if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
{
// pR->V &= VarNew;
pIsfR->uUniq |= (1 << v);
nRightVars++;
Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
}
// else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
{
// pL->V &= VarNew;
pIsfL->uUniq |= (1 << v);
nLeftVars++;
Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
}
}
}
// derive the functions Q and R for the left branch
// pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V );
// pL->R = bdd_exist( pF->R, pR->V );
// Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( Temp );
// pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q );
// Cudd_RecursiveDeref( dd, Temp );
// pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( pL->R );
Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uUniq );
Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
// assert( pL->Q != b0 );
// assert( pL->R != b0 );
// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
// assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
// derive the functions Q and R for the right branch
// Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( Temp );
// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
// Cudd_RecursiveDeref( dd, Temp );
// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
assert( pIsfL->uUniq );
assert( pIsfR->uUniq );
return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );
}
/**Function*************************************************************
Synopsis [Performs one step of bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
int WeightOr, WeightAnd, WeightOrL, WeightOrR, WeightAndL, WeightAndR;
Bdc_IsfClean( p->pIsfOL );
Bdc_IsfClean( p->pIsfOR );
Bdc_IsfClean( p->pIsfAL );
Bdc_IsfClean( p->pIsfAR );
// perform OR decomposition
WeightOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
// perform AND decomposition
Bdc_IsfNot( pIsf );
WeightAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
Bdc_IsfNot( pIsf );
Bdc_IsfNot( p->pIsfAL );
Bdc_IsfNot( p->pIsfAR );
// check the case when decomposition does not exist
if ( WeightOr == 0 && WeightAnd == 0 )
{
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_MUX;
}
// check the hash table
assert( WeightOr || WeightAnd );
WeightOrL = WeightOrR = 0;
if ( WeightOr )
{
if ( p->pIsfOL->uUniq )
{
Bdc_SuppMinimize( p, p->pIsfOL );
WeightOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
}
if ( p->pIsfOR->uUniq )
{
Bdc_SuppMinimize( p, p->pIsfOR );
WeightOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
}
}
WeightAndL = WeightAndR = 0;
if ( WeightAnd )
{
if ( p->pIsfAL->uUniq )
{
Bdc_SuppMinimize( p, p->pIsfAL );
WeightAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
}
if ( p->pIsfAR->uUniq )
{
Bdc_SuppMinimize( p, p->pIsfAR );
WeightAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
}
}
// check if there is any reuse for the components
if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
{
p->numReuse++;
p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
{
p->numReuse++;
p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
}
// compare the two-component costs
if ( WeightOr > WeightAnd )
{
if ( WeightOr < BDC_SCALE )
p->numWeaks++;
p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
if ( WeightAnd < BDC_SCALE )
p->numWeaks++;
p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
}
/**Function*************************************************************
Synopsis [Find variable that leads to minimum sum of support sizes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
{
int Var, VarMin, nSuppMin, nSuppCur;
unsigned uSupp0, uSupp1;
clock_t clk = 0; // Suppress "might be used uninitialized"
if ( p->pPars->fVerbose )
clk = clock();
VarMin = -1;
nSuppMin = 1000;
for ( Var = 0; Var < p->nVars; Var++ )
{
if ( (pIsf->uSupp & (1 << Var)) == 0 )
continue;
Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, Var );
Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, Var );
Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, Var );
Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, Var );
uSupp0 = Kit_TruthSupport( pIsfL->puOn, p->nVars ) & Kit_TruthSupport( pIsfL->puOff, p->nVars );
uSupp1 = Kit_TruthSupport( pIsfR->puOn, p->nVars ) & Kit_TruthSupport( pIsfR->puOff, p->nVars );
nSuppCur = Kit_WordCountOnes(uSupp0) + Kit_WordCountOnes(uSupp1);
if ( nSuppMin > nSuppCur )
{
nSuppMin = nSuppCur;
VarMin = Var;
break;
}
}
if ( VarMin >= 0 )
{
Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, VarMin );
Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, VarMin );
Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, VarMin );
Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, VarMin );
Bdc_SuppMinimize( p, pIsfL );
Bdc_SuppMinimize( p, pIsfR );
}
if ( p->pPars->fVerbose )
p->timeMuxes += clock() - clk;
return VarMin;
}
/**Function*************************************************************
Synopsis [Creates gates.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc )
{
unsigned * puTruth = p->puTemp1;
if ( Bdc_IsComplement(pFunc) )
Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars );
else
Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars );
return Bdc_TableCheckContainment( p, pIsf, puTruth );
}
/**Function*************************************************************
Synopsis [Creates gates.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Fun_t * Bdc_ManCreateGate( Bdc_Man_t * p, Bdc_Fun_t * pFunc0, Bdc_Fun_t * pFunc1, Bdc_Type_t Type )
{
Bdc_Fun_t * pFunc;
pFunc = Bdc_FunNew( p );
if ( pFunc == NULL )
return NULL;
pFunc->Type = Type;
pFunc->pFan0 = pFunc0;
pFunc->pFan1 = pFunc1;
pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
// get the truth table of the left branch
if ( Bdc_IsComplement(pFunc0) )
Kit_TruthNot( p->puTemp1, Bdc_Regular(pFunc0)->puFunc, p->nVars );
else
Kit_TruthCopy( p->puTemp1, pFunc0->puFunc, p->nVars );
// get the truth table of the right branch
if ( Bdc_IsComplement(pFunc1) )
Kit_TruthNot( p->puTemp2, Bdc_Regular(pFunc1)->puFunc, p->nVars );
else
Kit_TruthCopy( p->puTemp2, pFunc1->puFunc, p->nVars );
// compute the function of node
if ( pFunc->Type == BDC_TYPE_AND )
{
Kit_TruthAnd( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
}
else if ( pFunc->Type == BDC_TYPE_OR )
{
Kit_TruthOr( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
// transform to AND gate
pFunc->Type = BDC_TYPE_AND;
pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
pFunc = Bdc_Not(pFunc);
}
else
assert( 0 );
// add to table
Bdc_Regular(pFunc)->uSupp = Kit_TruthSupport( Bdc_Regular(pFunc)->puFunc, p->nVars );
Bdc_TableAdd( p, Bdc_Regular(pFunc) );
return pFunc;
}
/**Function*************************************************************
Synopsis [Performs one step of bi-decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
// int static Counter = 0;
// int LocalCounter = Counter++;
Bdc_Type_t Type;
Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
Bdc_Isf_t IsfL, * pIsfL = &IsfL;
Bdc_Isf_t IsfB, * pIsfR = &IsfB;
int iVar;
clock_t clk = 0; // Suppress "might be used uninitialized"
/*
printf( "Init function (%d):\n", LocalCounter );
Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
*/
// check computed results
assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
if ( p->pPars->fVerbose )
clk = clock();
pFunc = Bdc_TableLookup( p, pIsf );
if ( p->pPars->fVerbose )
p->timeCache += clock() - clk;
if ( pFunc )
return pFunc;
// decide on the decomposition type
if ( p->pPars->fVerbose )
clk = clock();
Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
if ( p->pPars->fVerbose )
p->timeCheck += clock() - clk;
if ( Type == BDC_TYPE_MUX )
{
if ( p->pPars->fVerbose )
clk = clock();
iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
if ( p->pPars->fVerbose )
p->timeMuxes += clock() - clk;
p->numMuxes++;
pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
if ( pFunc0 == NULL || pFunc1 == NULL )
return NULL;
pFunc = Bdc_FunWithId( p, iVar + 1 );
pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND );
pFunc1 = Bdc_ManCreateGate( p, pFunc, pFunc1, BDC_TYPE_AND );
if ( pFunc0 == NULL || pFunc1 == NULL )
return NULL;
pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR );
}
else
{
pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
if ( pFunc0 == NULL )
return NULL;
// decompose the right branch
if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) )
{
p->nNodesNew--;
return pFunc0;
}
Bdc_SuppMinimize( p, pIsfR );
pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
if ( pFunc1 == NULL )
return NULL;
// create new gate
pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
}
return pFunc;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
