|
| 1 | +#include <iostream> |
| 2 | +#include <list> |
| 3 | +#include <vector> |
| 4 | +#include <queue> |
| 5 | +#include <set> |
| 6 | +#include <map> |
| 7 | +#include <stdio.h> |
| 8 | +#include <stdlib.h> |
| 9 | +#include <strings.h> |
| 10 | +#include <string.h> |
| 11 | +#include <time.h> |
| 12 | +#include <algorithm> |
| 13 | +#include <ctime> |
| 14 | +#include <climits> |
| 15 | +#include <cassert> |
| 16 | +#include <sys/time.h> |
| 17 | +#include <sys/resource.h> |
| 18 | +#include <unistd.h> |
| 19 | + |
| 20 | +#include <ebmc/ebmc_base.h> |
| 21 | + |
| 22 | +#include "minisat/core/Solver.h" |
| 23 | +#include "minisat/simp/SimpSolver.h" |
| 24 | + |
| 25 | + |
| 26 | +using namespace std; |
| 27 | +#include "dnf_io.hh" |
| 28 | +#include "ccircuit.hh" |
| 29 | +#include "m0ic3.hh" |
| 30 | + |
| 31 | +/*==================================== |
| 32 | +
|
| 33 | + P R I N T _ A I G E R _ F O R M A T |
| 34 | +
|
| 35 | + ====================================*/ |
| 36 | +void CompInfo::print_aiger_format() |
| 37 | +{ |
| 38 | + |
| 39 | + int num_consts; |
| 40 | + int num_buffs; |
| 41 | + check_circuit(num_buffs,num_consts); |
| 42 | + // printf("num_buffs = %d\n",num_buffs); |
| 43 | + assert(num_consts <= 2); |
| 44 | + string full_name; |
| 45 | + assert(strlen(out_file) > 0); |
| 46 | + full_name = out_file; |
| 47 | + full_name += ".aag"; |
| 48 | + |
| 49 | + FILE *fp = fopen(full_name.c_str(),"w"); |
| 50 | + assert(fp!= NULL); |
| 51 | + |
| 52 | + DNF Gates; |
| 53 | + int out_ind = form_aiger_gates(Gates); |
| 54 | + |
| 55 | + int max_var = find_max_aiger_var(Gates); |
| 56 | + print_aiger_header(fp,max_var,Gates.size()); |
| 57 | + print_aiger_inps(fp); |
| 58 | + print_aiger_latches(fp); |
| 59 | + print_aiger_output(fp,Gates,out_ind); |
| 60 | + print_aiger_constrs(fp); |
| 61 | + print_aiger_gates(fp,Gates); |
| 62 | + fclose(fp); |
| 63 | +} /* end of function print_aiger_format */ |
| 64 | + |
| 65 | +/*======================================= |
| 66 | +
|
| 67 | + F O R M _ A I G E R _ G A T E S |
| 68 | +
|
| 69 | + =======================================*/ |
| 70 | +int CompInfo::form_aiger_gates(DNF &Gates) |
| 71 | +{ |
| 72 | + |
| 73 | + int ind = -1; |
| 74 | + assert(N->Outputs.size() == 1); |
| 75 | + size_t out_gate_ind = N->Outputs[0]; |
| 76 | + for (size_t i=0; i < N->Gate_list.size(); i++) { |
| 77 | + Gate &G = N->Gate_list[i]; |
| 78 | + if (G.gate_type == INPUT) continue; |
| 79 | + if (G.gate_type == LATCH) continue; |
| 80 | + if (G.func_type == CONST) continue; |
| 81 | + assert(G.ninputs <= 2); |
| 82 | + if (i == out_gate_ind) |
| 83 | + ind = Gates.size(); |
| 84 | + if (G.func_type == AND) { |
| 85 | + add_aiger_and_gate(Gates,i); |
| 86 | + continue; |
| 87 | + } |
| 88 | + assert(G.func_type == BUFFER); |
| 89 | + add_aiger_buffer(Gates,i); |
| 90 | + } |
| 91 | + assert(ind >= 0); |
| 92 | + return(ind); |
| 93 | + |
| 94 | +} /* end of function form_aiger_gates */ |
| 95 | +/*================================= |
| 96 | +
|
| 97 | + F I N D _ A I G E R _ L I T 1 |
| 98 | +
|
| 99 | + ================================*/ |
| 100 | +int CompInfo::find_aiger_lit1(int gate_ind,char polarity) |
| 101 | +{ |
| 102 | + |
| 103 | + Gate &G = N->get_gate(gate_ind); |
| 104 | + |
| 105 | + if (G.func_type == CONST) { |
| 106 | + if (G.F.size() > 0) return(1); |
| 107 | + else { |
| 108 | + assert(F.size() == 0); |
| 109 | + return(0); |
| 110 | + } |
| 111 | + } |
| 112 | + |
| 113 | + int lit = (gate_ind+1) << 1; |
| 114 | + if (polarity) return(lit+1); |
| 115 | + else return(lit); |
| 116 | + |
| 117 | +} /* end of function find_aiger_lit1 */ |
| 118 | + |
| 119 | +/*================================= |
| 120 | +
|
| 121 | + F I N D _ A I G E R _ L I T 2 |
| 122 | +
|
| 123 | + ================================*/ |
| 124 | +int CompInfo::find_aiger_lit2(int gate_ind,char polarity) |
| 125 | +{ |
| 126 | + |
| 127 | + |
| 128 | + int lit = (gate_ind+1) << 1; |
| 129 | + if (polarity) return(lit+1); |
| 130 | + else return(lit); |
| 131 | + |
| 132 | +} /* end of function find_aiger_lit2 */ |
| 133 | + |
| 134 | +/*======================================== |
| 135 | +
|
| 136 | + P R I N T _ A I G E R _ L A T C H E S |
| 137 | +
|
| 138 | + ======================================*/ |
| 139 | +void CompInfo::print_aiger_latches(FILE *fp) |
| 140 | +{ |
| 141 | + |
| 142 | + for (size_t i=0; i < N->Latches.size(); i++) { |
| 143 | + int gate_ind = N->Latches[i]; |
| 144 | + int lit = (gate_ind+1) << 1; |
| 145 | + fprintf(fp,"%d ",lit); |
| 146 | + Gate &G = N->get_gate(gate_ind); |
| 147 | + assert(G.Fanin_list.size() == 1); |
| 148 | + int next_lit = find_aiger_lit1(G.Fanin_list[0],0); |
| 149 | + fprintf(fp,"%d ",next_lit); |
| 150 | + if (G.init_value == 2) { |
| 151 | + fprintf(fp,"%d\n",lit); |
| 152 | + continue;} |
| 153 | + assert((G.init_value == 0) || (G.init_value == 1)); |
| 154 | + fprintf(fp,"%d\n",G.init_value); |
| 155 | + } |
| 156 | + |
| 157 | +} /* end of function print_aiger_latches */ |
| 158 | + |
| 159 | + |
| 160 | +/*======================================== |
| 161 | +
|
| 162 | + P R I N T _ A I G E R _ I N P S |
| 163 | +
|
| 164 | + ======================================*/ |
| 165 | +void CompInfo::print_aiger_inps(FILE *fp) |
| 166 | +{ |
| 167 | + |
| 168 | + for (size_t i=0; i < N->Inputs.size(); i++) { |
| 169 | + int gate_ind = N->Inputs[i]; |
| 170 | + fprintf(fp,"%d\n",(gate_ind+1)<<1); |
| 171 | + } |
| 172 | + |
| 173 | +} /* end of function print_aiger_inps */ |
| 174 | + |
| 175 | + |
| 176 | +/*======================================== |
| 177 | +
|
| 178 | + P R I N T _ A I G E R _ H E A D E R |
| 179 | +
|
| 180 | + ======================================*/ |
| 181 | +void CompInfo::print_aiger_header(FILE *fp,int max_var,int num_gates) |
| 182 | +{ |
| 183 | + |
| 184 | + fprintf(fp,"aag "); |
| 185 | + |
| 186 | + fprintf(fp,"%d ",max_var); |
| 187 | + fprintf(fp,"%d ",N->ninputs); |
| 188 | + fprintf(fp,"%d ",N->nlatches); |
| 189 | + fprintf(fp,"1 "); |
| 190 | + fprintf(fp,"%d",num_gates); |
| 191 | + if (Constr_gates.size() == 0) fprintf(fp,"\n"); |
| 192 | + else fprintf(fp," 0 %d\n",(int) Constr_gates.size()); |
| 193 | +} /* end of function print_aiger_header*/ |
| 194 | + |
| 195 | + |
| 196 | + |
| 197 | + |
| 198 | +/*============================== |
| 199 | +
|
| 200 | + C H E C K _ C I R C U I T |
| 201 | +
|
| 202 | + ===============================*/ |
| 203 | +void CompInfo::check_circuit(int &num_buffs,int &num_consts) |
| 204 | +{ |
| 205 | + |
| 206 | + num_consts = 0; |
| 207 | + num_buffs = 0; |
| 208 | + for (size_t i=0; i < N->Gate_list.size(); i++) { |
| 209 | + Gate &G = N->Gate_list[i]; |
| 210 | + if (G.gate_type == INPUT) continue; |
| 211 | + if (G.gate_type == LATCH) continue; |
| 212 | + assert(G.gate_type == GATE); |
| 213 | + bool cond = (G.func_type == AND); |
| 214 | + cond |= (G.func_type == BUFFER); |
| 215 | + cond |= (G.func_type == CONST); |
| 216 | + if (!cond) { |
| 217 | + p(); |
| 218 | + print_func_type(G); |
| 219 | + exit(100); |
| 220 | + } |
| 221 | + |
| 222 | + if (G.func_type == CONST) num_consts++; |
| 223 | + if (G.func_type == BUFFER) num_buffs++; |
| 224 | + |
| 225 | + if (G.ninputs != 2) { |
| 226 | + bool cond = (i == N->Gate_list.size()-2); |
| 227 | + cond |= (G.func_type == BUFFER); |
| 228 | + cond |= (G.func_type == CONST); |
| 229 | + if (!cond) { |
| 230 | + p(); |
| 231 | + printf("i = %d\n",i); |
| 232 | + printf("N->Gate_list.size() = %d\n",(int) N->Gate_list.size()); |
| 233 | + printf("G.ninputs = %d\n",G.ninputs); |
| 234 | + exit(100); |
| 235 | + } |
| 236 | + } |
| 237 | + } |
| 238 | + |
| 239 | +} /* end of function check_circuit */ |
0 commit comments