/**CFile*********************************************************************** FileName [eqvCmd.c] PackageName [eqv] Synopsis [Implements the eqv commands.] Description [This file initializes the eqv package and provides the interface between the command line and the top level routine which does the equivalence checking.] Author [Shaz Qadeer] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. 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. IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] ******************************************************************************/ #include "eqvInt.h" static char rcsid[] UNUSED = "$Id: eqvCmd.c,v 1.20 2009/04/11 18:26:04 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static jmp_buf timeOutEnv; /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int CommandCombEquivalence(Hrc_Manager_t **hmgr, int argc, char **argv); static int CommandSeqEquivalence(Hrc_Manager_t **hmgr, int argc, char **argv); static void TimeOutHandle(void); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [This function initializes the eqv package.] SideEffects [] SeeAlso [Eqv_End()] ******************************************************************************/ void Eqv_Init(void) { Cmd_CommandAdd("comb_verify", CommandCombEquivalence, 0); Cmd_CommandAdd("seq_verify", CommandSeqEquivalence, 0); } /**Function******************************************************************** Synopsis [This function ends the eqv package.] SideEffects [] SeeAlso [Eqv_Init()] ******************************************************************************/ void Eqv_End(void) { } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [This function sits between the command line and the top level function which checks combinational equivalence.] Description [The function parses the command line and generates the arguments to the top level routine.] SideEffects [If the variables of the network present at the current node of the existing hierarchy have not been ordered, they get ordered.] SeeAlso [Eqv_NetworkVerifyCombinationalEquivalence] CommandName [comb_verify] CommandSynopsis [verify the combinational equivalence of two flattened networks] CommandArguments [ \[-b\] \[-f <filename>\] \[-h\] \[-o <ordering method>\] \[-t <timeOut>\] \[-1 <partition method>\] \[-2 <partition method>\] \[-i\] <filename1> \[<filename2>\] ] CommandDescription [This command verifies the combinational equivalence of two flattened networks. In particular, any set of functions (the roots), defined over any set of intermediate variables (the leaves), can be checked for equivalence between the two networks. Roots and leaves are subsets of the nodes of a network, with the restriction that the leaves should form a complete support for the roots. The correspondence between the roots and the leaves in the two networks is specified in a file given by the option -f . The default option assumes that the roots are the combinational outputs and the leaves are the combinational inputs.

When there is a pseudo input in the set of leaves, the range of values it can take should be the same as that of the multi-valued variable corresponding to it, for comb_verify to function correctly. This restriction will be removed in future.

There are two ways to do combinational verification. In the first mode, two BLIF-MV files are given as arguments to the command, e.g.

  vis> comb_verify foo.mv bar.mv
Verification is done for the flattened networks at the root nodes of the two BLIF-MV hierarchies. In any error messages printed, "network1" refers to the first file, and "network2" refers to the second. Both of these networks are freed at the end of the command. This mode is totally independent from any existing hierarchy previously read in. In the second mode, it is assumed that a hierarchy has already been read in. Then, comb_verify can be called with a single BLIF-MV file, and this will do the comparison between the network present at the current node ("network1") and the network corresponding to the root node of the hierarchy in the BLIF-MV file("network2"). A typical sequence of commands is:

  vis> read_blifmv foo.mv
  vis> init_verify
  vis> comb_verify bar.mv
If a hierarchy has been read in but a flattened network does not exist at the current node (flatten_hierarchy has not been invoked), the command does nothing. If a network exists at the current node, but the variables haven't been ordered, then the variables are ordered and a partition created. This partition is freed at the end. A side-effect is that the variables are ordered. If a partition exists, then it is used if the vertices corresponding to the roots specified are present in it, otherwise a new partition is created with the current ordering. The partition created for the new network read in is always freed at the end.

Command options:

-b
Specifies that the files are BLIF files and not BLIF-MV files.

