Changeset 45 for vis_dev


Ignore:
Timestamp:
Feb 20, 2012, 6:45:17 PM (13 years ago)
Author:
cecile
Message:

fichier biblio avec lien sur le compte verif

Location:
vis_dev/vis-2.3
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/vis-2.3/models/debug/and2.v

    r43 r45  
    11module andgate(clk,a,b);
    22input clk;
    3 input a;
    4 input b;
     3input [1:0]a;
     4input [1:0]b;
    55
    6 reg c;
    7 reg d;
     6reg [1:0]c;
     7reg [1:0]d;
    88
    99initial c = 0;
  • vis_dev/vis-2.3/src/debug/debug.c

    r44 r45  
    6666static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6767static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
     68static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6869
    6970
     
    9596  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
    9697  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
     98  Cmd_CommandAdd("_cexbdd",      CommandBuildCexBdd, 0);
    9799  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
    98100
     
    700702 return rel;
    701703}
    702 
     704mdd_t * buildDummy2(mdd_manager * mddManager)
     705{
     706 mdd_t * rel = NIL(mdd_t);
     707 mdd_t * state0 = mdd_one(mddManager);
     708 mdd_t * state2 = mdd_one(mddManager);
     709 mdd_t * state3 = mdd_one(mddManager);
     710  // state0 = s0
     711 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
     712 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
     713 state0 = mdd_and(s0,s1,1,1);
     714  // state2 = s2
     715 s0 =  mdd_eq_c(mddManager,0, 0);
     716 s1 =  mdd_eq_c(mddManager,2, 1);
     717 state2 = mdd_and(s0,s1,1,1);
     718  // state3 = s3
     719 s0 =  mdd_eq_c(mddManager,0, 1);
     720 s1 =  mdd_eq_c(mddManager,2, 1);
     721 state3 = mdd_and(s0,s1,1,1);
     722// Build transition relation
     723
     724 array_t * mvarVal = array_alloc(int,0);
     725 array_insert_last(int, mvarVal,2);
     726 array_t * val = array_alloc(int,0);
     727 array_t * mvarName = array_alloc(char*,0);
     728 array_insert_last(char*, mvarName,"S1");
     729 int e1Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
     730 array_insert(char*, mvarName,0,"I");
     731 int e0Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
     732 array_insert_last(int, val,1);
     733 mdd_t * e1 = mdd_literal(mddManager, e1Id,val);
     734 mdd_t * e0 = mdd_literal(mddManager, e0Id,val);
     735 mdd_t * tmp2 = mdd_and(e1,e0,0,0);
     736mdd_t *  ne2_1 = mdd_or(e1,tmp2,1,1);
     737mdd_t *  ne2_0 = mdd_and(e1,e0,0,1);
     738
     739array_insert(char*, mvarName,0,"Next_SI");
     740int id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
     741Mvf_Function_t * mvf = Mvf_FunctionAlloc(mddManager, 2);
     742Mvf_FunctionAddMintermsToComponent(mvf,1,ne2_1);
     743Mvf_FunctionAddMintermsToComponent(mvf,0,ne2_0);
     744mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, id);
     745
     746//bdd_print(relation);
     747mdd_FunctionPrintMain (mddManager ,relation,"news",vis_stdout);
     748 //bdd_ite
     749 return rel;
     750
     751}
    703752
    704753/**Function********************************************************************
     
    713762 
    714763  CommandDescription [This command create a new transition relation that is a
    715   and of the Bdd of the old one and an other bdd.
     764  and of the Bdd of the old one and another bdd.
    716765  <p>
    717766
     
    780829/* with the transtion relation     */
    781830/***********************************/
    782 rel = buildDummyBdd(mddManager);
     831rel = buildDummy3(mddManager,network);
    783832if(rel == NIL(mdd_t))
    784833{
    785         fprintf(vis_stdout,"Problem when building the new relation bdd");
     834        fprintf(vis_stdout,"Problem when building the new relation bdd\n");
    786835        return 1;
    787836}
     
    809858    int mddId = array_fetch(int, rangeVarMddIdArray, i);
    810859        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
     860    mdd_FunctionPrintMain (mddManager ,relation,"MVF",vis_stdout);
     861
    811862        mdd_t * n_relation = mdd_and(relation,rel,1,1);
    812863    /* Build for each possible value */
     
    820871                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
    821872                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
     873
    822874
    823875        }
     
    857909}
    858910
    859 
     911static int
     912CommandBuildCexBdd(Hrc_Manager_t ** hmgr,
     913                   int  argc, char ** argv){
     914int            c;
     915int            verbose = 0;              /* default value */
     916
     917/*
     918 * Parse command line options.
     919 */
     920util_getopt_reset();
     921while ((c = util_getopt(argc, argv, "vh")) != EOF) {
     922  switch(c) {
     923    case 'v':
     924      verbose = 1;
     925      break;
     926    case 'h':
     927      goto usage;
     928    default:
     929      goto usage;
     930  }
     931}
     932
     933if (verbose) {
     934  (void) fprintf(vis_stdout, "The _cexBdd is under construction.\n");
     935}
     936
     937Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
     938Ntk_Network_t  *network      = NIL(Ntk_Network_t);
     939mdd_manager    *mddManager;
     940mdd_t          *rel          = NIL(mdd_t);
     941int            i;
     942/******************/
     943network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     944if(network == NIL(Ntk_Network_t))
     945        return 1;
     946fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
     947if(fsm ==  NIL(Fsm_Fsm_t))
     948        return 1;
     949mddManager   = Fsm_FsmReadMddManager(fsm);
     950
     951
     952
     953/**********   Build cex  ***********/
     954/* Here add the function           */
     955/* that build the Bdd to and       */
     956/* with the transtion relation     */
     957/***********************************/
     958//rel = buildDummyBdd(mddManager);
     959array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
     960array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
     961
     962/** state0 = s0 **/
     963 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
     964 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
     965 mdd_t * state0 =  mdd_one(mddManager);
     966 state0 = mdd_and(s0,s1,1,1);
     967/** Next state1 = s2 + !s2  **/
     968
     969 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
     970 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
     971 mdd_t * state1 =  mdd_one(mddManager);
     972 state1 = mdd_and(ns0,ns1,1,1);
     973 state1 = mdd_or(state1,state1,1,0);
     974
     975/** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/
     976 rel =  mdd_one(mddManager);
     977 rel =  mdd_or(state0,state1,0,0);
     978/**********/
     979/** state0 = s2 **/
     980 mdd_t * s02 =  mdd_eq_c(mddManager,0, 0);
     981 mdd_t * s12 =  mdd_eq_c(mddManager,2, 1);
     982 mdd_t * state02 =  mdd_one(mddManager);
     983 state02 = mdd_and(s02,s12,1,1);
     984/** Next state1 = s3  **/
     985
     986 mdd_t * ns02 =  mdd_eq_c(mddManager,1, 1);
     987 mdd_t * ns12 =  mdd_eq_c(mddManager,3, 1);
     988 mdd_t * state12 =  mdd_one(mddManager);
     989 state12 = mdd_and(ns02,ns12,1,1);
     990
     991/** state = s0) -> !(Nextstate = s3) **/
     992 mdd_t * new_rel =  mdd_one(mddManager);
     993 new_rel =  mdd_or(state02,state12,0,0);
     994 rel = mdd_and(new_rel,rel,1,1);
     995 mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
     996
     997return 0;               /* normal exit */
     998
     999usage:
     1000(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
     1001(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
     1002(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
     1003return 1;               /* error exit */
     1004
     1005}
     1006
     1007
  • vis_dev/vis-2.3/src/debug/debug.make

    r36 r45  
    1 CSRC += debug.c debugUtilities.c debugAbnormal.c
     1CSRC += debug.c debugUtilities.c debugAbnormal.c debugNewBdd.c
    22HEADERS += debug.h debugInt.h
    33
  • vis_dev/vis-2.3/src/debug/debugAbnormal.c

    r44 r45  
    55
    66  Description [Create new primary input in the current network at a given
    7   output node.  Return the variable created]
     7  output node.  Return the node created]
    88
    99  SideEffects [Modify the network]
     
    1212
    1313******************************************************************************/
    14 Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk,Ntk_Node_t*
     14Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk, Ntk_Node_t*
    1515node, char * varName  )
    1616{
  • vis_dev/vis-2.3/src/debug/debugInt.h

    r44 r45  
    8787void printNodeArray(array_t * nodeArray);
    8888boolean Dbg_TestNodeInSubs(char* nodeName,array_t * subsName);
     89mdd_t * buildDummy3(mdd_manager * mddManager,Ntk_Network_t * ntk);
    8990
    9091/**AutomaticEnd***************************************************************/
Note: See TracChangeset for help on using the changeset viewer.