From 5e99fd5ef9c4076cdc8eb0af76fce2442f148606 Mon Sep 17 00:00:00 2001 From: Tim Edwards Date: Thu, 8 Oct 2020 09:43:25 -0400 Subject: [PATCH] Found a counterexample which shows that the fast symmetry breaking introduced in revision 150 can result in an incorrect result reporting a bad match where the match is actually good (as proven by running the full symmetry breaking on the same netlist). Because the fast symmetry breaking is orders of magnitude faster for large circuits, and because the false positive result appears to be rare, I have introduced a command "symmetry" to switch methods between fast and full. So fast symmetry breaking can be run unless the result fails on symmetry breaking, in which case the method can be switched to full to see if the problem is a false positive or not. This is not an ideal solution, and some investigation is needed to determine if there is a way to apply fast symmetry breaking without encountering a false positive error. --- VERSION | 2 +- base/netcmp.c | 110 ++++++++++++++++++++++++++++++++++++++++++---- base/netcmp.h | 1 + tcltk/tclnetgen.c | 48 +++++++++++++++++++- 4 files changed, 151 insertions(+), 10 deletions(-) diff --git a/VERSION b/VERSION index 05c3baa..00be87e 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -1.5.156 +1.5.157 diff --git a/base/netcmp.c b/base/netcmp.c index 8db52c4..e60dccf 100644 --- a/base/netcmp.c +++ b/base/netcmp.c @@ -158,6 +158,9 @@ int right_col_end = 87; /* if TRUE, always partition ALL classes */ int ExhaustiveSubdivision = 0; +/* if TRUE, use fast symmetry breaking to resolve automorphisms */ +int FastSymmetryBreaking = 1; + #ifdef TEST static void PrintElement_List(struct Element *E) { @@ -5862,7 +5865,81 @@ int ResolveAutomorphsByProperty() /* *------------------------------------------------------------------------- * - * ResolveElementAutomorphisms -- + * ResolveAutormorphismsFull -- + * + * Arbitrarily equivalence one pair of elements within an automorphic class + * + * Return value is the same as VerifyMatching() + * + *------------------------------------------------------------------------- + */ + +int ResolveAutomorphismsFull() +{ + struct ElementClass *EC; + struct Element *E; + struct NodeClass *NC; + struct Node *N; + int C1, C2; + + for (EC = ElementClasses; EC != NULL; EC = EC->next) { + struct Element *E1, *E2; + C1 = C2 = 0; + E1 = E2 = NULL; + for (E = EC->elements; E != NULL; E = E->next) { + if (E->graph == Circuit1->file) { + C1++; + E1 = E; + } + else { + C2++; + E2 = E; + } + } + if (C1 == C2 && C1 != 1) { + unsigned long newhash; + Magic(newhash); + E1->hashval = newhash; + E2->hashval = newhash; + goto converge; + } + } + + for (NC = NodeClasses; NC != NULL; NC = NC->next) { + struct Node *N1, *N2; + C1 = C2 = 0; + N1 = N2 = NULL; + for (N = NC->nodes; N != NULL; N = N->next) { + if (N->graph == Circuit1->file) { + C1++; + N1 = N; + } + else { + C2++; + N2 = N; + } + } + if (C1 == C2 && C1 != 1) { + unsigned long newhash; + Magic(newhash); + N1->hashval = newhash; + N2->hashval = newhash; + goto converge; + } + } + + converge: + FractureElementClass(&ElementClasses); + FractureNodeClass(&NodeClasses); + ExhaustiveSubdivision = 1; + while (!Iterate() && VerifyMatching() != -1); + return(VerifyMatching()); +} + +/* + *------------------------------------------------------------------------- + * + * ResolveElementAutomorphismsFast -- * * Apply arbitrary symmetry breaking to symmetric element lists, then * iterate exhaustively to resolve all automorphisms. @@ -5872,7 +5949,7 @@ int ResolveAutomorphsByProperty() *------------------------------------------------------------------------- */ -int ResolveElementAutomorphisms() +int ResolveElementAutomorphismsFast() { struct ElementClass *EC; struct Element *E; @@ -5924,7 +6001,7 @@ int ResolveElementAutomorphisms() /* *------------------------------------------------------------------------- * - * ResolveNodeAutomorphisms -- + * ResolveNodeAutomorphismsFast -- * * Apply arbitrary symmetry breaking to symmetric node lists, then iterate * exhaustively to resolve all automorphisms. Normally, all automorphisms @@ -5937,7 +6014,7 @@ int ResolveElementAutomorphisms() * */ -int ResolveNodeAutomorphisms() +int ResolveNodeAutomorphismsFast() { struct Node *N; struct NodeClass *NC; @@ -5991,7 +6068,20 @@ int ResolveNodeAutomorphisms() * * ResolveAutormorphisms -- * - * Arbitrarily equivalence one pair of elements within an automorphic class + * Do symmetry breaking of automorphisms. If FastSymmetryBreaking is + * False (not the default), then run ResolveAutomorphismsFull() (q.v.). + * Otherwise, run the fast symmetry breaking method: + * + * Arbitrarily equivalence all pairs of elements and nodes within all + * automorphic classes, and run to completion. Note that this is a + * fast version of ResolveAutomorphismsFull(), and can run many orders + * of magnitude faster. However, it can also produce an incorrect + * result, declaring a global mismatch where none exists. In that + * case, the matching should be re-run with ResolveAutomorphismsFull(). + * + * Some investigation needs to be done to determine if there is a way + * to execute faster symmetry breaking without the possibility of + * producing an incorrect result. * * Return value is the same as VerifyMatching() * @@ -6002,9 +6092,12 @@ int ResolveAutomorphisms() { int result; - result = ResolveElementAutomorphisms(); + if (FastSymmetryBreaking == 0) + return ResolveAutomorphismsFull(); + + result = ResolveElementAutomorphismsFast(); if (result != 0) - result = ResolveNodeAutomorphisms(); + result = ResolveNodeAutomorphismsFast(); return result; } @@ -7454,7 +7547,8 @@ static void handler(int sig) /*----------------------------------------------------------------------*/ /* Note that this cover-all routine is not called from the Tcl/Tk */ /* version, which replaces it with the script "lvs". */ -/* return 1 if the two are identical. Try to resolve automorphisms. */ +/* return 1 if the two are identical. Try to resolve automorphisms */ +/* using the original "full" symmetry breaking algorithm. */ /*----------------------------------------------------------------------*/ int Compare(char *cell1, char *cell2) diff --git a/base/netcmp.h b/base/netcmp.h index 9d289f0..fba1bb0 100644 --- a/base/netcmp.h +++ b/base/netcmp.h @@ -7,6 +7,7 @@ extern struct nlist *Circuit1; extern struct nlist *Circuit2; extern int ExhaustiveSubdivision; +extern int FastSymmetryBreaking; extern int left_col_end; extern int right_col_end; diff --git a/tcltk/tclnetgen.c b/tcltk/tclnetgen.c index 89e9f7d..05b0800 100644 --- a/tcltk/tclnetgen.c +++ b/tcltk/tclnetgen.c @@ -94,6 +94,7 @@ int _netcmp_ignore(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); int _netcmp_permute(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); int _netcmp_property(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); int _netcmp_exhaustive(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); +int _netcmp_symmetry(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); int _netcmp_restart(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); int _netcmp_global(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); int _netcmp_convert(ClientData, Tcl_Interp *, int, Tcl_Obj *CONST objv[]); @@ -244,6 +245,9 @@ Command netcmp_cmds[] = { {"exhaustive", _netcmp_exhaustive, "\n " "toggle exhaustive subdivision"}, + {"symmetry", _netcmp_symmetry, + "[fast|full]\n " + "apply method for symmetry breaking"}, {"restart", _netcmp_restart, "\n " "start over (reset data structures)"}, @@ -3972,6 +3976,48 @@ _netcmp_permute(ClientData clientData, return TCL_OK; } +/*------------------------------------------------------*/ +/* Function name: _netcmp_symmetry */ +/* Syntax: netgen::symmetry [fast|full] */ +/* Formerly: x */ +/* Results: */ +/* Side Effects: */ +/*------------------------------------------------------*/ + +int +_netcmp_symmetry(ClientData clientData, + Tcl_Interp *interp, int objc, Tcl_Obj *CONST objv[]) +{ + char *fastfull[] = { + "fast", "full", NULL + }; + enum OptionIdx { + FAST_IDX, FULL_IDX + }; + int result, index; + + if (objc == 1) + index = -1; + else { + if (Tcl_GetIndexFromObj(interp, objv[1], (CONST84 char **)fastfull, + "option", 0, &index) != TCL_OK) + return TCL_ERROR; + } + + switch(index) { + case FAST_IDX: + FastSymmetryBreaking = TRUE; + break; + case FULL_IDX: + FastSymmetryBreaking = FALSE; + break; + } + Printf("Symmetry breaking method: %s.\n", + FastSymmetryBreaking ? "FAST" : "FULL"); + + return TCL_OK; +} + /*------------------------------------------------------*/ /* Function name: _netcmp_exhaustive */ /* Syntax: netgen::exhaustive [on|off] */ @@ -3993,7 +4039,7 @@ _netcmp_exhaustive(ClientData clientData, int result, index; if (objc == 1) - index = YES_IDX; + index = -1; else { if (Tcl_GetIndexFromObj(interp, objv[1], (CONST84 char **)yesno, "option", 0, &index) != TCL_OK)