luke
/
netgen
mirror of https://github.com/RTimothyEdwards/netgen.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

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.
This commit is contained in:
Tim Edwards 2020-10-08 09:43:25 -04:00
parent 04dd4a64d5
commit 5e99fd5ef9
4 changed files with 151 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
VERSION
View File

@ -1 +1 @@
1.5.156
1.5.157

110
base/netcmp.c
View File

@ -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)

1
base/netcmp.h
View File

@ -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;

48
tcltk/tclnetgen.c
View File

@ -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)