/**CFile*********************************************************************** FileName [puresatIPRefine.c] PackageName [puresat] Synopsis [Abstraction refinement for large scale invariant checking.] Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts: * Localization-reduction base Abstraction * K-induction or interpolation to prove the truth of a property * Bounded Model Checking to find bugs * Incremental concretization based methods to verify abstract bugs * Incremental SAT solver to improve efficiency * UNSAT proof based method to obtain refinement * AROSAT to bring in only necessary latches into unsat proofs * Bridge abstraction to get compact coarse refinement * Refinement minization to guarrantee minimal refinements * Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test * Refinement prediction to decrease the number of refinement iterations * Dynamic switching to redistribute computional resources to improve efficiency For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"] Author [Bing Li] Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.] ******************************************************************************/ #include "puresatInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Generate sufficient set from unsat proof] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ #if UNSATCORE void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager, satManager_t * cm, RTnode_t RTnode, st_table *ctTable, st_table *refineTable, FILE * fp) #else void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager, satManager_t * cm, RTnode_t RTnode, st_table *ctTable, st_table *refineTable) #endif { int i,ct; bAigTimeFrame_t *tf = manager->timeframeWOI; char *name; bAigEdge_t v,*lp; st_table *table; st_generator *stgen; RTManager_t * rm = cm->rm; if(RT_flag(RTnode)&RT_VisitedMask) return; RT_flag(RTnode) |= RT_VisitedMask; /*leaf*/ if(RT_pivot(RTnode)==0){ #if DBG assert(RT_oriClsIdx(RTnode)==0); #endif if(RT_oriClsIdx(RTnode)!=0) lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode)); else lp = RT_formula(RTnode) + cm->rm->fArray; for(i=0;iidx2name,(char*)v,&name)&& !st_lookup(tf->MultiLatchTable,(char*)v,&table)) continue; } #if 1 /* at least 2 times to be choosen as a candidate*/ if(st_lookup(ctTable,(char*)v,&ct)){ if(ct<0) continue; if(ct>=1){ if(!st_lookup(tf->MultiLatchTable,(char*)v,&table)){ int retVal = st_lookup(tf->idx2name,(char*)v,&name); assert(retVal); st_insert(refineTable,(char*)name,(char*)0); st_insert(ctTable,(char*)v,(char*)-1); } else{ #ifdef TIMEFRAME_VERIFY_ fprintf(vis_stdout,"%d is in MultiLatchTable: ",v); #endif st_foreach_item(table,stgen,(char**)&name, NIL(char*)){ #ifdef TIMEFRAME_VERIFY_ fprintf(vis_stdout,"%s ",name); #endif st_insert(refineTable,(char*)name,(char*)0); } #ifdef TIMEFRAME_VERIFY_ fprintf(vis_stdout,"\n"); #endif st_insert(ctTable,(char*)v,(char*)-1); } } } else{ ct=1; st_insert(ctTable,(char*)v,(char*)(long)ct); } #else retVal = st_lookup(tf->idx2name,(char*)v,(char**)&name); assert(retVal); st_insert(refineTable,(char*)name,(char*)0); #endif }/* if(SATflags(v)&StateBitMask){*/ } #if UNSATCORE fprintf(fp,"0\n"); #endif } /*non leaf*/ else{ assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL); #if UNSATCORE PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode), ctTable,refineTable,fp); PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode), ctTable,refineTable,fp); #else PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode), ctTable,refineTable); PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode), ctTable,refineTable); #endif } return; } /**Function******************************************************************** Synopsis [Generate sufficient set from unsat proof by bridge abstraction] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ //new pick latch #if UNSATCORE void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager, satManager_t * cm, RTnode_t RTnode, st_table *ctTable, st_table *refineTable, st_table *SufNameTable, FILE * fp) #else void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager, satManager_t * cm, RTnode_t RTnode, st_table *ctTable, st_table *refineTable, st_table *SufNameTable) #endif { int i,j,find,find1,times; bAigTimeFrame_t *tf = manager->timeframeWOI; char *name,*name1; bAigEdge_t v,v1,*lp,*lp1, *lp2, left,right; st_table *table; st_generator *stgen; RTManager_t * rm = cm->rm; long maxNode; if(RT_flag(RTnode)&RT_VisitedMask) return; RT_flag(RTnode) |= RT_VisitedMask; if(RT_pivot(RTnode)==0){ #if DBG assert(RT_oriClsIdx(RTnode)==0); #endif if(RT_oriClsIdx(RTnode)!=0) lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode)); else lp = RT_formula(RTnode) + cm->rm->fArray; lp1 = lp; (cm->line)++; for(i=0;iidx2name,(char*)v,&name)==0)&& (st_lookup(tf->MultiLatchTable,(char*)v,&table)==0)) continue; lp2 = lp1; left = SATnormalNode(leftChild(v)); right = SATnormalNode(rightChild(v)); //find largest node maxNode = -1; for(j=0;jMultiLatchTable,(char*)v,&table)){ int retVal = st_lookup(tf->idx2name,(char*)v,&name); assert(retVal); if(st_lookup(refineTable,(char*)name,×)) times++; st_insert(refineTable,(char*)name,(char*)(long)times); } /*for iden latches, we only add one, which is enough*/ else{ find = 0; find1 = 0; st_foreach_item(table,stgen,(char**)&name, NIL(char*)){ if(st_lookup(refineTable,name,NIL(char*))){ find = 1; break; } if(find1==0){ if(st_lookup(SufNameTable,name, NIL(char*))){ name1 = name; find1 = 1; } } } if(find==0){ times = 1; if(st_lookup(refineTable,(char*)name1,×)) times++; st_insert(refineTable,(char*)name1,(char*)(long)times); } } } } #if UNSATCORE fprintf(fp,"0\n"); #endif } /*non leaf*/ else{ assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL); #if UNSATCORE PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode), ctTable,refineTable,SufNameTable,fp); PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode), ctTable,refineTable,SufNameTable,fp); #else PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode), ctTable,refineTable,SufNameTable); PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode), ctTable,refineTable,SufNameTable); #endif } return; } /**Function******************************************************************** Synopsis [Generate sufficient set from unsat proof] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * PureSat_GetSufAbsFromCore(Ntk_Network_t *network, satManager_t * cm, PureSat_Manager_t *pm, bAigEdge_t property, st_table * SufAbsNameTable) { array_t * refArray = array_alloc(char *,0); char *name; st_generator *stgen; Ntk_Node_t *latch; bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); st_table * ctTable = st_init_table(st_numcmp,st_numhash); st_table * refineTable = st_init_table(strcmp,st_strhash); int times; #if UNSATCORE FILE * fp = fopen("unsatcore.txt","w"); #endif #if LAI st_table * refineTable1 = st_init_table(strcmp,st_strhash); #endif PureSat_CleanMask(manager,ResetVisited1234NewMask); #if UNSATCORE fprintf(fp,"p cnf %d line, # nodes:%d\n", cm->initNumVariables,cm->nodesArraySize); cm->line = 0; PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root, ctTable,refineTable,SufAbsNameTable,fp); fprintf(fp,"total lines: %d\n",cm->line); #else PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root, ctTable,refineTable,SufAbsNameTable); #endif PureSat_CleanMask(manager,ResetVisited1234NewMask); #if LAI ResetRTree(cm->rm); PureSat_GetLIAForNode(manager,property); PureSat_GetSufAbsByLIA(manager,cm,cm->rm->root, refineTable1); #endif st_foreach_item(refineTable,stgen,&name,×){ latch = Ntk_NetworkFindNodeByName(network,name); if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&& st_lookup(pm->SufAbsTable, (char*)latch,NIL(char*))){ array_insert_last(char *,refArray,name); if(pm->verbosity>=2) fprintf(vis_stdout,"ref cand:%s %d\n",name,times); } } #if LAI st_foreach_item(refineTable1,stgen,(char**)&name,NIL(char*)){ latch = Ntk_NetworkFindNodeByName(network,name); if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&& st_lookup(pm->CoiTable, (char*)latch,NIL(char*))){ if(pm->verbosity>=2) fprintf(vis_stdout,"from LIA ref candidate:%s\n",name); } } #endif #if UNSATCORE fclose(fp); #endif st_free_table(ctTable); st_free_table(refineTable); #if LAI st_free_table(refineTable1); #endif return refArray; } /**Function******************************************************************** Synopsis [Main procedure of refinement computation] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t *PureSat_RefineOnAbs(Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property, array_t *previousResultArray, int latchThreshHold, int * sccArray, array_t * sufArray) { array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3; array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2; satManager_t *cm; mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); st_table *table; char * name; int i,j; int NumInSecondLevel; st_generator *stgen; Ntk_Node_t *latch; double t1,t2,t3,t4; st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash); st_table * junkTable; int noArosat = 1; tmpRef = array_alloc(char *,0); st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){ name = Ntk_NodeReadName(latch); if(st_lookup(pm->vertexTable,name,NIL(char *))) array_insert_last(char *,tmpModel,name); array_insert_last(char *,tmpRef,name); st_insert(SufAbsNameTable,name,(char *)0); } t1 = util_cpu_ctime(); manager->assertArray = sat_ArrayAlloc(1); sat_ArrayInsert(manager->assertArray,manager->InitState); cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray); if(pm->Arosat){ cm->option->decisionHeuristic &= RESET_LC; cm->option->decisionHeuristic |= DVH_DECISION; cm->option->arosat = 1; } cm->option->coreGeneration = 1; cm->option->AbRf = 1; cm->property = property; cm->option->IP = 1; PureSat_CleanMask(manager,ResetVisibleVarMask); PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1); array_free(tmpRef); t3 = util_cpu_ctime(); PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length); t4 = util_cpu_ctime(); pm->tPro += t4-t3; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t4-t3)/1000.0),pm->tPro/1000); if(cm->option->arosat){ PureSatCreateLayer(network,pm,cm,tmpModel,sufArray); cm->Length = pm->Length; AS_Main(cm); noArosat = 0; st_foreach_item(cm->layerTable,stgen,&table,NIL(char*)) st_free_table(table); st_free_table(cm->layerTable); FREE(cm->assignedArray); FREE(cm->numArray); } else sat_Main(cm); manager->NodesArray = cm->nodesArray;; assert(cm->status==SAT_UNSAT); t3 = util_cpu_ctime(); PureSatPostprocess(manager,cm,pm); PureSatProcessDummy(manager,cm,cm->rm->root); ResetRTree(cm->rm); t4 = util_cpu_ctime(); pm->tPro += t4-t3; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t4-t3)/1000.0),pm->tPro/1000); t2 = util_cpu_ctime(); pm->tCoreGen += t2 - t1; if(pm->verbosity>=2) fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n", (double)(t2-t1)/1000.0,pm->tCoreGen/1000.0); t1 = util_cpu_ctime(); tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable); t2 = util_cpu_ctime(); st_free_table(SufAbsNameTable); RT_Free(cm->rm); sat_ArrayFree(manager->assertArray); PureSat_SatFreeManager(cm); /*Get suff set*/ tmpRef2 = array_alloc(char *,0); tmpRef3 = array_alloc(char *,0); tmpArray1 = array_alloc(char *,0); tmpArray2 = array_alloc(char *,0); if(noArosat){ t1 = util_cpu_ctime(); if(array_n(tmpRef1)){ tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1, &NumInSecondLevel); array_free(pm->latchArray); } } else{ if(array_n(tmpRef1)){ tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1, &NumInSecondLevel); array_free(pm->latchArray); } else tmpRef = array_alloc(char*,0); #if NOREFMIN if(pm->verbosity>=1){ fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n"); arrayForEachItem(char *,tmpRef,i,name) fprintf(vis_stdout,"%s\n",name); } PureSatAddIdenLatchToAbs(network,pm,tmpRef); array_free(tmpRef1); array_free(tmpModel); return tmpRef; #endif } /*Ref Minimization //try all the candidates*/ t1 = util_cpu_ctime(); if(pm->CoreRefMin && array_n(tmpRef)>=5){ if(pm->verbosity>=1) fprintf(vis_stdout,"Core Ref Min\n"); junkTable = st_init_table(strcmp,st_strhash); for(i=array_n(tmpRef)-1;i>=0;i--) { array_t * tmpA; name = array_fetch(char *,tmpRef,i); if(pm->verbosity>=1) fprintf(vis_stdout,"RefMin: testing %s\n",name); tmpArray2 = PureSatRemove_char(tmpRef,i); if(st_lookup(junkTable,name,NIL(char))){ array_free(tmpRef); tmpRef = tmpArray2; if(pm->verbosity>=1) fprintf(vis_stdout,"%s is junk\n",name); continue; } tmpA = array_dup(tmpModel); array_append(tmpA,tmpArray2); t3 = util_cpu_time(); tmpArray1 = array_alloc(char*,0); arrayForEachItem(char*,tmpA,j,name) if(!st_lookup(junkTable,name,NIL(char))) array_insert_last(char*,tmpArray1,name); array_free(tmpA); if(!PureSat_ConcretTest_Core(network,pm,tmpArray1,property, previousResultArray,junkTable)){ /*then the candidate can' be deleted*/ t4 = util_cpu_time(); if(pm->verbosity>=2) fprintf(vis_stdout," %g\n",(t4-t3)/1000); array_free(tmpArray2); } else /*delete it*/ { t4 = util_cpu_time(); if(pm->verbosity>=2) fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000); array_free(tmpRef); tmpRef = tmpArray2; } array_free(tmpArray1); } st_free_table(junkTable); } else{ for(i=array_n(tmpRef)-1;i>=0;i--) { name = array_fetch(char *,tmpRef,i); if(pm->verbosity>=1) fprintf(vis_stdout,"RefMin: testing %s\n",name); tmpArray2 = PureSatRemove_char(tmpRef,i); tmpArray1 = array_dup(tmpModel); array_append(tmpArray1,tmpArray2); t3 = util_cpu_time(); if(!PureSat_ConcretTest(network,pm,tmpArray1,property, previousResultArray,0,0,0)){ t4 = util_cpu_time(); if(pm->verbosity>=2) fprintf(vis_stdout," %g\n",(t4-t3)/1000); array_free(tmpArray2); } else /*delete it*/ { t4 = util_cpu_time(); if(pm->verbosity>=2) fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000); array_free(tmpRef); tmpRef = tmpArray2; } array_free(tmpArray1); } } t2 = util_cpu_ctime(); pm->tRefMin += t2 - t1; if(pm->verbosity>=2) fprintf(vis_stdout,"\ntime for Ref Min: %g, total:%g\n", (t2-t1)/1000,pm->tRefMin/1000); if(pm->verbosity>=1){ fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n"); arrayForEachItem(char *,tmpRef,i,name) fprintf(vis_stdout,"%s\n",name); } PureSatAddIdenLatchToAbs(network,pm,tmpRef); array_free(tmpRef1); array_free(tmpModel); return tmpRef; } /**Function******************************************************************** Synopsis [Refinement procedure without refinement minimization] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t *PureSat_RefineOnAbs_DA(Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property, array_t *previousResultArray, int latchThreshHold, int * sccArray, array_t * sufArray) { array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3; //= array_alloc(char *,0); array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2; satManager_t *cm; mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network); st_table *table; char * name; int i; int NumInSecondLevel; st_generator *stgen; Ntk_Node_t *latch; double t1,t2,t3,t4; st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash); int noArosat = 1; tmpRef = array_alloc(char *,0); st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){ name = Ntk_NodeReadName(latch); if(st_lookup(pm->vertexTable,name,NIL(char *))) array_insert_last(char *,tmpModel,name); array_insert_last(char *,tmpRef,name); st_insert(SufAbsNameTable,name,(char *)0); } t1 = util_cpu_ctime(); manager->assertArray = sat_ArrayAlloc(1); sat_ArrayInsert(manager->assertArray,manager->InitState); cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray); #if AROSAT cm->option->decisionHeuristic &= RESET_LC; cm->option->decisionHeuristic |= DVH_DECISION; cm->option->arosat = 1; #endif cm->option->coreGeneration = 1; cm->option->AbRf = 1; cm->option->IP = 1; cm->property = property; PureSat_CleanMask(manager,ResetVisibleVarMask); PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1); array_free(tmpRef); t3 = util_cpu_ctime(); PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length); t4 = util_cpu_ctime(); pm->tPro += t4-t3; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t4-t3)/1000.0),pm->tPro/1000); #if DBG PureSatCheckCoi(manager); #endif if(cm->option->arosat){ PureSatCreateLayer(network,pm,cm,tmpModel,sufArray); cm->Length = pm->Length; AS_Main(cm); noArosat = 0; st_foreach_item(cm->layerTable,stgen,&table,NIL(char*)) st_free_table(table); st_free_table(cm->layerTable); FREE(cm->assignedArray); FREE(cm->numArray); } else sat_Main(cm); manager->NodesArray = cm->nodesArray;; assert(cm->status==SAT_UNSAT); t3 = util_cpu_ctime(); PureSatPostprocess(manager,cm,pm); PureSatProcessDummy(manager,cm,cm->rm->root); ResetRTree(cm->rm); t4 = util_cpu_ctime(); pm->tPro += t4-t3; if(pm->verbosity>=2) fprintf(vis_stdout,"process time:%g,total:%g\n", (double)((t4-t3)/1000.0),pm->tPro/1000); t2 = util_cpu_ctime(); pm->tCoreGen += t2 - t1; if(pm->verbosity>=2) fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n", (double)(t2-t1)/1000.0,pm->tCoreGen/1000.0); #if DBG PureSat_CheckFanoutFanin(manager); #endif t1 = util_cpu_ctime(); tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable); t2 = util_cpu_ctime(); st_free_table(SufAbsNameTable); RT_Free(cm->rm); sat_ArrayFree(manager->assertArray); PureSat_SatFreeManager(cm); /*Get suff set*/ tmpRef2 = array_alloc(char *,0); tmpRef3 = array_alloc(char *,0); tmpArray1 = array_alloc(char *,0); tmpArray2 = array_alloc(char *,0); if(noArosat){ t1 = util_cpu_ctime(); if(array_n(tmpRef1)){ tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1, &NumInSecondLevel); array_free(pm->latchArray); } } /*if arosat*/ else{ if(array_n(tmpRef1)){ tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1, &NumInSecondLevel); array_free(pm->latchArray); } else tmpRef = array_alloc(char*,0); if(pm->verbosity>=1){ fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n"); arrayForEachItem(char *,tmpRef,i,name) fprintf(vis_stdout,"%s\n",name); } PureSatAddIdenLatchToAbs(network,pm,tmpRef); array_free(tmpRef1); array_free(tmpModel); return tmpRef; } }