/**CFile**************************************************************** FileName [bmcCexCut.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [SAT-based bounded model checking.] Synopsis [Derives characterization of bad states.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: bmcCexCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "bmc.h" #include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Generate justifying assignments.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Bmc_GiaGenerateJust_rec( Gia_Man_t * p, int iFrame, int iObj, Vec_Bit_t * vValues, Vec_Bit_t * vJustis ) { Gia_Obj_t * pObj; int Shift = Gia_ManObjNum(p) * iFrame; if ( iFrame < 0 ) return 0; assert( iFrame >= 0 ); if ( Vec_BitEntry( vJustis, Shift + iObj ) ) return 0; Vec_BitWriteEntry( vJustis, Shift + iObj, 1 ); pObj = Gia_ManObj( p, iObj ); if ( Gia_ObjIsCo(pObj) ) return Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis ); if ( Gia_ObjIsCi(pObj) ) return Bmc_GiaGenerateJust_rec( p, iFrame-1, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)), vValues, vJustis ); assert( Gia_ObjIsAnd(pObj) ); if ( Vec_BitEntry( vValues, Shift + iObj ) ) { Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis ); Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId1(pObj, iObj), vValues, vJustis ); } else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId0(pObj, iObj) ) == Gia_ObjFaninC0(pObj) ) Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis ); else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId1(pObj, iObj) ) == Gia_ObjFaninC1(pObj) ) Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId1(pObj, iObj), vValues, vJustis ); else assert( 0 ); return 0; } void Bmc_GiaGenerateJustNonRec( Gia_Man_t * p, int iFrame, Vec_Bit_t * vValues, Vec_Bit_t * vJustis ) { Gia_Obj_t * pObj; int i, k, Shift = Gia_ManObjNum(p) * iFrame; for ( i = iFrame; i >= 0; i--, Shift -= Gia_ManObjNum(p) ) { Gia_ManForEachObjReverse( p, pObj, k ) { if ( k == 0 || Gia_ObjIsPi(p, pObj) ) continue; if ( !Vec_BitEntry( vJustis, Shift + k ) ) continue; if ( Gia_ObjIsAnd(pObj) ) { if ( Vec_BitEntry( vValues, Shift + k ) ) { Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 ); Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId1(pObj, k), 1 ); } else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId0(pObj, k) ) == Gia_ObjFaninC0(pObj) ) Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 ); else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId1(pObj, k) ) == Gia_ObjFaninC1(pObj) ) Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId1(pObj, k), 1 ); else assert( 0 ); } else if ( Gia_ObjIsCo(pObj) ) Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 ); else if ( Gia_ObjIsCi(pObj) && i ) Vec_BitWriteEntry( vJustis, Shift - Gia_ManObjNum(p) + Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)), 1 ); } } } void Bmc_GiaGenerateJust( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvValues, Vec_Bit_t ** pvJustis ) { Vec_Bit_t * vValues = Vec_BitStart( Gia_ManObjNum(p) * (pCex->iFrame + 1) ); Vec_Bit_t * vJustis = Vec_BitStart( Gia_ManObjNum(p) * (pCex->iFrame + 1) ); Gia_Obj_t * pObj; int i, k, iBit = 0, fCompl0, fCompl1, fJusti0, fJusti1, Shift; Gia_ManCleanMark0(p); Gia_ManCleanMark1(p); Gia_ManForEachRi( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); for ( Shift = i = 0; i <= pCex->iFrame; i++, Shift += Gi
/*
 * Copyright (c) 2006, Swedish Institute of Computer Science.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions
 * are met:
 * 1. Redistributions of source code must retain the above copyright
 *    notice, this list of conditions and the following disclaimer.
 * 2. Redistributions in binary form must reproduce the above copyright
 *    notice, this list of conditions and the following disclaimer in the
 *    documentation and/or other materials provided with the distribution.
 * 3. Neither the name of the Institute nor the names of its contributors
 *    may be used to endorse or promote products derived from this software
 *    without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE INSTITUTE AND CONTRIBUTORS ``AS IS'' AND
 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED.  IN NO EVENT SHALL THE INSTITUTE OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
 * SUCH DAMAGE.
 *
 * This file is part of the uIP TCP/IP stack
 *
 * $Id: clock-arch.h,v 1.2 2006/06/12 08:00:31 adam Exp $
 */

#ifndef __CLOCK_ARCH_H__
#define __CLOCK_ARCH_H__

#include <ch.h>

typedef systime_t clock_time_t;
#define CLOCK_CONF_SECOND CH_FREQUENCY

