# -*- mode: python; -*-
#============================================================================
# Example Python setup script for 'xm create'.
# This script sets the parameters used when a domain is created using 'xm create'.
#
# This is a relatively advanced script that uses a parameter, vmid, to control
# the settings. So this script can be used to start a set of domains by
# setting the vmid parameter on the 'xm create' command line. For example:
#
# xm create vmid=1
# xm create vmid=2
# xm create vmid=3
#
# The vmid is purely a script variable, and has no effect on the the domain
# id assigned to the new domain.
#============================================================================
# Define script variables here.
# xm_vars is defined automatically, use xm_vars.var() to define a variable.
# This function checks that 'vmid' has been given a valid value.
# It is called automatically by 'xm create'.
def vmid_check(var, val):
val = int(val)
if val <= 0:
raise ValueError
return val
# Define the 'vmid' variable so that 'xm create' knows about it.
xm_vars.var('vmid',
use="Virtual machine id. Integer greater than 0.",
check=vmid_check)
# Check the defined variables have valid values..
xm_vars.check()
#----------------------------------------------------------------------------
# Kernel image file.
kernel = "/path/to/domU/kernel"
# Optional ramdisk.
#ramdisk = "/boot/initrd.gz"
# The domain build function. Default is 'linux'.
#builder='linux'
# Initial memory allocation (in megabytes) for the new domain.
#
# WARNING: Creating a domain with insufficient memory may cause out of
# memory errors. The domain needs enough memory to boot kernel
# and modules. Allocating less than 32MBs is not recommended.
memory = 64
# A name for the new domain. All domains have to have different names,
# so we use the vmid to create a name.
name = "VM%d" % vmid
# 128-bit UUID for the domain. The default behavior is to generate a new UUID
# on each call to 'xm create'.
#uuid = "06ed00fe-1162-4fc4-b5d8-11993ee4a8b9"
# List of which CPUS this domain is allowed to use, default Xen picks
#cpus = "" # leave to Xen to pick
#cpus = "0" # all vcpus run on CPU0
#cpus = "0-3,5,^1" # all vcpus run on cpus 0,2,3,5
#cpus = ["2", "3"] # VCPU0 runs on CPU2, VCPU1 runs on CPU3
cpus = "%s" % vmid # set based on vmid (mod number of CPUs)
#----------------------------------------------------------------------------
# Define network interfaces.
# Optionally define mac and/or bridge for the network interfaces.
# Random MACs are assigned if not given.
vif = [ 'ip=192.168.%d.1/24' % (vmid)]
#----------------------------------------------------------------------------
# Define the disk devices you want the domain to have access to, and
# what you want them accessible as.
# Each disk entry is of the form phy:UNAME,DEV,MODE
# where UNAME is the device, DEV is the device name the domain will see,
# and MODE is r for read-only, w for read-write.
# This makes the disk device depend on the vmid - assuming
# tHat devices sda7, sda8 etc. exist. The device is exported
# to all domains as sda1.
# All domains get sda6 read-only (to use for /usr, see below).
disk = [ 'phy:hda%d,hda1,w' % (vmid)]
#----------------------------------------------------------------------------
# Define frame buffer device.
#
# By default, no frame buffer device is configured.
#
# To create one using the SDL backend and sensible defaults:
#
# vfb = [ 'sdl=1' ]
#
# This uses environment variables XAUTHORITY and DISPLAY. You
# can override that:
#
# vfb = [ 'sdl=1,xauthority=/home/bozo/.Xauthority,display=:1' ]
#
# To create one using the VNC backend and sensible defaults:
#
# vfb = [ 'vnc=1' ]
#
# The backend listens on 127.0.0.1 port 5900+N by default, where N is
# the domain ID. You can override both address and N:
#
# vfb = [ 'vnc=1,vnclisten=127.0.0.1,vncdisplay=%d' % vmid ]
#
# Or you can bind the first unused port above 5900:
#
# vfb = [ 'vnc=1,vnclisten=0.0.0.0,vncunused=1' ]
#
# You can override the password:
#
# vfb = [ 'vnc=1,vncpasswd=MYPASSWD' ]
#
# Empty password disables authentication. Defaults to the vncpasswd
# configured in xend-config.sxp.
#----------------------------------------------------------------------------
# Define to which TPM instance the user domain should communicate.
# The vtpm entry is of the form 'instance=INSTANCE,backend=DOM'
# where INSTANCE indicates the instance number of the TPM the VM
# should be talking to and DOM provides the domain where the backend
# is located.
# Note that no two virtual machines should try to connect to the same
# TPM instance. The handling of all TPM instances does require
# some management effort in so far that VM configration files (and thus
# a VM) should be associated with a TPM instance throughout the lifetime
# of the VM / VM configuration file. The instance number must be
# greater or equal to 1.
#vtpm = ['instance=%d,backend=0' % (vmid) ]
#----------------------------------------------------------------------------
# Set the kernel command line for the new domain.
# You only need to define the IP parameters and hostname if the domain's
# IP config doesn't, e.g. in ifcfg-eth0 or via DHCP.
# You can use 'extra' to set the runlevel and custom environment
# variables used by custom rc scripts (e.g. VMID=, usr= ).
# Set if you want dhcp to allocate the IP address.
dhcp="off"
ip="192.168.%d.2" % (vmid)
# Set netmask.
netmask="255.255.255.0"
# Set default gateway.
gateway="192.168.%d.1" % (vmid)
# Set the hostname.
hostname= "domain-%d.xeno" % vmid
# Set root device.
root = "/dev/hda1 ro"
# Root device for nfs.
#root = "/dev/nfs"
# The nfs server.
#nfs_server = "10.212.4.103"
# Root directory on the nfs server.
#nfs_root = "/path/to/root/filesystem"
# Sets runlevel 4 and the device for /usr.
extra = "4 VMID=%d" % vmid
#----------------------------------------------------------------------------
# Configure the behaviour when a domain exits. There are three 'reasons'
# for a domain to stop: poweroff, reboot, and crash. For each of these you
# may specify:
#
# "destroy", meaning that the domain is cleaned up as normal;
# "restart", meaning that a new domain is started in place of the old
# one;
# "preserve", meaning that no clean-up is done until the domain is
# manually destroyed (using xm destroy, for example); or
# "rename-restart", meaning that the old domain is not cleaned up, but is
# renamed and a new domain started in its place.
#
# In the event a domain stops due to a crash, you have the additional options:
#
# "coredump-destroy", meaning dump the crashed domain's core and then destroy;
# "coredump-restart', meaning dump the crashed domain's core and the restart.
#
# The default is
#
# on_poweroff = 'destroy'
# on_reboot = 'restart'
# on_crash = 'restart'
#
# For backwards compatibility we also support the deprecated option restart
#
# restart = 'onreboot' means on_poweroff = 'destroy'
# on_reboot = 'restart'
# on_crash = 'destroy'
#
# restart = 'always' means on_poweroff = 'restart'
# on_reboot = 'restart'
# on_crash = 'restart'
#
# restart = 'never' means on_poweroff = 'destroy'
# on_reboot = 'destroy'
# on_crash = 'destroy'
#on_poweroff = 'destroy'
#on_reboot = 'restart'
#on_crash = 'restart'
#-----------------------------------------------------------------------------
# Configure PVSCSI devices:
#
#vscsi=[ 'PDEV, VDEV' ]
#
# PDEV gives physical SCSI device to be attached to specified guest
# domain by one of the following identifier format.
# - XX:XX:XX:XX (4-tuples with decimal notation which shows
# "host:channel:target:lun")
# - /dev/sdxx or sdx
# - /dev/stxx or stx
# - /dev/sgxx or sgx
# - result of 'scsi_id -gu -s'.
# ex. # scsi_id -gu -s /block/sdb
# 36000b5d0006a0000006a0257004c0000
#
# VDEV gives virtual SCSI device by 4-tuples (XX:XX:XX:XX) as
# which the specified guest domain recognize.
#
#vscsi = [ '/dev/sdx, 0:0:0:0' ]
#============================================================================
156' href='#n156'>156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
/**CFile****************************************************************
FileName [bmcMaxi.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcMaxi.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManMaxiUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, f;
pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
// control/data variables
Gia_ManForEachRo( p, pObj, i )
Gia_ManAppendCi( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ManAppendCi( pNew );
// build timeframes
assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
Gia_ManForEachRo( p, pObj, i )
{
int Value = Vec_IntEntry( vInit, i );
int iCtrl = Gia_ManCiLit( pNew, i );
int iData = Gia_ManCiLit( pNew, Gia_ManRegNum(p)+i );
// decide based on Value
if ( Value == 0 )
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, iCtrl, iData) : 0;
else if ( Value == 1 )
pObj->Value = fUseVars ? Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData) : 1;
else if ( Value == 2 )
pObj->Value = Gia_ManHashAnd(pNew, iCtrl, iData);
else if ( Value == 3 )
pObj->Value = Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData);
else if ( Value == 4 )
pObj->Value = 0;
else if ( Value == 5 )
pObj->Value = 1;
else assert( 0 );
}
for ( f = 0; f < nFrames; f++ )
{
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachRi( p, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
}
Gia_ManForEachRi( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManMaxiPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
{
int nIterMax = 1000000;
int i, iLit, Iter, status;
int nLits, * pLits;
abctime clkTotal = Abc_Clock();
abctime clkSat = 0;
Vec_Int_t * vLits, * vMap;
sat_solver * pSat;
Gia_Obj_t * pObj;
Gia_Man_t * p0 = Gia_ManMaxiUnfold( p, nFrames, 0, vInit );
Gia_Man_t * p1 = Gia_ManMaxiUnfold( p, nFrames, 1, vInit );
Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
Gia_ManStop( p0 );
Gia_ManStop( p1 );
assert( Gia_ManRegNum(p) > 0 );
if ( fVerbose )
printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// add one large OR clause
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
Gia_ManForEachCo( pM, pObj, i )
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
// create assumptions
Vec_IntClear( vLits );
Gia_ManForEachPi( pM, pObj, i )
if ( i == Gia_ManRegNum(p) )
break;
else if ( Vec_IntEntry(vInit, i) == 0 || Vec_IntEntry(vInit, i) == 1 )
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
if ( fVerbose )
{
printf( "Iter%6d : ", 0 );
printf( "Var =%10d ", sat_solver_nvars(pSat) );
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
printf( "Subset =%6d ", Vec_IntSize(vLits) );
Abc_PrintTime( 1, "Time", clkSat );
// ABC_PRTr( "Solver time", clkSat );
}
for ( Iter = 0; Iter < nIterMax; Iter++ )
{
abctime clk = Abc_Clock();
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
clkSat += Abc_Clock() - clk;
if ( status == l_Undef )
{
// if ( fVerbose )
// printf( "\n" );
printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter );
break;
}
if ( status == l_True )
{
// if ( fVerbose )
// printf( "\n" );
printf( "The problem is SAT after %d iterations. ", Iter );
break;
}
assert( status == l_False );
nLits = sat_solver_final( pSat, &pLits );
if ( fVerbose )
{
printf( "Iter%6d : ", Iter+1 );
printf( "Var =%10d ", sat_solver_nvars(pSat) );
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
printf( "Subset =%6d ", nLits );
Abc_PrintTime( 1, "Time", clkSat );
// ABC_PRTr( "Solver time", clkSat );
}
if ( Vec_IntSize(vLits) == nLits )
{
// if ( fVerbose )
// printf( "\n" );
printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 );
break;
}
// collect used literals
Vec_IntClear( vLits );
for ( i = 0; i < nLits; i++ )
Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
}
// create map
vMap = Vec_IntStart( pCnf->nVars );
Vec_IntForEachEntry( vLits, iLit, i )
Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
// create output
Vec_IntFree( vLits );
vLits = Vec_IntDup(vInit);
Gia_ManForEachPi( pM, pObj, i )
if ( i == Gia_ManRegNum(p) )
break;
else if ( Vec_IntEntry(vLits, i) == 4 || Vec_IntEntry(vLits, i) == 5 )
Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) );
else if ( (Vec_IntEntry(vLits, i) == 0 || Vec_IntEntry(vLits, i) == 1) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) )
Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 );
Vec_IntFree( vMap );
// cleanup
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pM );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return vLits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManMaxiTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
{
Vec_Int_t * vRes, * vInit;
vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) );
vRes = Gia_ManMaxiPerform( p, vInit, nFrames, nTimeOut, fVerbose );
if ( vInit != vInit0 )
Vec_IntFree( vInit );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|