Start of merging Mitch Bailey's code changes from github pull

request #59 ("Pin match").  Because the pull request has rather
sweeping modifications, I am doing this in two steps.  The change
that most breaks with existing comparison methods is in the
PinMatch() routine in netcmp.c, where the method of generating
proxy pins has been removed.  There are specific cases for which
the proxy pin method exists, although these were coping with
issues arising from extraction in magic which have been dealt
with to some extend.  Possibly the proxy pin method is no longer
needed.  So the PinMatch() changes will be done in a second
commit where it's easier to revert or modify the changes without
affecting the modifications from this commit.
This commit is contained in:
Tim Edwards 2022-09-13 10:55:00 -04:00
parent 79e193e0c9
commit 9297090dc1
5 changed files with 271 additions and 174 deletions

View File

@ -1 +1 @@
1.5.228
1.5.229

View File

@ -66,7 +66,7 @@ void flattenCell(char *name, int file)
else
ThisCell = LookupCellFile(name, file);
if (ThisCell == NULL) {
Printf("No cell %s found.\n", name);
Printf("No cell %s (%d) found.\n", name, file);
return;
}
@ -282,13 +282,14 @@ int flattenInstancesOf(char *name, int fnum, char *instance)
}
else {
if (Debug)
Printf("Flattening instances of %s within cell: %s\n", instance, name);
Printf("Flattening instances of %s within cell: %s (%d)\n", instance,
name, fnum);
if (fnum == -1)
ThisCell = LookupCell(name);
else
ThisCell = LookupCellFile(name, fnum);
if (ThisCell == NULL) {
Printf("No cell %s found.\n", name);
Printf("No cell %s (%d) found.\n", name, fnum);
return 0;
}
}
@ -688,7 +689,7 @@ void convertGlobalsOf(char *name, int fnum, char *instance)
else
ThisCell = LookupCellFile(name, fnum);
if (ThisCell == NULL) {
Printf("No cell %s found.\n", name);
Printf("No cell %s (%d) found.\n", name, fnum);
return;
}
}
@ -1118,7 +1119,7 @@ int UniquePins(char *name, int filenum)
ThisCell = LookupCellFile(name, filenum);
if (ThisCell == NULL) {
Printf("No cell %s found.\n", name);
Printf("No cell %s (%d) found.\n", name, filenum);
return 0;
}
@ -1159,7 +1160,8 @@ int UniquePins(char *name, int filenum)
continue;
}
else {
Printf("Duplicate pin %s in cell %s\n", ob->name, ThisCell->name);
Printf("Duplicate pin %s in cell %s (%d)\n", ob->name,
ThisCell->name, filenum);
}
}
if (nodecount[ob->node] > 1) {
@ -1360,7 +1362,7 @@ int CleanupPins(char *name, int filenum)
ThisCell = LookupCellFile(name, filenum);
if (ThisCell == NULL) {
Printf("No cell %s found.\n", name);
Printf("No cell %s (%d) found.\n", name, filenum);
return 0;
}

View File

@ -6185,7 +6185,8 @@ void PrintPropertyResults(int do_list)
/*----------------------------------------------------------------------*/
/* Return 0 if perfect matching found, else return number of */
/* automorphisms, and return -1 if invalid matching found. */
/* automorphisms, and return -1 if invalid matching found, */
/* and return -2 if there is a port count mismatch. */
/*----------------------------------------------------------------------*/
int VerifyMatching(void)
@ -6196,6 +6197,9 @@ int VerifyMatching(void)
struct Element *E;
struct Node *N;
int C1, C2, result;
int P1, P2;
struct objlist *ob1, *ob2;
int portMismatch = 0;
if (BadMatchDetected) return(-1);
@ -6216,14 +6220,40 @@ int VerifyMatching(void)
}
}
P1 = P2 = 0;
for (NC = NodeClasses; NC != NULL; NC = NC->next) {
C1 = C2 = 0;
for (N = NC->nodes; N != NULL; N = N->next) {
(N->graph == Circuit1->file) ? C1++ : C2++;
if (IsPort(N->object)) (N->graph == Circuit1->file) ? P1++ : P2++;
}
if (C1 != C2) return(-1);
if (P1 != P2) portMismatch = 1;
if (C1 != 1) ret++;
}
P1 = P2 = 0;
if (ret == 0) { /* automorphisms have precedence over port count mismatch */
if (portMismatch) return -2;
/* Count ports in each subcircuit including disconnected ports */
for (ob1 = Circuit1->cell; ob1 && IsPort(ob1); ob1 = ob1->next, P1++);
for (ob2 = Circuit2->cell; ob2 && IsPort(ob2); ob2 = ob2->next, P2++);
if (P1 == P2) { // pin counts match. Make sure disconnected pins match, too.
for (ob1 = Circuit1->cell; ob1 && IsPort(ob1); ob1 = ob1->next) {
if (ob1->node == -1) { // disconnected pin
for (ob2 = Circuit2->cell; ob2 && IsPort(ob2); ob2 = ob2->next) {
if (ob2->node == -1 && (*matchfunc)(ob1->name, ob2->name))
break; // disconnected pin match
}
if (ob2 == NULL) return -2;
}
}
}
else { // pin count mismatch
return -2;
}
}
return(ret);
}
@ -6322,7 +6352,7 @@ int ResolveAutomorphsByPin()
FractureElementClass(&ElementClasses);
FractureNodeClass(&NodeClasses);
ExhaustiveSubdivision = 1;
while (!Iterate() && VerifyMatching() != -1);
while (!Iterate() && VerifyMatching() >= 0);
return(VerifyMatching());
}
@ -6425,7 +6455,7 @@ int ResolveAutomorphsByProperty()
FractureElementClass(&ElementClasses);
FractureNodeClass(&NodeClasses);
ExhaustiveSubdivision = 1;
while (!Iterate() && VerifyMatching() != -1);
while (!Iterate() && VerifyMatching() >= 0);
return(VerifyMatching());
}
@ -6502,7 +6532,7 @@ int ResolveAutomorphisms()
FractureElementClass(&ElementClasses);
FractureNodeClass(&NodeClasses);
ExhaustiveSubdivision = 1;
while (!Iterate() && VerifyMatching() != -1);
while (!Iterate() && VerifyMatching() >= 0);
return(VerifyMatching());
}
@ -7197,32 +7227,31 @@ struct nlist *addproxies(struct hashlist *p, void *clientdata)
return NULL; /* Keep the search going */
}
/*------------------------------------------------------*/
/* Declare that the device class "name1" is equivalent */
/* to class "name2". This is the same as the above */
/* routine, except that the cells must be at the top */
/* of the compare queue, and must already be proven */
/* equivalent by LVS. Determine a pin correspondence, */
/* then modify all instances of "name2" to match all */
/* instances of "name1" by pin reordering. If either */
/* cell has disconnected pins, they are shuffled to the */
/* end of the pin list. If two or more pins correspond */
/* to net automorphisms, then they are added to the */
/* list of permuted pins. */
/* */
/* NOTE: This routine must not be called on any */
/* circuit pair that has not been matched. If a */
/* circuit pair has been matched with automorphisms, */
/* then some pins may be matched arbitrarily. */
/* */
/* If "dolist" is 1, append the list representing the */
/* output (if any) to variable tcl_out, if it exists. */
/* */
/* Return codes: */
/* 2: Neither cell had pins, so matching is unnecessary */
/* 1: Exact match */
/* 0: Inexact match resolved by proxy pin insertion */
/*------------------------------------------------------*/
/*--------------------------------------------------------------*/
/* Declare that the device class "name1" is equivalent to class */
/* "name2". This is the same as the above routine, except that */
/* the cells must be at the top of the compare queue, and must */
/* already be proven equivalent by LVS. Determine a pin */
/* correspondence, then modify all instances of "name2" to */
/* match all instances of "name1" by pin reordering. If either */
/* cell has disconnected pins, they are shuffled to the end of */
/* the pin list. If two or more pins correspond to net */
/* automorphisms, then they are added to the list of permuted */
/* pins. */
/* */
/* NOTE: This routine must not be called on any circuit pair */
/* that has not been matched. If a circuit pair has been */
/* matched with automorphisms, then some pins may be matched */
/* arbitrarily. */
/* */
/* If "dolist" is 1, append the list representing the output */
/* (if any) to variable tcl_out, if it exists. */
/* */
/* Return codes: */
/* 2: Neither cell had pins, so matching is unnecessary */
/* 1: Exact match */
/* 0: Inexact match resolved by proxy pin insertion. */
/*--------------------------------------------------------------*/
int MatchPins(struct nlist *tc1, struct nlist *tc2, int dolist)
{
@ -7817,7 +7846,7 @@ int MatchPins(struct nlist *tc1, struct nlist *tc2, int dolist)
}
/* Check for ports that did not get ordered */
for (obn = tc2->cell; obn && (obn->type == PORT); obn = obn->next) {
for (obn = tc2->cell; obn && IsPort(obn); obn = obn->next) {
if (obn->model.port == -1) {
if (obn->node == -1) {
// This only happens when pins have become separated from any net.
@ -7995,10 +8024,12 @@ int EquivalentElement(char *name, struct nlist *circuit, struct objlist **retobj
void FlattenCurrent()
{
if (Circuit1 != NULL && Circuit2 != NULL) {
Fprintf(stdout, "Flattening subcell %s\n", Circuit1->name);
Fprintf(stdout, "Flattening subcell %s (%d)\n", Circuit1->name,
Circuit1->file);
FlattenInstancesOf(Circuit1->name, Circuit1->file);
Fprintf(stdout, "Flattening subcell %s\n", Circuit2->name);
Fprintf(stdout, "Flattening subcell %s (%d)\n", Circuit2->name,
Circuit2->file);
FlattenInstancesOf(Circuit2->name, Circuit2->file);
}
}
@ -8069,7 +8100,25 @@ int Compare(char *cell1, char *cell2)
PrintIllegalClasses();
return(0);
}
if (automorphisms == 0) Fprintf(stdout, "Circuits match correctly.\n");
if (automorphisms > 0) {
Fprintf(stdout, "Circuits match with %d symmetries.\n", automorphisms);
if (VerboseOutput) PrintAutomorphisms();
/* arbitrarily resolve automorphisms */
Fprintf(stdout, "\n");
Fprintf(stdout, "Resolving automorphisms by arbitrary symmetry breaking:\n");
while ((automorphisms = ResolveAutomorphisms()) > 0) ;
if (automorphisms == -1) {
MatchFail(cell1, cell2);
Fprintf(stdout, "Circuits do not match.\n");
return 0;
}
}
if (automorphisms == -2) { // Port count mismatch
Fprintf(stderr, "Port counts do not match.\n");
return 0;
}
if (PropertyErrorDetected == 1) {
Fprintf(stdout, "There were property errors.\n");
PrintPropertyResults(0);
@ -8078,22 +8127,10 @@ int Compare(char *cell1, char *cell2)
Fprintf(stdout, "There were missing properties.\n");
PrintPropertyResults(0);
}
if (automorphisms == 0) return(1);
else
Fprintf(stdout, "Circuits match correctly.\n");
Fprintf(stdout, "Circuits match with %d automorphisms.\n", automorphisms);
if (VerboseOutput) PrintAutomorphisms();
/* arbitrarily resolve automorphisms */
Fprintf(stdout, "\n");
Fprintf(stdout, "Resolving automorphisms by arbitrary symmetry breaking:\n");
while ((automorphisms = ResolveAutomorphisms()) > 0) ;
if (automorphisms == -1) {
MatchFail(cell1, cell2);
Fprintf(stdout, "Circuits do not match.\n");
return(0);
}
Fprintf(stdout, "Circuits match correctly.\n");
return(1);
return 1;
}
@ -8147,9 +8184,12 @@ void NETCOMP(void)
PrintIllegalClasses();
Fprintf(stdout, "Netlists do not match.\n");
}
else if (automorphisms == -2) { // port count mismatch
Fprintf(stdout, "Port counts do not match.\n");
}
else {
if (automorphisms)
Printf("Circuits match with %d automorphisms.\n", automorphisms);
Printf("Circuits match with %d symmetries.\n", automorphisms);
else Printf("Circuits match correctly.\n");
}
}
@ -8162,11 +8202,13 @@ void NETCOMP(void)
while (!Iterate()) ;
automorphisms = VerifyMatching();
if (automorphisms == -1) Fprintf(stdout, "Netlists do not match.\n");
else if (automorphisms == -2) Fprintf(stdout, "Port counts do not match.\n");
else {
Printf("Netlists match with %d automorphisms.\n", automorphisms);
Printf("Netlists match with %d symmetries.\n", automorphisms);
while ((automorphisms = ResolveAutomorphisms()) > 0)
Printf(" automorphisms = %d.\n", automorphisms);
if (automorphisms == -1) Fprintf(stdout, "Netlists do not match.\n");
else if (automorphisms == -2) Fprintf(stdout, "Port counts do not match.\n");
else Printf("Circuits match correctly.\n");
}
}