-f <filename>
Provides the correspondence between the leaves and roots of network1 and network2. If this option is not used, it is assumed that the correspondence is by name, except that two latch inputs match if either they have the same name or the corresponding latch outputs have the same name. Leaves are the combinational inputs, and roots are the combinational outputs.

-h
Print the command usage.

-t <timeOut>
Time in seconds allowed to perform equivalence checking. The default is infinity.

-o <ordering method>
Specifies the ordering method to be used for assigning a common ordering to the leaves of network1 and network2. If this option is not used, ordering is done using a default method. Currently, only the default method is available.

-1 <partition method>
Specifies the partitioning method to be used for network1. Supported methods are "total", "partial", and "inout" (see the command build_partition_mdds for more information). If this option is not specified, then the default method "inout" is used.

-2 <partition method>
Specifies the partitioning method to be used for network2. Supported methods are "total", "partial", and "inout" (see the command build_partition_mdds for more information). If this option is not specified, then default method "inout" is used.

-i
Print Bdd statistics.
] ******************************************************************************/ static int CommandCombEquivalence( Hrc_Manager_t **hmgr, int argc, char **argv) { static int timeOutPeriod; static Hrc_Manager_t *hmgr1; static Hrc_Manager_t *hmgr2; static Ntk_Network_t *network1; static Ntk_Network_t *network2; int c; int check; FILE *fp; FILE *inputFile = NIL(FILE); char *fileName1; char *fileName2; char *name1; char *name2; st_generator *gen; static Part_PartitionMethod partMethod1; static Part_PartitionMethod partMethod2; static OFT AssignCommonOrder; static st_table *inputMap; static st_table *outputMap; st_table *rootsTable = NIL(st_table); st_table *leavesTable = NIL(st_table); boolean fileFlag = FALSE; boolean equivalent; boolean printBddInfo = FALSE; static boolean execMode; /* FALSE: verify against current network, TRUE: verify the two given networks */ boolean isBlif = FALSE; /* * These are the default values. These variables must be declared static * to avoid lint warnings. Since they are static, we must reinitialize * them outside of the variable declarations. */ timeOutPeriod = 0; hmgr1 = NIL(Hrc_Manager_t); hmgr2 = NIL(Hrc_Manager_t); partMethod1 = Part_Default_c; partMethod2 = Part_Default_c; AssignCommonOrder = DefaultCommonOrder; inputMap = NIL(st_table); outputMap = NIL(st_table); error_init(); util_getopt_reset(); while((c = util_getopt(argc, argv, "bf:o:1:2:ht:i")) != EOF) { switch(c) { case 'b': isBlif = TRUE; break; case 'f': if((inputFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found.\n", util_optarg); goto usage; } fileFlag = 1; break; case 'o': /* The following line causes a seg fault, because FindOrderingMethod() always returns NULL, and currently only DefaultCommonOrder is used. AssignCommonOrder = FindOrderingMethod(); */ /* The programmer supplies and modifies this function if any new ordering method is introduced. FindOrderingMethod() should return the type OFT. */ break; case 't': timeOutPeriod = atoi(util_optarg); break; case '1': if(!strcmp(util_optarg, "total")) { partMethod1 = Part_Total_c; } else if(!strcmp(util_optarg, "partial")) { partMethod1 = Part_Partial_c; } else if(!strcmp(util_optarg, "inout")) { partMethod1 = Part_InOut_c; } else { (void) fprintf(vis_stderr, "** eqv error: Unknown partition method 1\n"); goto usage; } break; case '2': if(!strcmp(util_optarg, "total")) { partMethod2 = Part_Total_c; } else if(!strcmp(util_optarg, "partial")) { partMethod2 = Part_Partial_c; } else if(!strcmp(util_optarg, "inout")) { partMethod2 = Part_InOut_c; } else { (void) fprintf(vis_stderr, "** eqv error: Unknown partition method 2\n"); goto usage; } break; case 'i': printBddInfo = TRUE; break; case 'h': goto usage; default : goto usage; } } if(argc == 1) { goto usage; } if(argc == util_optind+1) { execMode = FALSE; } else if(argc == util_optind+2) { execMode = TRUE; } else { error_append("** eqv error: Improper number of arguments.\n"); (void) fprintf(vis_stderr, "%s", error_string()); goto usage; } if(execMode == FALSE) { hmgr1 = *hmgr; if(Hrc_ManagerReadCurrentNode(hmgr1) == NIL(Hrc_Node_t)) { (void) fprintf(vis_stderr, "** eqv error: The hierarchy manager is empty. Read in design.\n"); return 1; } network1 = (Ntk_Network_t *) Hrc_NodeReadApplInfo( Hrc_ManagerReadCurrentNode(hmgr1), NTK_HRC_NODE_APPL_KEY); if(network1 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: There is no network. Use flatten_hierarchy.\n"); return 1; } if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) == NIL(void)) { (void) fprintf(vis_stderr, "** eqv error: Network has not been partitioned. Use build_partition_mdds.\n"); return 1; } fileName2 = argv[util_optind]; if(isBlif) { if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); goto usage; } } else { if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); return 1; } hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); fclose(fp); if(hmgr2 == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); return 1; } } network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), TRUE, (lsList) NULL); if(network2 == NIL(Ntk_Network_t)) { Hrc_ManagerFree(hmgr2); (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); return 1; } } else { fileName1 = argv[util_optind]; fileName2 = argv[util_optind+1]; if(isBlif) { if((hmgr1 = Io_BlifRead(fileName1, FALSE)) == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); return 1; } if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); if(hmgr1) { Hrc_ManagerFree(hmgr1); } return 1; } } else { if((fp = Cmd_FileOpen(fileName1, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName1); return 1; } hmgr1 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); fclose(fp); if(hmgr1 == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); goto usage; } if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); if(hmgr1) { Hrc_ManagerFree(hmgr1); } return 1; } hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); fclose(fp); if(hmgr2 == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); if(hmgr1) { Hrc_ManagerFree(hmgr1); } return 1; } } network1 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr1), TRUE, (lsList) NULL); network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), TRUE, (lsList) NULL); if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) { if(network1 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n"); } if(network2 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); } Hrc_ManagerFree(hmgr1); Hrc_ManagerFree(hmgr2); return 1; } if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) { if(network1 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n"); } if(network2 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); } Hrc_ManagerFree(hmgr1); Hrc_ManagerFree(hmgr2); return 1; } } if(Ntk_NetworkReadNumCombInputs(network1) != Ntk_NetworkReadNumCombInputs(network2)) { error_append("** eqv error: Different number of inputs in the two networks.\n"); if(!fileFlag) { if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); return 1; } } if(fileFlag) { rootsTable = st_init_table(strcmp, st_strhash); leavesTable = st_init_table(strcmp, st_strhash); check = ReadRootLeafMap(inputFile, rootsTable, leavesTable); fclose(inputFile); switch (check) { case 0 : /* error */ st_free_table(rootsTable); st_free_table(leavesTable); (void) fprintf(vis_stderr, "** eqv error: No data in the input file.\n"); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; case 1 : /* leaves only */ st_free_table(rootsTable); inputMap = MapNamesToNodes(network1, network2, leavesTable); st_foreach_item(leavesTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(leavesTable); if(inputMap == NIL(st_table)) { (void) fprintf(vis_stderr, "%s", error_string()); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } if((outputMap = MapCombOutputsByName(network1, network2)) == NIL(st_table)) { st_free_table(inputMap); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); return 1; } if(!TestRootsAndLeavesAreValid(network1, network2, inputMap, outputMap)){ st_free_table(inputMap); st_free_table(outputMap); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); return 1; } break; case 2 : /* roots only */ st_free_table(leavesTable); outputMap = MapNamesToNodes(network1, network2, rootsTable); st_foreach_item(rootsTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(rootsTable); if(outputMap ==NIL(st_table)) { (void) fprintf(vis_stderr, "%s", error_string()); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } if((inputMap = MapCombInputsByName(network1, network2)) == NIL(st_table)) { st_free_table(outputMap); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); return 1; } if(!TestRootsAndLeavesAreValid(network1, network2, inputMap, outputMap)){ st_free_table(inputMap); st_free_table(outputMap); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } break; case 3 : /* both leaves and roots */ inputMap = MapNamesToNodes(network1, network2, leavesTable); st_foreach_item(leavesTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(leavesTable); outputMap = MapNamesToNodes(network1, network2, rootsTable); st_foreach_item(rootsTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(rootsTable); if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) { (void) fprintf(vis_stderr, "%s", error_string()); if(inputMap) { st_free_table(inputMap); } if(outputMap) { st_free_table(outputMap); } if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } if(!TestRootsAndLeavesAreValid(network1, network2, inputMap, outputMap)){ st_free_table(inputMap); st_free_table(outputMap); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); return 1; } break; } } else { inputMap = MapCombInputsByName(network1, network2); outputMap = MapCombOutputsByName(network1, network2); if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) { if(inputMap) { st_free_table(inputMap); } if(outputMap) { st_free_table(outputMap); } if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); return 1; } } /* Start the timer before calling the equivalence checker. */ if (timeOutPeriod > 0){ (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(timeOutPeriod); if (setjmp(timeOutEnv) > 0) { (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod); alarm(0); return 1; } } equivalent = Eqv_NetworkVerifyCombinationalEquivalence(network1, network2, inputMap, outputMap, AssignCommonOrder, partMethod1, partMethod2); if(equivalent) { (void) fprintf(vis_stdout, "Networks are combinationally equivalent.\n\n"); } else { (void) fprintf(vis_stdout, "%s", error_string()); (void) fprintf(vis_stdout, "Networks are NOT combinationally equivalent.\n\n"); } if (printBddInfo) { bdd_print_stats(Ntk_NetworkReadMddManager(network1), vis_stdout); } st_free_table(inputMap); st_free_table(outputMap); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); alarm(0); return 0; /* normal exit */ usage: (void) fprintf(vis_stderr, "usage: comb_verify [-b] [-f filename] [-h] [-o ordering method] [-t time]\n"); (void) fprintf(vis_stderr, " [-1 partMethod1] [-2 partMethod2] [-i] file1 [file2]\n"); (void) fprintf(vis_stderr, " -b input files are BLIF\n"); (void) fprintf(vis_stderr, " -f file variable name correspondence file\n"); (void) fprintf(vis_stderr, " -h print the command usage\n"); (void) fprintf(vis_stderr, " -o method variable ordering method\n"); (void) fprintf(vis_stderr, " -t time time out period (in seconds)\n"); (void) fprintf(vis_stderr, " -1 method partitioning method for network1\n"); (void) fprintf(vis_stderr, " -2 method partitioning method for network2\n"); (void) fprintf(vis_stderr, " -i print Bdd statistics\n"); return 1; /* error exit */ } /**Function******************************************************************** Synopsis [This function sits between the command line and the main routine of sequential verification.] Description [The function parses the command line.] SideEffects [] SeeAlso [Eqv_NetworkVerifySequentialEquivalence] CommandName [seq_verify] CommandSynopsis [verify the sequential equivalence of two flattened networks] CommandArguments [\[-b\] \[-f <filename>\] \[-h\] \[-p <partition method>\] \[-t <timeOut>\] \[-B\] \[-i\] \[-r\] <filename> \[<filename>\]] CommandDescription [Please read the documentation for the command comb_verify before reading on. The concepts of roots and leaves in this command are the same as for comb_verify, except for an added constraint: the set of leaves has to be the set of all primary inputs. This obviously produces the constraint that both networks have the same number of primary inputs. Moreover, no pseudo inputs should be present in the two networks being compared. The set of roots can be an arbitrary subset of nodes.

The command verifies whether any state, where the values of two corresponding roots differ, can be reached from the set of initial states of the product machine. If this happens, a debug trace is provided.

The sequential verification is done by building the product finite state machine.

The command has two execution modes, just as for comb_verify. In the first mode, two BLIF-MV files are given as arguments to the command:

  vis> seq_verify foo.mv bar.mv
In the second mode, a single BLIF-MV file is taken. This is network2. It is assumed that network1 is from a hierarchy that has already been read in. If a network is present at the current node (i.e. flatten_hierarchy has been executed), it is used for verification; otherwise the command does nothing.

  vis> read_blifmv foo.mv
  vis> flatten_hierarchy
  vis> seq_verify bar.mv
Command options:

-b
Specifies that the input files are BLIF files.

-f <filename>
Provides the correspondence between the leaves and roots of network1 and network2. leaves has to be the set of primary inputs of the networks. roots can be any subset of nodes. If this option is not used, it is assumed that the correspondence is by name, and that the roots are the combinational outputs.

-h
Print the command usage.

-p <partition method>
Specifies the partitioning method for the product machine. Supported methods are "total", "partial", and "inout" (see the command build_partition_mdds for more information). If this option is not specified, then the default method "inout" is used.

-t <timeOut>
Time in seconds allowed to perform equivalence checking. The default is infinity.

-B
Use backward image computation to traverse the state space of the product machine. By default, forward image computaion is used.
-i
Print BDD statistics. This is the only way to see BDD stastics during this command. print_bdd_stats after this command doesn't show information related to this command.
-r
Enable BDD reordering during the equivalence check. Note that dynamic_var_ordering has no effect on whether reordering is enabled during the execution of seq_verify.
] ******************************************************************************/ static int CommandSeqEquivalence( Hrc_Manager_t **hmgr, int argc, char **argv) { static int timeOutPeriod; static Hrc_Manager_t *hmgr1; static Hrc_Manager_t *hmgr2; static Ntk_Network_t *network1; static Ntk_Network_t *network2; int c; int check; FILE *fp; static FILE *inputFile; char *fileName1; char *fileName2; char *name1; char *name2; st_generator *gen; static Part_PartitionMethod partMethod; st_table *outputMap = NIL(st_table); st_table *inputMap = NIL(st_table); st_table *rootsTable = NIL(st_table); st_table *leavesTable = NIL(st_table); static boolean fileFlag; static boolean execMode; /* FALSE: verify against the current network, TRUE: verify the two networks */ static boolean equivalent; boolean isBlif = FALSE; boolean printBddInfo = FALSE; static boolean useBackwardReach; boolean reordering = FALSE; /* * These are the default values. These variables must be declared static * to avoid lint warnings. Since they are static, we must reinitialize * them outside of the variable declarations. */ timeOutPeriod = 0; hmgr1 = NIL(Hrc_Manager_t); hmgr2 = NIL(Hrc_Manager_t); inputFile = NIL(FILE); partMethod = Part_Default_c; fileFlag = FALSE; equivalent = FALSE; useBackwardReach = FALSE; error_init(); util_getopt_reset(); while((c = util_getopt(argc, argv, "bBf:p:hFt:ir")) != EOF) { switch(c) { case 'b': isBlif = TRUE; break; case 'f': if((inputFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found.\n", util_optarg); return 1; } fileFlag = 1; break; case 'p': if(!strcmp(util_optarg, "total")) { partMethod = Part_Total_c; } else { if(!strcmp(util_optarg, "partial")) { partMethod = Part_Partial_c; } else { if(!strcmp(util_optarg, "inout")) { partMethod = Part_InOut_c; } else { (void) fprintf(vis_stderr, "** eqv error: Unknown partition method\n"); goto usage; } } } break; case 't': timeOutPeriod = atoi(util_optarg); break; case 'B': useBackwardReach = TRUE; break; case 'h': goto usage; case 'i': printBddInfo = TRUE; break; case 'r': reordering = TRUE; break; default: goto usage; } } if(argc == 1) { goto usage; } if(argc == util_optind+1) { execMode = FALSE; } else if(argc == util_optind+2) { execMode = TRUE; } else { error_append("** eqv error: Improper number of arguments.\n"); (void) fprintf(vis_stderr, "%s", error_string()); goto usage; } if(execMode == FALSE) { hmgr1 = *hmgr; if(Hrc_ManagerReadCurrentNode(hmgr1) == NIL(Hrc_Node_t)) { (void) fprintf(vis_stderr, "** eqv error: The hierarchy manager is empty. Read in design.\n"); return 1; } network1 = (Ntk_Network_t *) Hrc_NodeReadApplInfo( Hrc_ManagerReadCurrentNode(hmgr1), NTK_HRC_NODE_APPL_KEY); if(network1 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: There is no network. Use flatten_hierarchy.\n"); return 1; } if(!Ntk_NetworkReadNumLatches(network1)) { (void) fprintf(vis_stderr, "** eqv error: No latches present in the current network. Use comb_verify.\n"); return 1; } fileName2 = argv[util_optind]; if(isBlif) { if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); goto usage; } } else { if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); return 1; } hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); fclose(fp); if(hmgr2 == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); return 1; } } network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), TRUE, (lsList) NULL); if(network2 == NIL(Ntk_Network_t)) { Hrc_ManagerFree(hmgr2); (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); return 1; } if(!Ntk_NetworkReadNumLatches(network2)) { (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName2); Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } } else { fileName1 = argv[util_optind]; fileName2 = argv[util_optind+1]; if(isBlif) { if((hmgr1 = Io_BlifRead(fileName1, FALSE)) == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); return 1; } if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); if(hmgr1) { Hrc_ManagerFree(hmgr1); } return 1; } } else { if((fp = Cmd_FileOpen(fileName1, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName1); return 1; } hmgr1 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); fclose(fp); if(hmgr1 == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); goto usage; } if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); if(hmgr1) { Hrc_ManagerFree(hmgr1); } return 1; } hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); fclose(fp); if(hmgr2 == NIL(Hrc_Manager_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); if(hmgr1) { Hrc_ManagerFree(hmgr1); } return 1; } } network1 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr1), TRUE, (lsList) NULL); network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), TRUE, (lsList) NULL); if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) { if(network1 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n"); } if(network2 == NIL(Ntk_Network_t)) { (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); } Hrc_ManagerFree(hmgr1); Hrc_ManagerFree(hmgr2); return 1; } if(!Ntk_NetworkReadNumLatches(network1)) { (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName1); Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } if(!Ntk_NetworkReadNumLatches(network2)) { (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName2); Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } } if(Ntk_NetworkReadNumPrimaryInputs(network1) != Ntk_NetworkReadNumInputs(network1)) { error_append("** eqv error: Pseudo inputs present in network1. Unable to do verification.\n"); (void) fprintf(vis_stderr, "%s", error_string()); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } if(Ntk_NetworkReadNumPrimaryInputs(network2) != Ntk_NetworkReadNumInputs(network2)) { error_append("** eqv error: Pseudo inputs present in network2. Unable to do verification.\n"); (void) fprintf(vis_stderr, "%s", error_string()); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } if(Ntk_NetworkReadNumPrimaryInputs(network1) != Ntk_NetworkReadNumPrimaryInputs(network2)) { error_append("** eqv error: Different number of inputs in the two networks.\n"); (void) fprintf(vis_stderr, "%s", error_string()); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); return 1; } /* Start the timer before calling the equivalence checker. */ if (timeOutPeriod > 0){ (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(timeOutPeriod); if (setjmp(timeOutEnv) > 0) { (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod); alarm(0); return 1; } } if(fileFlag) { rootsTable = st_init_table(strcmp, st_strhash); leavesTable = st_init_table(strcmp, st_strhash); check = ReadRootLeafMap(inputFile, rootsTable, leavesTable); fclose(inputFile); if(check == 0) { st_free_table(rootsTable); st_free_table(leavesTable); (void) fprintf(vis_stderr, "** eqv error: No data in the input file\n"); alarm(0); return 1; } switch (check) { case 1 : st_free_table(rootsTable); outputMap = MapPrimaryOutputsByName(network1, network2); if((outputMap == NIL(st_table)) || !TestLeavesAreValid(network1, network2, leavesTable)) { st_foreach_item(leavesTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(leavesTable); if(outputMap) { st_free_table(outputMap); } (void) fprintf(vis_stderr, "%s", error_string()); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); alarm(0); return 1; } equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, network2, NIL(st_table), leavesTable, partMethod, useBackwardReach, reordering); st_foreach_item(leavesTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(leavesTable); break; case 2 : st_free_table(leavesTable); inputMap = MapPrimaryInputsByName(network1, network2); if((inputMap == NIL(st_table)) || !TestRootsAreValid(network1, network2, rootsTable)) { st_foreach_item(rootsTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(rootsTable); if(inputMap) { st_free_table(inputMap); } (void) fprintf(vis_stderr, "%s", error_string()); if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); alarm(0); return 1; } equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, network2, rootsTable, NIL(st_table), partMethod, useBackwardReach, reordering); st_foreach_item(rootsTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(rootsTable); break; case 3 : if(TestRootsAreValid(network1, network2, rootsTable) && TestLeavesAreValid(network1, network2, leavesTable)) { equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, network2, rootsTable, leavesTable, partMethod, useBackwardReach, reordering); st_foreach_item(rootsTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(rootsTable); st_foreach_item(leavesTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(leavesTable); } else { if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); st_foreach_item(rootsTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(rootsTable); st_foreach_item(leavesTable, gen, &name1, &name2) { FREE(name1); FREE(name2); } st_free_table(leavesTable); (void) fprintf(vis_stderr, "%s", error_string()); alarm(0); return 1; } } } else { outputMap = MapPrimaryOutputsByName(network1, network2); inputMap = MapPrimaryInputsByName(network1, network2); if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) { if(inputMap) { st_free_table(inputMap); } if(outputMap) { st_free_table(outputMap); } if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); (void) fprintf(vis_stderr, "%s", error_string()); alarm(0); return 1; /* all primary outputs do not match */ } st_free_table(inputMap); st_free_table(outputMap); equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, network2, NIL(st_table), NIL(st_table), partMethod, useBackwardReach, reordering); } if(equivalent) { (void) fprintf(vis_stdout, "Networks are sequentially equivalent.\n\n"); } else { (void) fprintf(vis_stdout, "Networks are NOT sequentially equivalent.\n\n"); } if (printBddInfo) { bdd_print_stats(Ntk_NetworkReadMddManager(network2), vis_stdout); } if(execMode) { Hrc_ManagerFree(hmgr1); Ntk_NetworkFree(network1); } Hrc_ManagerFree(hmgr2); Ntk_NetworkFree(network2); alarm(0); return 0; /* normal exit */ usage : (void) fprintf(vis_stderr, "usage: seq_verify [-b] [-f filename] [-h] [-p partition method] [-t time] [-B]\n\t\t [-i] [-r] file1 [file2]\n"); (void) fprintf(vis_stderr, " -b input files are BLIF\n"); (void) fprintf(vis_stderr, " -f file variable name correspondence file\n"); (void) fprintf(vis_stderr, " -h print the command usage\n"); (void) fprintf(vis_stderr, " -p method partitioning method for product machine\n"); (void) fprintf(vis_stderr, " -t time time out period (in seconds)\n"); (void) fprintf(vis_stderr, " -B use backward image computation\n"); (void) fprintf(vis_stderr, " -i print BDD statistics\n"); (void) fprintf(vis_stderr, " -r enable BDD variable reordering\n"); return 1; /* error exit */ } /**Function******************************************************************** Synopsis [Handle function for timeout.] Description [This function is called when the time out occurs.] SideEffects [] ******************************************************************************/ static void TimeOutHandle(void) { longjmp(timeOutEnv, 1); }