/**CFile****************************************************************
FileName [giaAbs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Counter-example-guided abstraction refinement.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Gia_ManCleanMark0(pAig);
Gia_ManForEachRo( pAig, pObj, i )
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
{
pObjRo->fMark0 = pObjRi->fMark0;
}
}
assert( iBit == p->nBits );
if ( fDualOut )
RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
else
RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
Gia_ManCleanMark0(pAig);
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
assert( Gia_ManPiNum(pAig) == p->nPis );
Gia_ManCleanMark0(pAig);
// Gia_ManForEachRo( pAig, pObj, i )
// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
{
Gia_ManForEachPi( pAig, pObj, k )
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
Gia_ManForEachAnd( pAig, pObj, k )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachCo( pAig, pObj, k )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == p->nBits );
// figure out the number of failed output
RetValue = -1;
// for ( i = Gia_ManPoNum(pAig) - 1; i >= nOutputs; i-- )
for ( i = nOutputs; i < Gia_ManPoNum(pAig); i++ )
{
if ( Gia_ManPo(pAig, i)->fMark0 )
{
RetValue = i;
break;
}
}
Gia_ManCleanMark0(pAig);
return RetValue;
}
/**Function*************************************************************
Synopsis [Starts the process of returning values for internal nodes.]
Description [Should be called when pCex is available, before probing
any object for its value using Gia_ManCounterExampleValueLookup().]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex )
{
Gia_Obj_t * pObj, * pObjRi, * pObjRo;
int Val0, Val1, nObjs, i, k, iBit = 0;
assert( Gia_ManRegNum(pGia) > 0 ); // makes sense only for sequential AIGs
assert( pGia->pData2 == NULL ); // if this fail, there may be a memory leak
// allocate memory to store simulation bits for internal nodes
pGia->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Gia_ManObjNum(pGia) ) );
// the register values in the counter-example should be zero
Gia_ManForEachRo( pGia, pObj, k )
assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
// iterate through the timeframes
nObjs = Gia_ManObjNum(pGia);
for ( i = 0; i <= pCex->iFrame; i++ )
{
// no need to set constant-0 node
// set primary inputs according to the counter-example
Gia_ManForEachPi( pGia, pObj, k )
if ( Abc_InfoHasBit(pCex->pData, iBit++) )
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
// compute values for each node
Gia_ManForEachAnd( pGia, pObj, k )
{
Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) );
Val1 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId1p(pGia, pObj) );
if ( (Val0 ^ Gia_ObjFaninC0(pObj)) & (Val1 ^ Gia_ObjFaninC1(pObj)) )
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
}
// derive values for combinational outputs
Gia_ManForEachCo( pGia, pObj, k )
{
Val0 = Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjFaninId0p(pGia, pObj) );
if ( Val0 ^ Gia_ObjFaninC0(pObj) )
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObj) );
}
if ( i == pCex->iFrame )
continue;
// transfer values to the register output of the next frame
Gia_ManForEachRiRo( pGia, pObjRi, pObjRo, k )
if ( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * i + Gia_ObjId(pGia, pObjRi) ) )
Abc_InfoSetBit( (unsigned *)pGia->pData2, nObjs * (i+1) + Gia_ObjId(pGia, pObjRo) );
}
assert( iBit == pCex->nBits );
// check that the counter-example is correct, that is, the corresponding output is asserted
assert( Abc_InfoHasBit( (unsigned *)pGia->pData2, nObjs * pCex->iFrame + Gia_ObjId(pGia, Gia_ManCo(pGia, pCex->iPo)) ) );
}
/**Function*************************************************************
Synopsis [Stops the process of returning values for internal nodes.]
Description [Should be called when probing is no longer needed]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia )
{
assert( pGia->pData2 != NULL ); // if this fail, we try to call this procedure more than once
ABC_FREE( pGia->pData2 );
pGia->pData2 = NULL;
}
/**Function*************************************************************
Synopsis [Returns the value of the given object in the given timeframe.]
Description [Should be called to probe the value of an object with
the given ID (iFrame is a 0-based number of a time frame - should not
exceed the number of timeframes in the original counter-example).]
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame )
{
assert( Id >= 0 && Id < Gia_ManObjNum(pGia) );
return Abc_InfoHasBit( (unsigned *)pGia->pData2, Gia_ManObjNum(pGia) * iFrame + Id );
}
/**Function*************************************************************
Synopsis [Procedure to test the above code.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCounterExampleValueTest( Gia_Man_t * pGia, Abc_Cex_t * pCex )
{
Gia_Obj_t * pObj = Gia_ManObj( pGia, Gia_ManObjNum(pGia)/2 );
int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
Gia_ManCounterExampleValueStart( pGia, pCex );
printf( "Value of object %d in frame %d is %d.\n", Gia_ObjId(pGia, pObj), iFrame,
Gia_ManCounterExampleValueLookup(pGia, Gia_ObjId(pGia, pObj), iFrame) );
Gia_ManCounterExampleValueStop( pGia );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
67' href='#n167'>167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
#
# Copyright (C) 2006-2011 OpenWrt.org
#
# This is free software, licensed under the GNU General Public License v2.
# See /LICENSE for more information.
#
LEDS_MENU:=LED modules
define KernelPackage/leds-gpio
SUBMENU:=$(LEDS_MENU)
TITLE:=GPIO LED support
DEPENDS:= @GPIO_SUPPORT
KCONFIG:=CONFIG_LEDS_GPIO
FILES:=$(LINUX_DIR)/drivers/leds/leds-gpio.ko
AUTOLOAD:=$(call AutoLoad,60,leds-gpio,1)
endef
define KernelPackage/leds-gpio/description
Kernel module for LEDs on GPIO lines
endef
$(eval $(call KernelPackage,leds-gpio))
define KernelPackage/ledtrig-heartbeat
SUBMENU:=$(LEDS_MENU)
TITLE:=LED Heartbeat Trigger
KCONFIG:=CONFIG_LEDS_TRIGGER_HEARTBEAT
FILES:=$(LINUX_DIR)/drivers/leds/$(if $(call kernel_patchver_ge,3.10),trigger/)ledtrig-heartbeat.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-heartbeat)
endef
define KernelPackage/ledtrig-gpio/description
Kernel module that allows LEDs to blink like heart beat
endef
$(eval $(call KernelPackage,ledtrig-heartbeat))
define KernelPackage/ledtrig-gpio
SUBMENU:=$(LEDS_MENU)
TITLE:=LED GPIO Trigger
KCONFIG:=CONFIG_LEDS_TRIGGER_GPIO
FILES:=$(LINUX_DIR)/drivers/leds/$(if $(call kernel_patchver_ge,3.10),trigger/)ledtrig-gpio.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-gpio)
endef
define KernelPackage/ledtrig-gpio/description
Kernel module that allows LEDs to be controlled by gpio events
endef
$(eval $(call KernelPackage,ledtrig-gpio))
define KernelPackage/ledtrig-morse
SUBMENU:=$(LEDS_MENU)
TITLE:=LED Morse Trigger
KCONFIG:=CONFIG_LEDS_TRIGGER_MORSE
FILES:=$(LINUX_DIR)/drivers/leds/ledtrig-morse.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-morse)
endef
define KernelPackage/ledtrig-morse/description
Kernel module to show morse coded messages on LEDs
endef
$(eval $(call KernelPackage,ledtrig-morse))
define KernelPackage/ledtrig-netdev
SUBMENU:=$(LEDS_MENU)
TITLE:=LED NETDEV Trigger
KCONFIG:=CONFIG_LEDS_TRIGGER_NETDEV
FILES:=$(LINUX_DIR)/drivers/leds/ledtrig-netdev.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-netdev)
endef
define KernelPackage/ledtrig-netdev/description
Kernel module to drive LEDs based on network activity
endef
$(eval $(call KernelPackage,ledtrig-netdev))
define KernelPackage/ledtrig-netfilter
SUBMENU:=$(LEDS_MENU)
TITLE:=LED NetFilter Trigger
DEPENDS:=kmod-ipt-core
KCONFIG:=CONFIG_NETFILTER_XT_TARGET_LED
FILES:=$(LINUX_DIR)/net/netfilter/xt_LED.ko
AUTOLOAD:=$(call AutoLoad,50,xt_LED)
endef
define KernelPackage/ledtrig-netfilter/description
Kernel module to flash LED when a particular packets passing through your machine.
For example to create an LED trigger for incoming SSH traffic:
iptables -A INPUT -p tcp --dport 22 -j LED --led-trigger-id ssh --led-delay 1000
Then attach the new trigger to an LED on your system:
echo netfilter-ssh > /sys/class/leds/<ledname>/trigger
endef
$(eval $(call KernelPackage,ledtrig-netfilter))
define KernelPackage/ledtrig-usbdev
SUBMENU:=$(LEDS_MENU)
TITLE:=LED USB device Trigger
DEPENDS:=@USB_SUPPORT kmod-usb-core
KCONFIG:=CONFIG_LEDS_TRIGGER_USBDEV
FILES:=$(LINUX_DIR)/drivers/leds/ledtrig-usbdev.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-usbdev)
endef
define KernelPackage/ledtrig-usbdev/description
Kernel module to drive LEDs based on USB device presence/activity
endef
$(eval $(call KernelPackage,ledtrig-usbdev))
define KernelPackage/ledtrig-default-on
SUBMENU:=$(LEDS_MENU)
TITLE:=LED Default ON Trigger
KCONFIG:=CONFIG_LEDS_TRIGGER_DEFAULT_ON
FILES:=$(LINUX_DIR)/drivers/leds/$(if $(call kernel_patchver_ge,3.10),trigger/)ledtrig-default-on.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-default-on,1)
endef
define KernelPackage/ledtrig-default-on/description
Kernel module that allows LEDs to be initialised in the ON state
endef
$(eval $(call KernelPackage,ledtrig-default-on))
define KernelPackage/ledtrig-timer
SUBMENU:=$(LEDS_MENU)
TITLE:=LED Timer Trigger
KCONFIG:=CONFIG_LEDS_TRIGGER_TIMER
FILES:=$(LINUX_DIR)/drivers/leds/$(if $(call kernel_patchver_ge,3.10),trigger/)ledtrig-timer.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-timer,1)
endef
define KernelPackage/ledtrig-timer/description
Kernel module that allows LEDs to be controlled by a programmable timer
via sysfs
endef
$(eval $(call KernelPackage,ledtrig-timer))
define KernelPackage/ledtrig-oneshot
SUBMENU:=$(LEDS_MENU)
TITLE:=LED One-Shot Trigger
DEPENDS:=@!LINUX_3_3
KCONFIG:=CONFIG_LEDS_TRIGGER_ONESHOT
FILES:=$(LINUX_DIR)/drivers/leds/$(if $(call kernel_patchver_ge,3.10),trigger/)ledtrig-oneshot.ko
AUTOLOAD:=$(call AutoLoad,50,ledtrig-oneshot)
endef
define KernelPackage/ledtrig-oneshot/description
Kernel module that allows LEDs to be triggered by sporadic events in
one-shot pulses
endef
$(eval $(call KernelPackage,ledtrig-oneshot))
define KernelPackage/leds-tlc59116
SUBMENU:=$(LEDS_MENU)
TITLE:=TLC59116 LED support
DEPENDS:=@TARGET_mvebu kmod-i2c-core
KCONFIG:=CONFIG_LEDS_TLC59116
FILES:=$(LINUX_DIR)/drivers/leds/leds-tlc59116.ko
AUTOLOAD:=$(call AutoLoad,60,leds-tlc59116,1)
endef
define KernelPackage/leds-tlc59116/description
Kernel module for LEDs on TLC59116
endef
$(eval $(call KernelPackage,leds-tlc59116))
|