View File

@ -532,14 +532,24 @@ proc netgen::lvs { name1 name2 {setupfile setup.tcl} {logfile comp.out} args} {
}
set properr {}
set matcherr {}
set pinsgood -1
set childMismatch 0 ;# 1 indicates black-box child subcircuit mismatch
while {$endval != {}} {
if {$dolist == 1} {
netgen::run -list converge
} else {
netgen::run converge
}
netgen::log echo on
set pinMismatch 0 ;# indicates pin mismatch in top cell
set doCheckFlatten 0
set doFlatten 0
if {[netgen::print queue] == {}} {
set doEquatePins 1 ;# run equate pins on top cell
} else {
set doEquatePins 0 ;# don't run equate pins unless unique match
}
set forceMatch 0 ;# for pin matching
netgen::log echo off
if {[verify equivalent]} {
# Resolve automorphisms by pin and property
if {$dolist == 1} {
@ -548,98 +558,105 @@ proc netgen::lvs { name1 name2 {setupfile setup.tcl} {logfile comp.out} args} {
netgen::run resolve
}
set uresult [verify unique]
# uresult: -3 : unique with property error
# -2 : equivalent with port errors
# -1 : black box
# 0 : equivalent but not unique
# 1 : unique
if {$uresult == 0} {
netgen::log echo on
netgen::log put " Networks match locally but not globally.\n"
netgen::log put " Probably connections are swapped.\n"
netgen::log put " Check the end of logfile ${logfile} for implicated nodes.\n"
netgen::log echo off
if {$dolist == 1} {
verify -list nodes
} else {
verify nodes
}
# Flatten the non-matching subcircuit (but not the top-level cells)
if {[netgen::print queue] != {}} {
if {([lsearch $noflat [lindex $endval 0]] == -1) &&
([lsearch $noflat [lindex $endval 1]] == -1)} {
netgen::log put " Flattening non-matched subcircuits $endval\n"
netgen::flatten class "[lindex $endval 0] $fnum1"
netgen::flatten class "[lindex $endval 1] $fnum2"
} else {
netgen::log put " Continuing with black-boxed subcircuits $endval\n"
lappend matcherr [lindex $endval 0]"($fnum1)"
lappend matcherr [lindex $endval 1]"($fnum2)"
netgen::flatten prohibit "[lindex $endval 0] $fnum1"
netgen::flatten prohibit "[lindex $endval 1] $fnum2"
# Match pins
netgen::log echo off
if {$dolist == 1} {
set result [equate -list -force pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
} else {
set result [equate -force pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
}
if {$result != 0} {
equate classes "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"
}
set pinsgood $result
netgen::log echo on
}
}
set doCheckFlatten 1
} else {
netgen::log echo off
if {$dolist == 1} {
set result [equate -list pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
} else {
set result [equate pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
}
if {$result != 0} {
equate classes "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"
}
# If $uresult == -1 then these are black-box entries and
# $pinsgood should not be set to the resulting value.
if {$uresult > 0} {
set pinsgood $result
}
netgen::log echo on
# Equate pins for black boxes, unique matches (possibly with property
# errors), and unique with port errors
set doEquatePins 1
}
if {$uresult == -1} { ;# black box
set forceMatch 1
} elseif {$uresult == -3} { ;# property error
lappend properr [lindex $endval 0]
} elseif {$uresult == -2} { ;# unmatched pins
set doCheckFlatten 1
}
if {$uresult == 2} {lappend properr [lindex $endval 0]}
} else {
# Flatten the non-matching subcircuit (but not the top-level cells)
if {[netgen::print queue] != {}} {
# not equivalent
netgen::log echo on
# netgen::log put " DEBUG: not equivalent $endval\n"
netgen::log echo off
set doCheckFlatten 1
}
if {$doCheckFlatten} {
# Flatten the non-matching subcircuit (but not the top-level cell,
# or cells explicitly prohibited from flattening)
if {[netgen::print queue] != {}} {
if {([lsearch $noflat [lindex $endval 0]] == -1) &&
([lsearch $noflat [lindex $endval 1]] == -1)} {
netgen::log put " Flattening non-matched subcircuits $endval\n"
netgen::flatten class "[lindex $endval 0] $fnum1"
netgen::flatten class "[lindex $endval 1] $fnum2"
} else {
([lsearch $noflat [lindex $endval 1]] == -1)} {
set doFlatten 1
} else {
netgen::log echo on
netgen::log put " Continuing with black-boxed subcircuits $endval\n"
netgen::log echo off
lappend matcherr [lindex $endval 0]"($fnum1)"
lappend matcherr [lindex $endval 0]"($fnum2)"
# Match pins
netgen::log echo off
if {$dolist == 1} {
set result [equate -list -force pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
} else {
set result [equate -force pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
}
if {$result != 0} {
equate classes "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"
}
set pinsgood $result
netgen::log echo on
lappend matcherr [lindex $endval 1]"($fnum2)"
netgen::flatten prohibit "[lindex $endval 0] $fnum1"
netgen::flatten prohibit "[lindex $endval 1] $fnum2"
set doEquatePins 1
set childMismatch 1
set forceMatch 1
}
}
}
netgen::log echo off
if {$doEquatePins} {
# Match pins
if {$dolist == 1} {
if {$forceMatch} {
set result [equate -list -force pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
} else {
set result [equate -list pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
}
} else {
if {$forceMatch} {
set result [equate -force pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
} else {
set result [equate pins "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"]
}
}
if {$result >= 0} {
equate classes "$fnum1 [lindex $endval 0]" \
"$fnum2 [lindex $endval 1]"
}
# Do not set pinMismatch for black boxes
if {$result < 0} {
if {$result == -1 && [netgen::print queue] != {} && $forceMatch != 1} {
# flatten pin mismatch, but not empty cells (-2) or top cell or
# cells prohibited from flattening.
set doFlatten 1
}
} elseif {[netgen::print queue] == {} && $result == 0} {
set pinMismatch 1
}
}
if {$doFlatten} {
netgen::log echo on
netgen::log put " Flattening non-matched subcircuits $endval\n"
netgen::log echo off
netgen::flatten class "[lindex $endval 0] $fnum1"
netgen::flatten class "[lindex $endval 1] $fnum2"
}
if {$dolist == 1} {
catch {lappend lvs_final $lvs_out}
set lvs_out {}
@ -648,20 +665,23 @@ proc netgen::lvs { name1 name2 {setupfile setup.tcl} {logfile comp.out} args} {
set endval [netgen::compare hierarchical]
}
}
netgen::log echo off
puts stdout "Result: " nonewline
netgen::log echo on
if {$pinsgood == 0} {
# NOTE: Need to disambiguate these two cases. . .
netgen::log put "Cells failed matching, or top level cell failed pin matching.\n"
netgen::log put "\nFinal result: "
if {$pinMismatch || $childMismatch} {
if {$childMismatch} {
netgen::log put "Subcell(s) failed matching.\n"
}
if {$pinMismatch} {
netgen::log put "Top level cell failed pin matching.\n"
}
} else {
verify only
}
if {$properr != {}} {
netgen::log put "The following cells had property errors:\n " [regsub -all { } $properr "\n "] "\n"
netgen::log put "\nThe following cells had property errors:\n " [regsub -all { } $properr "\n "] "\n"
}
if {$matcherr != {}} {
netgen::log put "The following subcells failed to match:\n " [regsub -all { } $matcherr "\n "] "\n"
netgen::log put "\nThe following subcells failed to match:\n " [regsub -all { } $matcherr "\n "] "\n"
}
if {$dolog} {
netgen::log end

View File

@ -1937,9 +1937,17 @@ _netgen_log(ClientData clientData,
switch(index) {
case START_IDX:
LoggingFile = fopen(LogFileName, "w");
if (!LoggingFile) {
Tcl_SetResult(interp, "Could not open log file.", NULL);
return TCL_ERROR;
}
break;
case RESUME_IDX:
LoggingFile = fopen(LogFileName, "a");
if (!LoggingFile) {
Tcl_SetResult(interp, "Could not open log file.", NULL);
return TCL_ERROR;
}
break;
case END_IDX:
fclose(LoggingFile);
@ -1948,6 +1956,10 @@ _netgen_log(ClientData clientData,
case RESET_IDX:
fclose(LoggingFile);
LoggingFile = fopen(LogFileName, "w");
if (!LoggingFile) {
Tcl_SetResult(interp, "Could not open log file.", NULL);
return TCL_ERROR;
}
break;
case SUSPEND_IDX:
fclose(LoggingFile);
@ -2209,11 +2221,11 @@ _netcmp_compare(ClientData clientData,
hascontents2 = HasContents(tp2);
if (hascontents1 && !hascontents2 && (tp2->flags & CELL_PLACEHOLDER)) {
Fprintf(stdout, "Circuit 2 cell %s is a black box; will not flatten "
Fprintf(stdout, "\nCircuit 2 cell %s is a black box; will not flatten "
"Circuit 1\n", name2);
}
else if (hascontents2 && !hascontents1 && (tp1->flags & CELL_PLACEHOLDER)) {
Fprintf(stdout, "Circuit 1 cell %s is a black box; will not flatten "
Fprintf(stdout, "\nCircuit 1 cell %s is a black box; will not flatten "
"Circuit 2\n", name1);
}
else if (hascontents1 || hascontents2) {
@ -2229,6 +2241,10 @@ _netcmp_compare(ClientData clientData,
DescribeContents(name1, fnum1, name2, fnum2);
}
}
else { /* Two empty subcircuits */
Fprintf(stdout, "\nCircuit 1 cell %s and Circuit 2 cell %s are black"
" boxes.\n", name1, name2);
}
CreateTwoLists(name1, fnum1, name2, fnum2, dolist);
// Return the names of the two cells being compared, if doing "compare
@ -2485,39 +2501,37 @@ _netcmp_run(ClientData clientData,
ExhaustiveSubdivision = 1;
while (!Iterate() && !InterruptPending);
automorphisms = VerifyMatching();
if (automorphisms == -1)
Fprintf(stdout, "Netlists do not match.\n");
else if (automorphisms == 0)
Fprintf(stdout, "Netlists match uniquely.\n");
else {
if (automorphisms > 0) {
// First try to resolve automorphisms uniquely using
// property matching
automorphisms = ResolveAutomorphsByProperty();
if (automorphisms == 0)
Fprintf(stdout, "Netlists match uniquely.\n");
else if (automorphisms > 0) {
if (automorphisms > 0) {
// Next, attempt to resolve automorphisms uniquely by
// using the pin names
automorphisms = ResolveAutomorphsByPin();
}
if (automorphisms == 0)
Fprintf(stdout, "Netlists match uniquely.\n");
else if (automorphisms > 0) {
if (automorphisms > 0) {
// Anything left is truly indistinguishable
Fprintf(stdout, "Netlists match with %d symmetr%s.\n",
automorphisms, (automorphisms == 1) ? "y" : "ies");
while ((automorphisms = ResolveAutomorphisms()) > 0);
while (ResolveAutomorphisms() > 0);
}
if (automorphisms == -1)
Fprintf(stdout, "Netlists do not match.\n");
else
Fprintf(stdout, "Circuits match correctly.\n");
}
if (PropertyErrorDetected) {
Fprintf(stdout, "There were property errors.\n");
PrintPropertyResults(dolist);
if (automorphisms == -1)
Fprintf(stdout, "Netlists do not match.\n");
else if (automorphisms == -2)
Fprintf(stdout, "Netlists match uniquely with port errors.\n");
else {
if (automorphisms == 0)
Fprintf(stdout, "Netlists match uniquely");
else
Fprintf(stdout, "Netlists match with %d symmetr%s",
automorphisms, (automorphisms == 1) ? "y" : "ies");
if (PropertyErrorDetected) {
Fprintf(stdout, " with property errors.\n");
PrintPropertyResults(dolist);
}
else
Fprintf(stdout, ".\n");
}
disable_interrupt();
}
@ -2535,8 +2549,14 @@ _netcmp_run(ClientData clientData,
/* all, or no option. */
/* Formerly: v */
/* Results: */
/* For only, equivalent, unique: Return 1 if */
/* verified, zero if not. */
/* For only, equivalent, unique: Return */
/* 1: verified */
/* 0: not verified */
/* -1: no elements or nodes */
/* -3: verified with property error */
/* equiv option */
/* -2: pin mismatch */
/* */
/* Side Effects: */
/* For options elements, nodes, and all without */
/* option -list: Write output to log file. */
@ -2636,7 +2656,7 @@ _netcmp_verify(ClientData clientData,
Tcl_SetObjResult(interp, Tcl_NewIntObj((int)automorphisms));
else if (index == UNIQUE_IDX)
Tcl_SetObjResult(interp, Tcl_NewBooleanObj(0));
else
else if (index > 0)
Printf("Circuits match with %d symmetr%s.\n",
automorphisms, (automorphisms == 1) ? "y" : "ies");
}
@ -2645,11 +2665,13 @@ _netcmp_verify(ClientData clientData,
if (PropertyErrorDetected == 0)
Tcl_SetObjResult(interp, Tcl_NewBooleanObj(1));
else
Tcl_SetObjResult(interp, Tcl_NewIntObj(2));
Tcl_SetObjResult(interp, Tcl_NewIntObj(-3));
}
else {
else if (index > 0) {
Fprintf(stdout, "Circuits match uniquely.\n");
if (PropertyErrorDetected != 0)
if (PropertyErrorDetected == 0)
Fprintf(stdout, ".\n");
else
Fprintf(stdout, "Property errors were found.\n");
}
}
@ -3072,7 +3094,11 @@ _netcmp_equate(ClientData clientData,
tp1->flags |= CELL_PLACEHOLDER;
tp2->flags |= CELL_PLACEHOLDER;
}
else {
else if (doforce != TRUE) {
/* When doforce is TRUE, ElementClass has been set to NULL
* even though circuits contain elements, so this message
* is not correct.
*/
Fprintf(stdout, "Equate pins: cell %s and/or %s "
"has no elements.\n", name1, name2);
/* This is not necessarily an error, so go ahead and match pins. */
@ -3104,6 +3130,13 @@ _netcmp_equate(ClientData clientData,
else if (result > 0) {
Fprintf(stdout, "Cell pin lists are equivalent.\n");
}
else if (result == -1) {
Fprintf(stdout, "Cell pin lists for %s and %s do not match.\n",
name1, name2);
}
else if (result == -2) {
Fprintf(stdout, "Attempt to match empty cell to non-empty cell.\n");
}
else {
Fprintf(stdout, "Cell pin lists for %s and %s altered to match.\n",
name1, name2);