ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
sparse.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/*
11 module: sparse.c
12
13 make_sparse is a last-step cleanup to reduce the total number
14 of literals in the cover.
15
16 This is done by reducing the "sparse" variables (using a modified
17 version of irredundant rather than reduce), followed by expanding
18 the "dense" variables (using modified version of expand).
19*/
20
21#include "espresso.h"
22
24
25
27pcover F, D, R;
28{
29 cost_t cost, best_cost;
30
31 cover_cost(F, &best_cost);
32
33 do {
34 EXECUTE(F = mv_reduce(F, D), MV_REDUCE_TIME, F, cost);
35 if (cost.total == best_cost.total)
36 break;
37 copy_cost(&cost, &best_cost);
38
39 EXECUTE(F = expand(F, R, TRUE), RAISE_IN_TIME, F, cost);
40 if (cost.total == best_cost.total)
41 break;
42 copy_cost(&cost, &best_cost);
43 } while (force_irredundant);
44
45 return F;
46}
47
48/*
49 mv_reduce -- perform an "optimal" reduction of the variables which
50 we desire to be sparse
51
52 This could be done using "reduce" and then saving just the desired
53 part of the reduction. Instead, this version uses IRRED to find
54 which cubes of an output are redundant. Note that this gets around
55 the cube-ordering problem.
56
57 In normal use, it is expected that the cover is irredundant and
58 hence no cubes will be reduced to the empty cube (however, this is
59 checked for and such cubes will be deleted)
60*/
61
64pcover F, D;
65{
66 register int i, var;
67 register pcube p, p1, last;
68 int index;
69 pcover F1, D1;
70 pcube *F_cube_table;
71
72 /* loop for each multiple-valued variable */
73 for(var = 0; var < cube.num_vars; var++) {
74
75 if (cube.sparse[var]) {
76
77 /* loop for each part of the variable */
78 for(i = cube.first_part[var]; i <= cube.last_part[var]; i++) {
79
80 /* remember mapping of F1 cubes back to F cubes */
81 F_cube_table = ALLOC(pcube, F->count);
82
83 /* 'cofactor' against part #i of variable #var */
84 F1 = new_cover(F->count);
85 foreach_set(F, last, p) {
86 if (is_in_set(p, i)) {
87 F_cube_table[F1->count] = p;
88 p1 = GETSET(F1, F1->count++);
89 (void) set_diff(p1, p, cube.var_mask[var]);
90 set_insert(p1, i);
91 }
92 }
93
94 /* 'cofactor' against part #i of variable #var */
95 /* not really necessary -- just more efficient ? */
96 D1 = new_cover(D->count);
97 foreach_set(D, last, p) {
98 if (is_in_set(p, i)) {
99 p1 = GETSET(D1, D1->count++);
100 (void) set_diff(p1, p, cube.var_mask[var]);
101 set_insert(p1, i);
102 }
103 }
104
105 mark_irredundant(F1, D1);
106
107 /* now remove part i from cubes which are redundant */
108 index = 0;
109 foreach_set(F1, last, p1) {
110 if (! TESTP(p1, ACTIVE)) {
111 p = F_cube_table[index];
112
113 /* don't reduce a variable which is full
114 * (unless it is the output variable)
115 */
116 if (var == cube.num_vars-1 ||
117 ! setp_implies(cube.var_mask[var], p)) {
118 set_remove(p, i);
119 }
120 RESET(p, PRIME);
121 }
122 index++;
123 }
124
125 free_cover(F1);
126 free_cover(D1);
127 FREE(F_cube_table);
128 }
129 }
130 }
131
132 /* Check if any cubes disappeared */
133 (void) sf_active(F);
134 for(var = 0; var < cube.num_vars; var++) {
135 if (cube.sparse[var]) {
136 foreach_active_set(F, last, p) {
137 if (setp_disjoint(p, cube.var_mask[var])) {
138 RESET(p, ACTIVE);
139 F->active_count--;
140 }
141 }
142 }
143 }
144
145 if (F->count != F->active_count) {
146 F = sf_inactive(F);
147 }
148 return F;
149}
151
#define TRUE
Definition abcBm.c:38
#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 mark_irredundant()
pcover expand()
pset_family sf_inactive()
void copy_cost()
pcover make_sparse()
#define is_in_set(set, e)
Definition espresso.h:170
#define TESTP(set, flag)
Definition espresso.h:124
struct cost_struct cost_t
#define set_insert(set, e)
Definition espresso.h:172
bool setp_disjoint()
#define ACTIVE
Definition espresso.h:129
#define foreach_active_set(R, last, p)
Definition espresso.h:139
#define RAISE_IN_TIME
Definition espresso.h:385
pset_family sf_active()
#define pcube
Definition espresso.h:261
#define EXECUTE(fct, i, S, cost)
Definition espresso.h:422
#define free_cover(r)
Definition espresso.h:266
#define GETSET(family, index)
Definition espresso.h:161
pset set_diff()
#define set_remove(set, e)
Definition espresso.h:171
#define foreach_set(R, last, p)
Definition espresso.h:135
bool setp_implies()
void cover_cost()
#define RESET(set, flag)
Definition espresso.h:123
#define PRIME
Definition espresso.h:127
bool force_irredundant
Definition globals.c:27
pcover mv_reduce()
#define new_cover(i)
Definition espresso.h:265
#define MV_REDUCE_TIME
Definition espresso.h:384
Cube * p
Definition exorList.c:222
Definition exor.h:123