#endif /* __CLOCK_ARCH_H__ */
generated by cgit v1.2.3 (git 2.25.1) at 2025-12-05 04:14:41 +0000
assert( pObj->Value > 0 ); } if ( i == pCex->iFrame ) break; Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) { pObjRo->fMark0 = pObjRi->fMark0; pObjRo->Value = pObjRi->Value; } } assert( iBit == pCex->nBits ); // create PO Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value ); } Gia_ManHashStop( pNew ); Vec_BitFree( vInitEnd ); // cleanup pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; } /**Function************************************************************* Synopsis [Generates one frame.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Bmc_GiaGenerateGiaAllOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd ) { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj, * pObjRo, * pObjRi; int i, k, iBit = 0, fCompl0, fCompl1; // skip trough the first iFrEnd frames Gia_ManCleanMark0(p); Gia_ManForEachRo( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); *pvInits = Vec_BitStart( Gia_ManRegNum(p) ); for ( i = 0; i < iFrEnd; i++ ) { // remember values in frame iFrBeg if ( i == iFrBeg ) Gia_ManForEachRo( p, pObjRo, k ) if ( pObjRo->fMark0 ) Vec_BitWriteEntry( *pvInits, k, 1 ); // simulate other values Gia_ManForEachPi( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); Gia_ManForEachAnd( p, pObj, k ) pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); Gia_ManForEachCo( p, pObj, k ) pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) pObjRo->fMark0 = pObjRi->fMark0; } assert( i == iFrEnd ); // create new AIG manager pNew = Gia_ManStart( 10000 ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 1; Gia_ManForEachPi( p, pObj, k ) pObj->Value = 1; Gia_ManForEachRo( p, pObjRo, k ) pObjRo->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 ); Gia_ManHashStart( pNew ); for ( i = iFrEnd; i <= pCex->iFrame; i++ ) { Gia_ManForEachPi( p, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++); Gia_ManForEachAnd( p, pObj, k ) { fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj); pObj->fMark0 = fCompl0 & fCompl1; if ( pObj->fMark0 ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); else if ( !fCompl0 && !fCompl1 ) pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); else if ( !fCompl0 ) pObj->Value = Gia_ObjFanin0(pObj)->Value; else if ( !fCompl1 ) pObj->Value = Gia_ObjFanin1(pObj)->Value; else assert( 0 ); assert( pObj->Value > 0 ); } Gia_ManForEachCo( p, pObj, k ) { pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj); pObj->Value = Gia_ObjFanin0(pObj)->Value; assert( pObj->Value > 0 ); } if ( i == pCex->iFrame ) break; Gia_ManForEachRiRo( p, pObjRi, pObjRo, k ) { pObjRo->fMark0 = pObjRi->fMark0; pObjRo->Value = pObjRi->Value; } } Gia_ManHashStop( pNew ); assert( iBit == pCex->nBits ); // create PO Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value ); // cleanup pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; } /**Function************************************************************* Synopsis [Generate GIA for target bad states.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose ) { Gia_Man_t * pNew, * pTemp; Vec_Bit_t * vInitNew; if ( iFrBeg < 0 ) { printf( "Starting frame is less than 0.\n" ); return NULL; } if ( iFrEnd < 0 ) { printf( "Stopping frame is less than 0.\n" ); return NULL; } if ( iFrBeg > pCex->iFrame ) { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } if ( iFrEnd > pCex->iFrame ) { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; } if ( iFrBeg > iFrEnd ) { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; } assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame ); assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame ); assert( iFrBeg < iFrEnd ); if ( fUseOne ) pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd ); else if ( fAllFrames ) pNew = Bmc_GiaGenerateGiaAllFrames( p, pCex, &vInitNew, iFrBeg, iFrEnd ); else pNew = Bmc_GiaGenerateGiaAllOne( p, pCex, &vInitNew, iFrBeg, iFrEnd ); if ( !fCombOnly ) { // create new GIA pNew = Gia_ManDupWithNewPo( p, pTemp = pNew ); Gia_ManStop( pTemp ); // create new initial state pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) ); Gia_ManStop( pTemp ); } Vec_BitFree( vInitNew ); return pNew; } /**Function************************************************************* Synopsis [Generate AIG for target bad states.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose ) { Aig_Man_t * pAig; Gia_Man_t * pGia, * pRes; pGia = Gia_ManFromAigSimple( p ); if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) ) { Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName ); Gia_ManStop( pGia ); return NULL; } pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fAllFrames, fVerbose ); Gia_ManStop( pGia ); pAig = Gia_ManToAigSimple( pRes ); Gia_ManStop( pRes ); return pAig; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END