ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
equiv.c
Go to the documentation of this file.
1/*
2 * Revision Control Information
3 *
4 * $Source$
5 * $Author$
6 * $Revision$
7 * $Date$
8 *
9 */
10#include "espresso.h"
11
13
14
15
17pPLA PLA;
18{
19 int i, j, ipart, jpart, some_equiv;
20 pcover *R, *F;
21
22 some_equiv = FALSE;
23
24 makeup_labels(PLA);
25
26 F = ALLOC(pcover, cube.part_size[cube.output]);
27 R = ALLOC(pcover, cube.part_size[cube.output]);
28
29 for(i = 0; i < cube.part_size[cube.output]; i++) {
30 ipart = cube.first_part[cube.output] + i;
31 R[i] = cof_output(PLA->R, ipart);
32 F[i] = complement(cube1list(R[i]));
33 }
34
35 for(i = 0; i < cube.part_size[cube.output]-1; i++) {
36 for(j = i+1; j < cube.part_size[cube.output]; j++) {
37 ipart = cube.first_part[cube.output] + i;
38 jpart = cube.first_part[cube.output] + j;
39
40 if (check_equiv(F[i], F[j])) {
41 (void) printf("# Outputs %d and %d (%s and %s) are equivalent\n",
42 i, j, PLA->label[ipart], PLA->label[jpart]);
43 some_equiv = TRUE;
44 } else if (check_equiv(F[i], R[j])) {
45 (void) printf("# Outputs %d and NOT %d (%s and %s) are equivalent\n",
46 i, j, PLA->label[ipart], PLA->label[jpart]);
47 some_equiv = TRUE;
48 } else if (check_equiv(R[i], F[j])) {
49 (void) printf("# Outputs NOT %d and %d (%s and %s) are equivalent\n",
50 i, j, PLA->label[ipart], PLA->label[jpart]);
51 some_equiv = TRUE;
52 } else if (check_equiv(R[i], R[j])) {
53 (void) printf("# Outputs NOT %d and NOT %d (%s and %s) are equivalent\n",
54 i, j, PLA->label[ipart], PLA->label[jpart]);
55 some_equiv = TRUE;
56 }
57 }
58 }
59
60 if (! some_equiv) {
61 (void) printf("# No outputs are equivalent\n");
62 }
63
64 for(i = 0; i < cube.part_size[cube.output]; i++) {
65 free_cover(F[i]);
66 free_cover(R[i]);
67 }
68 FREE(F);
69 FREE(R);
70}
71
72
73
74int check_equiv(f1, f2)
75pcover f1, f2;
76{
77 register pcube *f1list, *f2list;
78 register pcube p, last;
79
80 f1list = cube1list(f1);
81 foreach_set(f2, last, p) {
82 if (! cube_is_covered(f1list, p)) {
83 return FALSE;
84 }
85 }
86 free_cubelist(f1list);
87
88 f2list = cube1list(f2);
89 foreach_set(f1, last, p) {
90 if (! cube_is_covered(f2list, p)) {
91 return FALSE;
92 }
93 }
94 free_cubelist(f2list);
95
96 return TRUE;
97}
99
#define TRUE
Definition abcBm.c:38
#define FALSE
Definition abcBm.c:37
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define ALLOC(type, num)
Definition avl.h:27
#define FREE(obj)
Definition avl.h:31
#define pcover
Definition espresso.h:264
void find_equiv_outputs()
struct PLA_t * pPLA
#define pcube
Definition espresso.h:261
int check_equiv()
#define free_cover(r)
Definition espresso.h:266
#define foreach_set(R, last, p)
Definition espresso.h:135
pcover cof_output()
bool cube_is_covered()
#define free_cubelist(T)
Definition espresso.h:267
pcube * cube1list()
pcover complement()
void makeup_labels()
Cube * p
Definition exorList.c:222
Definition exor.h:123