projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge remote-tracking branch 'origin/master' into eddie/shiftx2mux
[yosys.git] / frontends / verific / verific.cc
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 *
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
9 *
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
17 *
18 */
19
20 #include "kernel/yosys.h"
21 #include "kernel/sigtools.h"
22 #include "kernel/celltypes.h"
23 #include "kernel/log.h"
24 #include <stdlib.h>
25 #include <stdio.h>
26 #include <string.h>
27
28 #ifndef _WIN32
29 # include <unistd.h>
30 # include <dirent.h>
31 #endif
32
33 #include "frontends/verific/verific.h"
34
35 USING_YOSYS_NAMESPACE
36
37 #ifdef YOSYS_ENABLE_VERIFIC
38
39 #ifdef __clang__
40 #pragma clang diagnostic push
41 #pragma clang diagnostic ignored "-Woverloaded-virtual"
42 #endif
43
44 #include "veri_file.h"
45 #include "vhdl_file.h"
46 #include "hier_tree.h"
47 #include "VeriModule.h"
48 #include "VeriWrite.h"
49 #include "VhdlUnits.h"
50 #include "VeriLibrary.h"
51
52 #ifndef SYMBIOTIC_VERIFIC_API_VERSION
53 # error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
54 #endif
55
56 #if SYMBIOTIC_VERIFIC_API_VERSION < 1
57 # error "Please update your version of Symbiotic EDA flavored Verific."
58 #endif
59
60 #ifdef __clang__
61 #pragma clang diagnostic pop
62 #endif
63
64 #ifdef VERIFIC_NAMESPACE
65 using namespace Verific;
66 #endif
67
68 #endif
69
70 #ifdef YOSYS_ENABLE_VERIFIC
71 YOSYS_NAMESPACE_BEGIN
72
73 int verific_verbose;
74 bool verific_import_pending;
75 string verific_error_msg;
76 int verific_sva_fsm_limit;
77
78 vector<string> verific_incdirs, verific_libdirs;
79
80 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
81 {
82 string message_prefix = stringf("VERIFIC-%s [%s] ",
83 msg_type == VERIFIC_NONE ? "NONE" :
84 msg_type == VERIFIC_ERROR ? "ERROR" :
85 msg_type == VERIFIC_WARNING ? "WARNING" :
86 msg_type == VERIFIC_IGNORE ? "IGNORE" :
87 msg_type == VERIFIC_INFO ? "INFO" :
88 msg_type == VERIFIC_COMMENT ? "COMMENT" :
89 msg_type == VERIFIC_PROGRAM_ERROR ? "PROGRAM_ERROR" : "UNKNOWN", message_id);
90
91 string message = linefile ? stringf("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile)) : "";
92 message += vstringf(msg, args);
93
94 if (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_WARNING || msg_type == VERIFIC_PROGRAM_ERROR)
95 log_warning_noprefix("%s%s\n", message_prefix.c_str(), message.c_str());
96 else
97 log("%s%s\n", message_prefix.c_str(), message.c_str());
98
99 if (verific_error_msg.empty() && (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_PROGRAM_ERROR))
100 verific_error_msg = message;
101 }
102
103 string get_full_netlist_name(Netlist *nl)
104 {
105 if (nl->NumOfRefs() == 1) {
106 Instance *inst = (Instance*)nl->GetReferences()->GetLast();
107 return get_full_netlist_name(inst->Owner()) + "." + inst->Name();
108 }
109
110 return nl->CellBaseName();
111 }
112
113 // ==================================================================
114
115 VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
116 mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
117 mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover),
118 mode_fullinit(mode_fullinit)
119 {
120 }
121
122 RTLIL::SigBit VerificImporter::net_map_at(Net *net)
123 {
124 if (net->IsExternalTo(netlist))
125 log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
126 get_full_netlist_name(net->Owner()).c_str(), net->Name(), get_full_netlist_name(netlist).c_str());
127
128 return net_map.at(net);
129 }
130
131 bool is_blackbox(Netlist *nl)
132 {
133 if (nl->IsBlackBox() || nl->IsEmptyBox())
134 return true;
135
136 const char *attr = nl->GetAttValue("blackbox");
137 if (attr != nullptr && strcmp(attr, "0"))
138 return true;
139
140 return false;
141 }
142
143 RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj)
144 {
145 std::string s = stringf("$verific$%s", obj->Name());
146 if (obj->Linefile())
147 s += stringf("$%s:%d", Verific::LineFile::GetFileName(obj->Linefile()), Verific::LineFile::GetLineNo(obj->Linefile()));
148 s += stringf("$%d", autoidx++);
149 return s;
150 }
151
152 void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
153 {
154 MapIter mi;
155 Att *attr;
156
157 if (obj->Linefile())
158 attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
159
160 // FIXME: Parse numeric attributes
161 FOREACH_ATTRIBUTE(obj, mi, attr) {
162 if (attr->Key()[0] == ' ' || attr->Value() == nullptr)
163 continue;
164 attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
165 }
166 }
167
168 RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
169 {
170 RTLIL::SigSpec sig;
171 for (int i = int(inst->InputSize())-1; i >= 0; i--)
172 if (inst->GetInputBit(i))
173 sig.append(net_map_at(inst->GetInputBit(i)));
174 else
175 sig.append(RTLIL::State::Sz);
176 return sig;
177 }
178
179 RTLIL::SigSpec VerificImporter::operatorInput1(Instance *inst)
180 {
181 RTLIL::SigSpec sig;
182 for (int i = int(inst->Input1Size())-1; i >= 0; i--)
183 if (inst->GetInput1Bit(i))
184 sig.append(net_map_at(inst->GetInput1Bit(i)));
185 else
186 sig.append(RTLIL::State::Sz);
187 return sig;
188 }
189
190 RTLIL::SigSpec VerificImporter::operatorInput2(Instance *inst)
191 {
192 RTLIL::SigSpec sig;
193 for (int i = int(inst->Input2Size())-1; i >= 0; i--)
194 if (inst->GetInput2Bit(i))
195 sig.append(net_map_at(inst->GetInput2Bit(i)));
196 else
197 sig.append(RTLIL::State::Sz);
198 return sig;
199 }
200
201 RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portname)
202 {
203 PortBus *portbus = inst->View()->GetPortBus(portname);
204 if (portbus) {
205 RTLIL::SigSpec sig;
206 for (unsigned i = 0; i < portbus->Size(); i++) {
207 Net *net = inst->GetNet(portbus->ElementAtIndex(i));
208 if (net) {
209 if (net->IsGnd())
210 sig.append(RTLIL::State::S0);
211 else if (net->IsPwr())
212 sig.append(RTLIL::State::S1);
213 else
214 sig.append(net_map_at(net));
215 } else
216 sig.append(RTLIL::State::Sz);
217 }
218 return sig;
219 } else {
220 Port *port = inst->View()->GetPort(portname);
221 log_assert(port != NULL);
222 Net *net = inst->GetNet(port);
223 return net_map_at(net);
224 }
225 }
226
227 RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets)
228 {
229 RTLIL::SigSpec sig;
230 RTLIL::Wire *dummy_wire = NULL;
231 for (int i = int(inst->OutputSize())-1; i >= 0; i--)
232 if (inst->GetOutputBit(i) && (!any_all_nets || !any_all_nets->count(inst->GetOutputBit(i)))) {
233 sig.append(net_map_at(inst->GetOutputBit(i)));
234 dummy_wire = NULL;
235 } else {
236 if (dummy_wire == NULL)
237 dummy_wire = module->addWire(new_verific_id(inst));
238 else
239 dummy_wire->width++;
240 sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
241 }
242 return sig;
243 }
244
245 bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
246 {
247 if (inst->Type() == PRIM_AND) {
248 module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
249 return true;
250 }
251
252 if (inst->Type() == PRIM_NAND) {
253 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
254 module->addAndGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
255 module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
256 return true;
257 }
258
259 if (inst->Type() == PRIM_OR) {
260 module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
261 return true;
262 }
263
264 if (inst->Type() == PRIM_NOR) {
265 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
266 module->addOrGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
267 module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
268 return true;
269 }
270
271 if (inst->Type() == PRIM_XOR) {
272 module->addXorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
273 return true;
274 }
275
276 if (inst->Type() == PRIM_XNOR) {
277 module->addXnorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
278 return true;
279 }
280
281 if (inst->Type() == PRIM_BUF) {
282 auto outnet = inst->GetOutput();
283 if (!any_all_nets.count(outnet))
284 module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
285 return true;
286 }
287
288 if (inst->Type() == PRIM_INV) {
289 module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
290 return true;
291 }
292
293 if (inst->Type() == PRIM_MUX) {
294 module->addMuxGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
295 return true;
296 }
297
298 if (inst->Type() == PRIM_TRI) {
299 module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
300 return true;
301 }
302
303 if (inst->Type() == PRIM_FADD)
304 {
305 RTLIL::SigSpec a = net_map_at(inst->GetInput1()), b = net_map_at(inst->GetInput2()), c = net_map_at(inst->GetCin());
306 RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(new_verific_id(inst));
307 RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
308 RTLIL::SigSpec tmp1 = module->addWire(new_verific_id(inst));
309 RTLIL::SigSpec tmp2 = module->addWire(new_verific_id(inst));
310 RTLIL::SigSpec tmp3 = module->addWire(new_verific_id(inst));
311 module->addXorGate(new_verific_id(inst), a, b, tmp1);
312 module->addXorGate(inst_name, tmp1, c, y);
313 module->addAndGate(new_verific_id(inst), tmp1, c, tmp2);
314 module->addAndGate(new_verific_id(inst), a, b, tmp3);
315 module->addOrGate(new_verific_id(inst), tmp2, tmp3, x);
316 return true;
317 }
318
319 if (inst->Type() == PRIM_DFFRS)
320 {
321 VerificClocking clocking(this, inst->GetClock());
322 log_assert(clocking.disable_sig == State::S0);
323 log_assert(clocking.body_net == nullptr);
324
325 if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
326 clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
327 else if (inst->GetSet()->IsGnd())
328 clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S0);
329 else if (inst->GetReset()->IsGnd())
330 clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S1);
331 else
332 clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
333 net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
334 return true;
335 }
336
337 return false;
338 }
339
340 bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
341 {
342 RTLIL::Cell *cell = nullptr;
343
344 if (inst->Type() == PRIM_AND) {
345 cell = module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
346 import_attributes(cell->attributes, inst);
347 return true;
348 }
349
350 if (inst->Type() == PRIM_NAND) {
351 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
352 cell = module->addAnd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
353 import_attributes(cell->attributes, inst);
354 cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
355 import_attributes(cell->attributes, inst);
356 return true;
357 }
358
359 if (inst->Type() == PRIM_OR) {
360 cell = module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
361 import_attributes(cell->attributes, inst);
362 return true;
363 }
364
365 if (inst->Type() == PRIM_NOR) {
366 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
367 cell = module->addOr(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
368 import_attributes(cell->attributes, inst);
369 cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
370 import_attributes(cell->attributes, inst);
371 return true;
372 }
373
374 if (inst->Type() == PRIM_XOR) {
375 cell = module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
376 import_attributes(cell->attributes, inst);
377 return true;
378 }
379
380 if (inst->Type() == PRIM_XNOR) {
381 cell = module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
382 import_attributes(cell->attributes, inst);
383 return true;
384 }
385
386 if (inst->Type() == PRIM_INV) {
387 cell = module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
388 import_attributes(cell->attributes, inst);
389 return true;
390 }
391
392 if (inst->Type() == PRIM_MUX) {
393 cell = module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
394 import_attributes(cell->attributes, inst);
395 return true;
396 }
397
398 if (inst->Type() == PRIM_TRI) {
399 cell = module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
400 import_attributes(cell->attributes, inst);
401 return true;
402 }
403
404 if (inst->Type() == PRIM_FADD)
405 {
406 RTLIL::SigSpec a_plus_b = module->addWire(new_verific_id(inst), 2);
407 RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
408 if (inst->GetCout())
409 y.append(net_map_at(inst->GetCout()));
410 cell = module->addAdd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
411 import_attributes(cell->attributes, inst);
412 cell = module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
413 import_attributes(cell->attributes, inst);
414 return true;
415 }
416
417 if (inst->Type() == PRIM_DFFRS)
418 {
419 VerificClocking clocking(this, inst->GetClock());
420 log_assert(clocking.disable_sig == State::S0);
421 log_assert(clocking.body_net == nullptr);
422
423 if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
424 cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
425 else if (inst->GetSet()->IsGnd())
426 cell = clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
427 else if (inst->GetReset()->IsGnd())
428 cell = clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
429 else
430 cell = clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
431 net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
432 import_attributes(cell->attributes, inst);
433 return true;
434 }
435
436 if (inst->Type() == PRIM_DLATCHRS)
437 {
438 if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
439 cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
440 else
441 cell = module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
442 net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
443 import_attributes(cell->attributes, inst);
444 return true;
445 }
446
447 #define IN operatorInput(inst)
448 #define IN1 operatorInput1(inst)
449 #define IN2 operatorInput2(inst)
450 #define OUT operatorOutput(inst)
451 #define FILTERED_OUT operatorOutput(inst, &any_all_nets)
452 #define SIGNED inst->View()->IsSigned()
453
454 if (inst->Type() == OPER_ADDER) {
455 RTLIL::SigSpec out = OUT;
456 if (inst->GetCout() != NULL)
457 out.append(net_map_at(inst->GetCout()));
458 if (inst->GetCin()->IsGnd()) {
459 cell = module->addAdd(inst_name, IN1, IN2, out, SIGNED);
460 import_attributes(cell->attributes, inst);
461 } else {
462 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst), GetSize(out));
463 cell = module->addAdd(new_verific_id(inst), IN1, IN2, tmp, SIGNED);
464 import_attributes(cell->attributes, inst);
465 cell = module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
466 import_attributes(cell->attributes, inst);
467 }
468 return true;
469 }
470
471 if (inst->Type() == OPER_MULTIPLIER) {
472 cell = module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
473 import_attributes(cell->attributes, inst);
474 return true;
475 }
476
477 if (inst->Type() == OPER_DIVIDER) {
478 cell = module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
479 import_attributes(cell->attributes, inst);
480 return true;
481 }
482
483 if (inst->Type() == OPER_MODULO) {
484 cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
485 import_attributes(cell->attributes, inst);
486 return true;
487 }
488
489 if (inst->Type() == OPER_REMAINDER) {
490 cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
491 import_attributes(cell->attributes, inst);
492 return true;
493 }
494
495 if (inst->Type() == OPER_SHIFT_LEFT) {
496 cell = module->addShl(inst_name, IN1, IN2, OUT, false);
497 import_attributes(cell->attributes, inst);
498 return true;
499 }
500
501 if (inst->Type() == OPER_ENABLED_DECODER) {
502 RTLIL::SigSpec vec;
503 vec.append(net_map_at(inst->GetControl()));
504 for (unsigned i = 1; i < inst->OutputSize(); i++) {
505 vec.append(RTLIL::State::S0);
506 }
507 cell = module->addShl(inst_name, vec, IN, OUT, false);
508 import_attributes(cell->attributes, inst);
509 return true;
510 }
511
512 if (inst->Type() == OPER_DECODER) {
513 RTLIL::SigSpec vec;
514 vec.append(RTLIL::State::S1);
515 for (unsigned i = 1; i < inst->OutputSize(); i++) {
516 vec.append(RTLIL::State::S0);
517 }
518 cell = module->addShl(inst_name, vec, IN, OUT, false);
519 import_attributes(cell->attributes, inst);
520 return true;
521 }
522
523 if (inst->Type() == OPER_SHIFT_RIGHT) {
524 Net *net_cin = inst->GetCin();
525 Net *net_a_msb = inst->GetInput1Bit(0);
526 if (net_cin->IsGnd())
527 cell = module->addShr(inst_name, IN1, IN2, OUT, false);
528 else if (net_cin == net_a_msb)
529 cell = module->addSshr(inst_name, IN1, IN2, OUT, true);
530 else
531 log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
532 import_attributes(cell->attributes, inst);
533 return true;
534 }
535
536 if (inst->Type() == OPER_REDUCE_AND) {
537 cell = module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
538 import_attributes(cell->attributes, inst);
539 return true;
540 }
541
542 if (inst->Type() == OPER_REDUCE_NAND) {
543 Wire *tmp = module->addWire(NEW_ID);
544 cell = module->addReduceAnd(inst_name, IN, tmp, SIGNED);
545 module->addNot(NEW_ID, tmp, net_map_at(inst->GetOutput()));
546 import_attributes(cell->attributes, inst);
547 return true;
548 }
549
550 if (inst->Type() == OPER_REDUCE_OR) {
551 cell = module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
552 import_attributes(cell->attributes, inst);
553 return true;
554 }
555
556 if (inst->Type() == OPER_REDUCE_XOR) {
557 cell = module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
558 import_attributes(cell->attributes, inst);
559 return true;
560 }
561
562 if (inst->Type() == OPER_REDUCE_XNOR) {
563 cell = module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
564 import_attributes(cell->attributes, inst);
565 return true;
566 }
567
568 if (inst->Type() == OPER_REDUCE_NOR) {
569 SigSpec t = module->ReduceOr(new_verific_id(inst), IN, SIGNED);
570 cell = module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
571 import_attributes(cell->attributes, inst);
572 return true;
573 }
574
575 if (inst->Type() == OPER_LESSTHAN) {
576 Net *net_cin = inst->GetCin();
577 if (net_cin->IsGnd())
578 cell = module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
579 else if (net_cin->IsPwr())
580 cell = module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
581 else
582 log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
583 import_attributes(cell->attributes, inst);
584 return true;
585 }
586
587 if (inst->Type() == OPER_WIDE_AND) {
588 cell = module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
589 import_attributes(cell->attributes, inst);
590 return true;
591 }
592
593 if (inst->Type() == OPER_WIDE_OR) {
594 cell = module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
595 import_attributes(cell->attributes, inst);
596 return true;
597 }
598
599 if (inst->Type() == OPER_WIDE_XOR) {
600 cell = module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
601 import_attributes(cell->attributes, inst);
602 return true;
603 }
604
605 if (inst->Type() == OPER_WIDE_XNOR) {
606 cell = module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
607 import_attributes(cell->attributes, inst);
608 return true;
609 }
610
611 if (inst->Type() == OPER_WIDE_BUF) {
612 cell = module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
613 import_attributes(cell->attributes, inst);
614 return true;
615 }
616
617 if (inst->Type() == OPER_WIDE_INV) {
618 cell = module->addNot(inst_name, IN, OUT, SIGNED);
619 import_attributes(cell->attributes, inst);
620 return true;
621 }
622
623 if (inst->Type() == OPER_MINUS) {
624 cell = module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
625 import_attributes(cell->attributes, inst);
626 return true;
627 }
628
629 if (inst->Type() == OPER_UMINUS) {
630 cell = module->addNeg(inst_name, IN, OUT, SIGNED);
631 import_attributes(cell->attributes, inst);
632 return true;
633 }
634
635 if (inst->Type() == OPER_EQUAL) {
636 cell = module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
637 import_attributes(cell->attributes, inst);
638 return true;
639 }
640
641 if (inst->Type() == OPER_NEQUAL) {
642 cell = module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
643 import_attributes(cell->attributes, inst);
644 return true;
645 }
646
647 if (inst->Type() == OPER_WIDE_MUX) {
648 cell = module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
649 import_attributes(cell->attributes, inst);
650 return true;
651 }
652
653 if (inst->Type() == OPER_NTO1MUX) {
654 cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
655 import_attributes(cell->attributes, inst);
656 return true;
657 }
658
659 if (inst->Type() == OPER_WIDE_NTO1MUX)
660 {
661 SigSpec data = IN2, out = OUT;
662
663 int wordsize_bits = ceil_log2(GetSize(out));
664 int wordsize = 1 << wordsize_bits;
665
666 SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)};
667
668 SigSpec padded_data;
669 for (int i = 0; i < GetSize(data); i += GetSize(out)) {
670 SigSpec d = data.extract(i, GetSize(out));
671 d.extend_u0(wordsize);
672 padded_data.append(d);
673 }
674
675 cell = module->addShr(inst_name, padded_data, sel, out);
676 import_attributes(cell->attributes, inst);
677 return true;
678 }
679
680 if (inst->Type() == OPER_SELECTOR)
681 {
682 cell = module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
683 import_attributes(cell->attributes, inst);
684 return true;
685 }
686
687 if (inst->Type() == OPER_WIDE_SELECTOR)
688 {
689 SigSpec out = OUT;
690 cell = module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
691 import_attributes(cell->attributes, inst);
692 return true;
693 }
694
695 if (inst->Type() == OPER_WIDE_TRI) {
696 cell = module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
697 import_attributes(cell->attributes, inst);
698 return true;
699 }
700
701 if (inst->Type() == OPER_WIDE_DFFRS)
702 {
703 VerificClocking clocking(this, inst->GetClock());
704 log_assert(clocking.disable_sig == State::S0);
705 log_assert(clocking.body_net == nullptr);
706
707 RTLIL::SigSpec sig_set = operatorInport(inst, "set");
708 RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
709
710 if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
711 cell = clocking.addDff(inst_name, IN, OUT);
712 else
713 cell = clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
714 import_attributes(cell->attributes, inst);
715
716 return true;
717 }
718
719 #undef IN
720 #undef IN1
721 #undef IN2
722 #undef OUT
723 #undef SIGNED
724
725 return false;
726 }
727
728 void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
729 {
730 bool keep_running = true;
731 SigMap sigmap;
732
733 while (keep_running)
734 {
735 keep_running = false;
736
737 dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
738 SigSpec dbits;
739
740 for (auto cell : candidates) {
741 SigBit bit = sigmap(cell->getPort("\\D"));
742 dbits_db[bit].insert(cell);
743 dbits.append(bit);
744 }
745
746 dbits.sort_and_unify();
747
748 for (auto chunk : dbits.chunks())
749 {
750 SigSpec sig_d = chunk;
751
752 if (chunk.wire == nullptr || GetSize(sig_d) == 1)
753 continue;
754
755 SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
756 RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);
757
758 if (verific_verbose)
759 log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
760
761 for (int i = 0; i < GetSize(sig_d); i++)
762 for (auto old_ff : dbits_db[sig_d[i]])
763 {
764 if (verific_verbose)
765 log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i);
766
767 SigBit old_q = old_ff->getPort("\\Q");
768 SigBit new_q = sig_q[i];
769
770 sigmap.add(old_q, new_q);
771 module->connect(old_q, new_q);
772 candidates.erase(old_ff);
773 module->remove(old_ff);
774 keep_running = true;
775 }
776 }
777 }
778 }
779
780 void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
781 {
782 dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
783
784 for (auto cell : candidates)
785 {
786 SigBit clock = cell->getPort("\\CLK");
787 bool clock_pol = cell->getParam("\\CLK_POLARITY").as_bool();
788 database[make_pair(clock, int(clock_pol))].insert(cell);
789 }
790
791 for (auto it : database)
792 merge_past_ffs_clock(it.second, it.first.first, it.first.second);
793 }
794
795 void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename)
796 {
797 std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
798 std::string module_name = netlist_name;
799
800 if (nl->IsOperator() || nl->IsPrimitive()) {
801 module_name = "$verific$" + module_name;
802 } else {
803 if (!norename && *nl->Name()) {
804 module_name += "(";
805 module_name += nl->Name();
806 module_name += ")";
807 }
808 module_name = "\\" + module_name;
809 }
810
811 netlist = nl;
812
813 if (design->has(module_name)) {
814 if (!nl->IsOperator() && !is_blackbox(nl))
815 log_cmd_error("Re-definition of module `%s'.\n", netlist_name.c_str());
816 return;
817 }
818
819 module = new RTLIL::Module;
820 module->name = module_name;
821 design->add(module);
822
823 if (is_blackbox(nl)) {
824 log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
825 module->set_bool_attribute("\\blackbox");
826 } else {
827 log("Importing module %s.\n", RTLIL::id2cstr(module->name));
828 }
829
830 SetIter si;
831 MapIter mi, mi2;
832 Port *port;
833 PortBus *portbus;
834 Net *net;
835 NetBus *netbus;
836 Instance *inst;
837 PortRef *pr;
838
839 FOREACH_PORT_OF_NETLIST(nl, mi, port)
840 {
841 if (port->Bus())
842 continue;
843
844 if (verific_verbose)
845 log(" importing port %s.\n", port->Name());
846
847 RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
848 import_attributes(wire->attributes, port);
849
850 wire->port_id = nl->IndexOf(port) + 1;
851
852 if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
853 wire->port_input = true;
854 if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
855 wire->port_output = true;
856
857 if (port->GetNet()) {
858 net = port->GetNet();
859 if (net_map.count(net) == 0)
860 net_map[net] = wire;
861 else if (wire->port_input)
862 module->connect(net_map_at(net), wire);
863 else
864 module->connect(wire, net_map_at(net));
865 }
866 }
867
868 FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
869 {
870 if (verific_verbose)
871 log(" importing portbus %s.\n", portbus->Name());
872
873 RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
874 wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
875 import_attributes(wire->attributes, portbus);
876
877 if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
878 wire->port_input = true;
879 if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
880 wire->port_output = true;
881
882 for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
883 if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
884 net = portbus->ElementAtIndex(i)->GetNet();
885 RTLIL::SigBit bit(wire, i - wire->start_offset);
886 if (net_map.count(net) == 0)
887 net_map[net] = bit;
888 else if (wire->port_input)
889 module->connect(net_map_at(net), bit);
890 else
891 module->connect(bit, net_map_at(net));
892 }
893 if (i == portbus->RightIndex())
894 break;
895 }
896 }
897
898 module->fixup_ports();
899
900 dict<Net*, char, hash_ptr_ops> init_nets;
901 pool<Net*, hash_ptr_ops> anyconst_nets, anyseq_nets;
902 pool<Net*, hash_ptr_ops> allconst_nets, allseq_nets;
903 any_all_nets.clear();
904
905 FOREACH_NET_OF_NETLIST(nl, mi, net)
906 {
907 if (net->IsRamNet())
908 {
909 RTLIL::Memory *memory = new RTLIL::Memory;
910 memory->name = RTLIL::escape_id(net->Name());
911 log_assert(module->count_id(memory->name) == 0);
912 module->memories[memory->name] = memory;
913
914 int number_of_bits = net->Size();
915 int bits_in_word = number_of_bits;
916 FOREACH_PORTREF_OF_NET(net, si, pr) {
917 if (pr->GetInst()->Type() == OPER_READ_PORT) {
918 bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
919 continue;
920 }
921 if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
922 bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
923 continue;
924 }
925 log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
926 net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
927 }
928
929 memory->width = bits_in_word;
930 memory->size = number_of_bits / bits_in_word;
931
932 const char *ascii_initdata = net->GetWideInitialValue();
933 if (ascii_initdata) {
934 while (*ascii_initdata != 0 && *ascii_initdata != '\'')
935 ascii_initdata++;
936 if (*ascii_initdata == '\'')
937 ascii_initdata++;
938 if (*ascii_initdata != 0) {
939 log_assert(*ascii_initdata == 'b');
940 ascii_initdata++;
941 }
942 for (int word_idx = 0; word_idx < memory->size; word_idx++) {
943 Const initval = Const(State::Sx, memory->width);
944 bool initval_valid = false;
945 for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
946 if (*ascii_initdata == 0)
947 break;
948 if (*ascii_initdata == '0' || *ascii_initdata == '1') {
949 initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
950 initval_valid = true;
951 }
952 ascii_initdata++;
953 }
954 if (initval_valid) {
955 RTLIL::Cell *cell = module->addCell(new_verific_id(net), "$meminit");
956 cell->parameters["\\WORDS"] = 1;
957 if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
958 cell->setPort("\\ADDR", word_idx);
959 else
960 cell->setPort("\\ADDR", memory->size - word_idx - 1);
961 cell->setPort("\\DATA", initval);
962 cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str());
963 cell->parameters["\\ABITS"] = 32;
964 cell->parameters["\\WIDTH"] = memory->width;
965 cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1);
966 }
967 }
968 }
969 continue;
970 }
971
972 if (net->GetInitialValue())
973 init_nets[net] = net->GetInitialValue();
974
975 const char *rand_const_attr = net->GetAttValue(" rand_const");
976 const char *rand_attr = net->GetAttValue(" rand");
977
978 const char *anyconst_attr = net->GetAttValue("anyconst");
979 const char *anyseq_attr = net->GetAttValue("anyseq");
980
981 const char *allconst_attr = net->GetAttValue("allconst");
982 const char *allseq_attr = net->GetAttValue("allseq");
983
984 if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) {
985 anyconst_nets.insert(net);
986 any_all_nets.insert(net);
987 }
988 else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) {
989 anyseq_nets.insert(net);
990 any_all_nets.insert(net);
991 }
992 else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) {
993 anyconst_nets.insert(net);
994 any_all_nets.insert(net);
995 }
996 else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) {
997 anyseq_nets.insert(net);
998 any_all_nets.insert(net);
999 }
1000 else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) {
1001 allconst_nets.insert(net);
1002 any_all_nets.insert(net);
1003 }
1004 else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'"))) {
1005 allseq_nets.insert(net);
1006 any_all_nets.insert(net);
1007 }
1008
1009 if (net_map.count(net)) {
1010 if (verific_verbose)
1011 log(" skipping net %s.\n", net->Name());
1012 continue;
1013 }
1014
1015 if (net->Bus())
1016 continue;
1017
1018 RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : new_verific_id(net));
1019
1020 if (verific_verbose)
1021 log(" importing net %s as %s.\n", net->Name(), log_id(wire_name));
1022
1023 RTLIL::Wire *wire = module->addWire(wire_name);
1024 import_attributes(wire->attributes, net);
1025
1026 net_map[net] = wire;
1027 }
1028
1029 FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
1030 {
1031 bool found_new_net = false;
1032 for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
1033 net = netbus->ElementAtIndex(i);
1034 if (net_map.count(net) == 0)
1035 found_new_net = true;
1036 if (i == netbus->RightIndex())
1037 break;
1038 }
1039
1040 if (found_new_net)
1041 {
1042 RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : new_verific_id(netbus));
1043
1044 if (verific_verbose)
1045 log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
1046
1047 RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
1048 wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
1049 import_attributes(wire->attributes, netbus);
1050
1051 RTLIL::Const initval = Const(State::Sx, GetSize(wire));
1052 bool initval_valid = false;
1053
1054 for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
1055 {
1056 if (netbus->ElementAtIndex(i))
1057 {
1058 int bitidx = i - wire->start_offset;
1059 net = netbus->ElementAtIndex(i);
1060 RTLIL::SigBit bit(wire, bitidx);
1061
1062 if (init_nets.count(net)) {
1063 if (init_nets.at(net) == '0')
1064 initval.bits.at(bitidx) = State::S0;
1065 if (init_nets.at(net) == '1')
1066 initval.bits.at(bitidx) = State::S1;
1067 initval_valid = true;
1068 init_nets.erase(net);
1069 }
1070
1071 if (net_map.count(net) == 0)
1072 net_map[net] = bit;
1073 else
1074 module->connect(bit, net_map_at(net));
1075 }
1076
1077 if (i == netbus->RightIndex())
1078 break;
1079 }
1080
1081 if (initval_valid)
1082 wire->attributes["\\init"] = initval;
1083 }
1084 else
1085 {
1086 if (verific_verbose)
1087 log(" skipping netbus %s.\n", netbus->Name());
1088 }
1089
1090 SigSpec anyconst_sig;
1091 SigSpec anyseq_sig;
1092 SigSpec allconst_sig;
1093 SigSpec allseq_sig;
1094
1095 for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
1096 net = netbus->ElementAtIndex(i);
1097 if (net != nullptr && anyconst_nets.count(net)) {
1098 anyconst_sig.append(net_map_at(net));
1099 anyconst_nets.erase(net);
1100 }
1101 if (net != nullptr && anyseq_nets.count(net)) {
1102 anyseq_sig.append(net_map_at(net));
1103 anyseq_nets.erase(net);
1104 }
1105 if (net != nullptr && allconst_nets.count(net)) {
1106 allconst_sig.append(net_map_at(net));
1107 allconst_nets.erase(net);
1108 }
1109 if (net != nullptr && allseq_nets.count(net)) {
1110 allseq_sig.append(net_map_at(net));
1111 allseq_nets.erase(net);
1112 }
1113 if (i == netbus->LeftIndex())
1114 break;
1115 }
1116
1117 if (GetSize(anyconst_sig))
1118 module->connect(anyconst_sig, module->Anyconst(new_verific_id(netbus), GetSize(anyconst_sig)));
1119
1120 if (GetSize(anyseq_sig))
1121 module->connect(anyseq_sig, module->Anyseq(new_verific_id(netbus), GetSize(anyseq_sig)));
1122
1123 if (GetSize(allconst_sig))
1124 module->connect(allconst_sig, module->Allconst(new_verific_id(netbus), GetSize(allconst_sig)));
1125
1126 if (GetSize(allseq_sig))
1127 module->connect(allseq_sig, module->Allseq(new_verific_id(netbus), GetSize(allseq_sig)));
1128 }
1129
1130 for (auto it : init_nets)
1131 {
1132 Const initval;
1133 SigBit bit = net_map_at(it.first);
1134 log_assert(bit.wire);
1135
1136 if (bit.wire->attributes.count("\\init"))
1137 initval = bit.wire->attributes.at("\\init");
1138
1139 while (GetSize(initval) < GetSize(bit.wire))
1140 initval.bits.push_back(State::Sx);
1141
1142 if (it.second == '0')
1143 initval.bits.at(bit.offset) = State::S0;
1144 if (it.second == '1')
1145 initval.bits.at(bit.offset) = State::S1;
1146
1147 bit.wire->attributes["\\init"] = initval;
1148 }
1149
1150 for (auto net : anyconst_nets)
1151 module->connect(net_map_at(net), module->Anyconst(new_verific_id(net)));
1152
1153 for (auto net : anyseq_nets)
1154 module->connect(net_map_at(net), module->Anyseq(new_verific_id(net)));
1155
1156 pool<Instance*, hash_ptr_ops> sva_asserts;
1157 pool<Instance*, hash_ptr_ops> sva_assumes;
1158 pool<Instance*, hash_ptr_ops> sva_covers;
1159 pool<Instance*, hash_ptr_ops> sva_triggers;
1160
1161 pool<RTLIL::Cell*> past_ffs;
1162
1163 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1164 {
1165 RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : new_verific_id(inst));
1166
1167 if (verific_verbose)
1168 log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
1169
1170 if (mode_verific)
1171 goto import_verific_cells;
1172
1173 if (inst->Type() == PRIM_PWR) {
1174 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
1175 continue;
1176 }
1177
1178 if (inst->Type() == PRIM_GND) {
1179 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
1180 continue;
1181 }
1182
1183 if (inst->Type() == PRIM_BUF) {
1184 auto outnet = inst->GetOutput();
1185 if (!any_all_nets.count(outnet))
1186 module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
1187 continue;
1188 }
1189
1190 if (inst->Type() == PRIM_X) {
1191 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
1192 continue;
1193 }
1194
1195 if (inst->Type() == PRIM_Z) {
1196 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
1197 continue;
1198 }
1199
1200 if (inst->Type() == OPER_READ_PORT)
1201 {
1202 RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
1203 int numchunks = int(inst->OutputSize()) / memory->width;
1204 int chunksbits = ceil_log2(numchunks);
1205
1206 if ((numchunks * memory->width) != int(inst->OutputSize()) || (numchunks & (numchunks - 1)) != 0)
1207 log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
1208
1209 for (int i = 0; i < numchunks; i++)
1210 {
1211 RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
1212 RTLIL::SigSpec data = operatorOutput(inst).extract(i * memory->width, memory->width);
1213
1214 RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
1215 RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memrd");
1216 cell->parameters["\\MEMID"] = memory->name.str();
1217 cell->parameters["\\CLK_ENABLE"] = false;
1218 cell->parameters["\\CLK_POLARITY"] = true;
1219 cell->parameters["\\TRANSPARENT"] = false;
1220 cell->parameters["\\ABITS"] = GetSize(addr);
1221 cell->parameters["\\WIDTH"] = GetSize(data);
1222 cell->setPort("\\CLK", RTLIL::State::Sx);
1223 cell->setPort("\\EN", RTLIL::State::Sx);
1224 cell->setPort("\\ADDR", addr);
1225 cell->setPort("\\DATA", data);
1226 }
1227 continue;
1228 }
1229
1230 if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
1231 {
1232 RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
1233 int numchunks = int(inst->Input2Size()) / memory->width;
1234 int chunksbits = ceil_log2(numchunks);
1235
1236 if ((numchunks * memory->width) != int(inst->Input2Size()) || (numchunks & (numchunks - 1)) != 0)
1237 log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetOutput()->Name());
1238
1239 for (int i = 0; i < numchunks; i++)
1240 {
1241 RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
1242 RTLIL::SigSpec data = operatorInput2(inst).extract(i * memory->width, memory->width);
1243
1244 RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
1245 RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memwr");
1246 cell->parameters["\\MEMID"] = memory->name.str();
1247 cell->parameters["\\CLK_ENABLE"] = false;
1248 cell->parameters["\\CLK_POLARITY"] = true;
1249 cell->parameters["\\PRIORITY"] = 0;
1250 cell->parameters["\\ABITS"] = GetSize(addr);
1251 cell->parameters["\\WIDTH"] = GetSize(data);
1252 cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
1253 cell->setPort("\\CLK", RTLIL::State::S0);
1254 cell->setPort("\\ADDR", addr);
1255 cell->setPort("\\DATA", data);
1256
1257 if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
1258 cell->parameters["\\CLK_ENABLE"] = true;
1259 cell->setPort("\\CLK", net_map_at(inst->GetClock()));
1260 }
1261 }
1262 continue;
1263 }
1264
1265 if (!mode_gates) {
1266 if (import_netlist_instance_cells(inst, inst_name))
1267 continue;
1268 if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
1269 log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
1270 } else {
1271 if (import_netlist_instance_gates(inst, inst_name))
1272 continue;
1273 }
1274
1275 if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
1276 sva_asserts.insert(inst);
1277
1278 if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_RESTRICT)
1279 sva_assumes.insert(inst);
1280
1281 if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
1282 sva_covers.insert(inst);
1283
1284 if (inst->Type() == PRIM_SVA_TRIGGERED)
1285 sva_triggers.insert(inst);
1286
1287 if (inst->Type() == OPER_SVA_STABLE)
1288 {
1289 VerificClocking clocking(this, inst->GetInput2Bit(0));
1290 log_assert(clocking.disable_sig == State::S0);
1291 log_assert(clocking.body_net == nullptr);
1292
1293 log_assert(inst->Input1Size() == inst->OutputSize());
1294
1295 SigSpec sig_d, sig_q, sig_o;
1296 sig_q = module->addWire(new_verific_id(inst), inst->Input1Size());
1297
1298 for (int i = int(inst->Input1Size())-1; i >= 0; i--){
1299 sig_d.append(net_map_at(inst->GetInput1Bit(i)));
1300 sig_o.append(net_map_at(inst->GetOutputBit(i)));
1301 }
1302
1303 if (verific_verbose) {
1304 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1305 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1306 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1307 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1308 }
1309
1310 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1311 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1312
1313 if (!mode_keep)
1314 continue;
1315 }
1316
1317 if (inst->Type() == PRIM_SVA_STABLE)
1318 {
1319 VerificClocking clocking(this, inst->GetInput2());
1320 log_assert(clocking.disable_sig == State::S0);
1321 log_assert(clocking.body_net == nullptr);
1322
1323 SigSpec sig_d = net_map_at(inst->GetInput1());
1324 SigSpec sig_o = net_map_at(inst->GetOutput());
1325 SigSpec sig_q = module->addWire(new_verific_id(inst));
1326
1327 if (verific_verbose) {
1328 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1329 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1330 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1331 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1332 }
1333
1334 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1335 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1336
1337 if (!mode_keep)
1338 continue;
1339 }
1340
1341 if (inst->Type() == PRIM_SVA_PAST)
1342 {
1343 VerificClocking clocking(this, inst->GetInput2());
1344 log_assert(clocking.disable_sig == State::S0);
1345 log_assert(clocking.body_net == nullptr);
1346
1347 SigBit sig_d = net_map_at(inst->GetInput1());
1348 SigBit sig_q = net_map_at(inst->GetOutput());
1349
1350 if (verific_verbose)
1351 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1352 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1353
1354 past_ffs.insert(clocking.addDff(new_verific_id(inst), sig_d, sig_q));
1355
1356 if (!mode_keep)
1357 continue;
1358 }
1359
1360 if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
1361 {
1362 VerificClocking clocking(this, inst->GetInput2());
1363 log_assert(clocking.disable_sig == State::S0);
1364 log_assert(clocking.body_net == nullptr);
1365
1366 SigBit sig_d = net_map_at(inst->GetInput1());
1367 SigBit sig_o = net_map_at(inst->GetOutput());
1368 SigBit sig_q = module->addWire(new_verific_id(inst));
1369
1370 if (verific_verbose)
1371 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1372 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1373
1374 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1375 module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
1376
1377 if (!mode_keep)
1378 continue;
1379 }
1380
1381 if (!mode_keep && verific_sva_prims.count(inst->Type())) {
1382 if (verific_verbose)
1383 log(" skipping SVA cell in non k-mode\n");
1384 continue;
1385 }
1386
1387 if (inst->Type() == PRIM_HDL_ASSERTION)
1388 {
1389 SigBit cond = net_map_at(inst->GetInput());
1390
1391 if (verific_verbose)
1392 log(" assert condition %s.\n", log_signal(cond));
1393
1394 const char *assume_attr = nullptr; // inst->GetAttValue("assume");
1395
1396 Cell *cell = nullptr;
1397 if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
1398 cell = module->addAssume(new_verific_id(inst), cond, State::S1);
1399 else
1400 cell = module->addAssert(new_verific_id(inst), cond, State::S1);
1401
1402 import_attributes(cell->attributes, inst);
1403 continue;
1404 }
1405
1406 if (inst->IsPrimitive())
1407 {
1408 if (!mode_keep)
1409 log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1410
1411 if (!verific_sva_prims.count(inst->Type()))
1412 log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1413 }
1414
1415 import_verific_cells:
1416 nl_todo.insert(inst->View());
1417
1418 std::string inst_type = inst->View()->Owner()->Name();
1419
1420 if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) {
1421 inst_type = "$verific$" + inst_type;
1422 } else {
1423 if (*inst->View()->Name()) {
1424 inst_type += "(";
1425 inst_type += inst->View()->Name();
1426 inst_type += ")";
1427 }
1428 inst_type = "\\" + inst_type;
1429 }
1430
1431 RTLIL::Cell *cell = module->addCell(inst_name, inst_type);
1432
1433 if (inst->IsPrimitive() && mode_keep)
1434 cell->attributes["\\keep"] = 1;
1435
1436 dict<IdString, vector<SigBit>> cell_port_conns;
1437
1438 if (verific_verbose)
1439 log(" ports in verific db:\n");
1440
1441 FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
1442 if (verific_verbose)
1443 log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
1444 const char *port_name = pr->GetPort()->Name();
1445 int port_offset = 0;
1446 if (pr->GetPort()->Bus()) {
1447 port_name = pr->GetPort()->Bus()->Name();
1448 port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
1449 min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
1450 }
1451 IdString port_name_id = RTLIL::escape_id(port_name);
1452 auto &sigvec = cell_port_conns[port_name_id];
1453 if (GetSize(sigvec) <= port_offset) {
1454 SigSpec zwires = module->addWire(new_verific_id(inst), port_offset+1-GetSize(sigvec));
1455 for (auto bit : zwires)
1456 sigvec.push_back(bit);
1457 }
1458 sigvec[port_offset] = net_map_at(pr->GetNet());
1459 }
1460
1461 if (verific_verbose)
1462 log(" ports in yosys db:\n");
1463
1464 for (auto &it : cell_port_conns) {
1465 if (verific_verbose)
1466 log(" .%s(%s)\n", log_id(it.first), log_signal(it.second));
1467 cell->setPort(it.first, it.second);
1468 }
1469 }
1470
1471 if (!mode_nosva)
1472 {
1473 for (auto inst : sva_asserts) {
1474 if (mode_autocover)
1475 verific_import_sva_cover(this, inst);
1476 verific_import_sva_assert(this, inst);
1477 }
1478
1479 for (auto inst : sva_assumes)
1480 verific_import_sva_assume(this, inst);
1481
1482 for (auto inst : sva_covers)
1483 verific_import_sva_cover(this, inst);
1484
1485 for (auto inst : sva_triggers)
1486 verific_import_sva_trigger(this, inst);
1487
1488 merge_past_ffs(past_ffs);
1489 }
1490
1491 if (!mode_fullinit)
1492 {
1493 pool<SigBit> non_ff_bits;
1494 CellTypes ff_types;
1495
1496 ff_types.setup_internals_ff();
1497 ff_types.setup_stdcells_mem();
1498
1499 for (auto cell : module->cells())
1500 {
1501 if (ff_types.cell_known(cell->type))
1502 continue;
1503
1504 for (auto conn : cell->connections())
1505 {
1506 if (!cell->output(conn.first))
1507 continue;
1508
1509 for (auto bit : conn.second)
1510 if (bit.wire != nullptr)
1511 non_ff_bits.insert(bit);
1512 }
1513 }
1514
1515 for (auto wire : module->wires())
1516 {
1517 if (!wire->attributes.count("\\init"))
1518 continue;
1519
1520 Const &initval = wire->attributes.at("\\init");
1521 for (int i = 0; i < GetSize(initval); i++)
1522 {
1523 if (initval[i] != State::S0 && initval[i] != State::S1)
1524 continue;
1525
1526 if (non_ff_bits.count(SigBit(wire, i)))
1527 initval[i] = State::Sx;
1528 }
1529
1530 if (initval.is_fully_undef())
1531 wire->attributes.erase("\\init");
1532 }
1533 }
1534 }
1535
1536 // ==================================================================
1537
1538 VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
1539 {
1540 module = importer->module;
1541
1542 log_assert(importer != nullptr);
1543 log_assert(net != nullptr);
1544
1545 Instance *inst = net->Driver();
1546
1547 if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
1548 {
1549 net = inst->GetInput1();
1550 body_net = inst->GetInput2();
1551
1552 inst = net->Driver();
1553
1554 Instance *body_inst = body_net->Driver();
1555 if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) {
1556 disable_net = body_inst->GetInput1();
1557 disable_sig = importer->net_map_at(disable_net);
1558 body_net = body_inst->GetInput2();
1559 }
1560 }
1561 else
1562 {
1563 if (sva_at_only)
1564 return;
1565 }
1566
1567 // Use while() instead of if() to work around VIPER #13453
1568 while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
1569 {
1570 net = inst->GetInput();
1571 inst = net->Driver();;
1572 }
1573
1574 if (inst != nullptr && inst->Type() == PRIM_INV)
1575 {
1576 net = inst->GetInput();
1577 inst = net->Driver();;
1578 posedge = false;
1579 }
1580
1581 // Detect clock-enable circuit
1582 do {
1583 if (inst == nullptr || inst->Type() != PRIM_AND)
1584 break;
1585
1586 Net *net_dlatch = inst->GetInput1();
1587 Instance *inst_dlatch = net_dlatch->Driver();
1588
1589 if (inst_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS)
1590 break;
1591
1592 if (!inst_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd())
1593 break;
1594
1595 Net *net_enable = inst_dlatch->GetInput();
1596 Net *net_not_clock = inst_dlatch->GetControl();
1597
1598 if (net_enable == nullptr || net_not_clock == nullptr)
1599 break;
1600
1601 Instance *inst_not_clock = net_not_clock->Driver();
1602
1603 if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV)
1604 break;
1605
1606 Net *net_clock1 = inst_not_clock->GetInput();
1607 Net *net_clock2 = inst->GetInput2();
1608
1609 if (net_clock1 == nullptr || net_clock1 != net_clock2)
1610 break;
1611
1612 enable_net = net_enable;
1613 enable_sig = importer->net_map_at(enable_net);
1614
1615 net = net_clock1;
1616 inst = net->Driver();;
1617 } while (0);
1618
1619 // Detect condition expression
1620 do {
1621 if (body_net == nullptr)
1622 break;
1623
1624 Instance *inst_mux = body_net->Driver();
1625
1626 if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
1627 break;
1628
1629 if (!inst_mux->GetInput1()->IsPwr())
1630 break;
1631
1632 Net *sva_net = inst_mux->GetInput2();
1633 if (!verific_is_sva_net(importer, sva_net))
1634 break;
1635
1636 body_net = sva_net;
1637 cond_net = inst_mux->GetControl();
1638 } while (0);
1639
1640 clock_net = net;
1641 clock_sig = importer->net_map_at(clock_net);
1642
1643 const char *gclk_attr = clock_net->GetAttValue("gclk");
1644 if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'")))
1645 gclk = true;
1646 }
1647
1648 Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
1649 {
1650 log_assert(GetSize(sig_d) == GetSize(sig_q));
1651
1652 if (GetSize(init_value) != 0) {
1653 log_assert(GetSize(sig_q) == GetSize(init_value));
1654 if (sig_q.is_wire()) {
1655 sig_q.as_wire()->attributes["\\init"] = init_value;
1656 } else {
1657 Wire *w = module->addWire(NEW_ID, GetSize(sig_q));
1658 w->attributes["\\init"] = init_value;
1659 module->connect(sig_q, w);
1660 sig_q = w;
1661 }
1662 }
1663
1664 if (enable_sig != State::S1)
1665 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1666
1667 if (disable_sig != State::S0) {
1668 log_assert(gclk == false);
1669 log_assert(GetSize(sig_q) == GetSize(init_value));
1670 return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
1671 }
1672
1673 if (gclk)
1674 return module->addFf(name, sig_d, sig_q);
1675
1676 return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
1677 }
1678
1679 Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
1680 {
1681 log_assert(gclk == false);
1682 log_assert(disable_sig == State::S0);
1683
1684 if (enable_sig != State::S1)
1685 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1686
1687 return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge);
1688 }
1689
1690 Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
1691 {
1692 log_assert(gclk == false);
1693 log_assert(disable_sig == State::S0);
1694
1695 if (enable_sig != State::S1)
1696 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1697
1698 return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
1699 }
1700
1701 // ==================================================================
1702
1703 struct VerificExtNets
1704 {
1705 int portname_cnt = 0;
1706
1707 // a map from Net to the same Net one level up in the design hierarchy
1708 std::map<Net*, Net*> net_level_up_drive_up;
1709 std::map<Net*, Net*> net_level_up_drive_down;
1710
1711 Net *route_up(Net *net, bool drive_up, Net *final_net = nullptr)
1712 {
1713 auto &net_level_up = drive_up ? net_level_up_drive_up : net_level_up_drive_down;
1714
1715 if (net_level_up.count(net) == 0)
1716 {
1717 Netlist *nl = net->Owner();
1718
1719 // Simply return if Netlist is not unique
1720 log_assert(nl->NumOfRefs() == 1);
1721
1722 Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
1723 Netlist *up_nl = up_inst->Owner();
1724
1725 // create new Port
1726 string name = stringf("___extnets_%d", portname_cnt++);
1727 Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN);
1728 nl->Add(new_port);
1729 net->Connect(new_port);
1730
1731 // create new Net in up Netlist
1732 Net *new_net = final_net;
1733 if (new_net == nullptr || new_net->Owner() != up_nl) {
1734 new_net = new Net(name.c_str());
1735 up_nl->Add(new_net);
1736 }
1737 up_inst->Connect(new_port, new_net);
1738
1739 net_level_up[net] = new_net;
1740 }
1741
1742 return net_level_up.at(net);
1743 }
1744
1745 Net *route_up(Net *net, bool drive_up, Netlist *dest, Net *final_net = nullptr)
1746 {
1747 while (net->Owner() != dest)
1748 net = route_up(net, drive_up, final_net);
1749 if (final_net != nullptr)
1750 log_assert(net == final_net);
1751 return net;
1752 }
1753
1754 Netlist *find_common_ancestor(Netlist *A, Netlist *B)
1755 {
1756 std::set<Netlist*> ancestors_of_A;
1757
1758 Netlist *cursor = A;
1759 while (1) {
1760 ancestors_of_A.insert(cursor);
1761 if (cursor->NumOfRefs() != 1)
1762 break;
1763 cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
1764 }
1765
1766 cursor = B;
1767 while (1) {
1768 if (ancestors_of_A.count(cursor))
1769 return cursor;
1770 if (cursor->NumOfRefs() != 1)
1771 break;
1772 cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
1773 }
1774
1775 log_error("No common ancestor found between %s and %s.\n", get_full_netlist_name(A).c_str(), get_full_netlist_name(B).c_str());
1776 }
1777
1778 void run(Netlist *nl)
1779 {
1780 MapIter mi, mi2;
1781 Instance *inst;
1782 PortRef *pr;
1783
1784 vector<tuple<Instance*, Port*, Net*>> todo_connect;
1785
1786 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1787 run(inst->View());
1788
1789 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1790 FOREACH_PORTREF_OF_INST(inst, mi2, pr)
1791 {
1792 Port *port = pr->GetPort();
1793 Net *net = pr->GetNet();
1794
1795 if (!net->IsExternalTo(nl))
1796 continue;
1797
1798 if (verific_verbose)
1799 log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
1800
1801 Netlist *ext_nl = net->Owner();
1802
1803 if (verific_verbose)
1804 log(" external net owner: %s\n", get_full_netlist_name(ext_nl).c_str());
1805
1806 Netlist *ca_nl = find_common_ancestor(nl, ext_nl);
1807
1808 if (verific_verbose)
1809 log(" common ancestor: %s\n", get_full_netlist_name(ca_nl).c_str());
1810
1811 Net *ca_net = route_up(net, !port->IsOutput(), ca_nl);
1812 Net *new_net = ca_net;
1813
1814 if (ca_nl != nl)
1815 {
1816 if (verific_verbose)
1817 log(" net in common ancestor: %s\n", ca_net->Name());
1818
1819 string name = stringf("___extnets_%d", portname_cnt++);
1820 new_net = new Net(name.c_str());
1821 nl->Add(new_net);
1822
1823 Net *n YS_ATTRIBUTE(unused) = route_up(new_net, port->IsOutput(), ca_nl, ca_net);
1824 log_assert(n == ca_net);
1825 }
1826
1827 if (verific_verbose)
1828 log(" new local net: %s\n", new_net->Name());
1829
1830 log_assert(!new_net->IsExternalTo(nl));
1831 todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, new_net));
1832 }
1833
1834 for (auto it : todo_connect) {
1835 get<0>(it)->Disconnect(get<1>(it));
1836 get<0>(it)->Connect(get<1>(it), get<2>(it));
1837 }
1838 }
1839 };
1840
1841 void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
1842 {
1843 verific_sva_fsm_limit = 16;
1844
1845 std::set<Netlist*> nl_todo, nl_done;
1846
1847 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
1848 VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
1849 Array *netlists = NULL;
1850 Array veri_libs, vhdl_libs;
1851 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
1852 if (veri_lib) veri_libs.InsertLast(veri_lib);
1853
1854 Map verific_params(STRING_HASH);
1855 for (const auto &i : parameters)
1856 verific_params.Insert(i.first.c_str(), i.second.c_str());
1857
1858 if (top.empty()) {
1859 netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
1860 }
1861 else {
1862 Array veri_modules, vhdl_units;
1863
1864 if (veri_lib) {
1865 VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
1866 if (veri_module) {
1867 veri_modules.InsertLast(veri_module);
1868 }
1869
1870 // Also elaborate all root modules since they may contain bind statements
1871 MapIter mi;
1872 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
1873 if (!veri_module->IsRootModule()) continue;
1874 veri_modules.InsertLast(veri_module);
1875 }
1876 }
1877
1878 if (vhdl_lib) {
1879 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
1880 if (vhdl_unit)
1881 vhdl_units.InsertLast(vhdl_unit);
1882 }
1883
1884 netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
1885 }
1886
1887 Netlist *nl;
1888 int i;
1889
1890 FOREACH_ARRAY_ITEM(netlists, i, nl) {
1891 if (top.empty() && nl->CellBaseName() != top)
1892 continue;
1893 nl->AddAtt(new Att(" \\top", NULL));
1894 nl_todo.insert(nl);
1895 }
1896
1897 delete netlists;
1898
1899 if (!verific_error_msg.empty())
1900 log_error("%s\n", verific_error_msg.c_str());
1901
1902 for (auto nl : nl_todo)
1903 nl->ChangePortBusStructures(1 /* hierarchical */);
1904
1905 VerificExtNets worker;
1906 for (auto nl : nl_todo)
1907 worker.run(nl);
1908
1909 while (!nl_todo.empty()) {
1910 Netlist *nl = *nl_todo.begin();
1911 if (nl_done.count(nl) == 0) {
1912 VerificImporter importer(false, false, false, false, false, false, false);
1913 importer.import_netlist(design, nl, nl_todo, nl->Owner()->Name() == top);
1914 }
1915 nl_todo.erase(nl);
1916 nl_done.insert(nl);
1917 }
1918
1919 veri_file::Reset();
1920 vhdl_file::Reset();
1921 Libset::Reset();
1922 verific_incdirs.clear();
1923 verific_libdirs.clear();
1924 verific_import_pending = false;
1925
1926 if (!verific_error_msg.empty())
1927 log_error("%s\n", verific_error_msg.c_str());
1928 }
1929
1930 YOSYS_NAMESPACE_END
1931 #endif /* YOSYS_ENABLE_VERIFIC */
1932
1933 PRIVATE_NAMESPACE_BEGIN
1934
1935 #ifdef YOSYS_ENABLE_VERIFIC
1936 bool check_noverific_env()
1937 {
1938 const char *e = getenv("YOSYS_NOVERIFIC");
1939 if (e == nullptr)
1940 return false;
1941 if (atoi(e) == 0)
1942 return false;
1943 return true;
1944 }
1945 #endif
1946
1947 struct VerificPass : public Pass {
1948 VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
1949 void help() YS_OVERRIDE
1950 {
1951 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1952 log("\n");
1953 log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
1954 log("\n");
1955 log("Load the specified Verilog/SystemVerilog files into Verific.\n");
1956 log("\n");
1957 log("All files specified in one call to this command are one compilation unit.\n");
1958 log("Files passed to different calls to this command are treated as belonging to\n");
1959 log("different compilation units.\n");
1960 log("\n");
1961 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
1962 log("the language version (and before file names) to set additional verilog defines.\n");
1963 log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
1964 log("\n");
1965 log("\n");
1966 log(" verific -formal <verilog-file>..\n");
1967 log("\n");
1968 log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
1969 log("\n");
1970 log("\n");
1971 log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
1972 log("\n");
1973 log("Load the specified VHDL files into Verific.\n");
1974 log("\n");
1975 log("\n");
1976 log(" verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>\n");
1977 log("\n");
1978 log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
1979 log("(default library when -work is not present: \"work\")\n");
1980 log("\n");
1981 log("\n");
1982 log(" verific [-L <libname>] {-sv|-vhdl|...} <hdl-file>\n");
1983 log("\n");
1984 log("Look up external definitions in the specified library.\n");
1985 log("(-L may be used more than once)\n");
1986 log("\n");
1987 log("\n");
1988 log(" verific -vlog-incdir <directory>..\n");
1989 log("\n");
1990 log("Add Verilog include directories.\n");
1991 log("\n");
1992 log("\n");
1993 log(" verific -vlog-libdir <directory>..\n");
1994 log("\n");
1995 log("Add Verilog library directories. Verific will search in this directories to\n");
1996 log("find undefined modules.\n");
1997 log("\n");
1998 log("\n");
1999 log(" verific -vlog-define <macro>[=<value>]..\n");
2000 log("\n");
2001 log("Add Verilog defines.\n");
2002 log("\n");
2003 log("\n");
2004 log(" verific -vlog-undef <macro>..\n");
2005 log("\n");
2006 log("Remove Verilog defines previously set with -vlog-define.\n");
2007 log("\n");
2008 log("\n");
2009 log(" verific -set-error <msg_id>..\n");
2010 log(" verific -set-warning <msg_id>..\n");
2011 log(" verific -set-info <msg_id>..\n");
2012 log(" verific -set-ignore <msg_id>..\n");
2013 log("\n");
2014 log("Set message severity. <msg_id> is the string in square brackets when a message\n");
2015 log("is printed, such as VERI-1209.\n");
2016 log("\n");
2017 log("\n");
2018 log(" verific -import [options] <top-module>..\n");
2019 log("\n");
2020 log("Elaborate the design for the specified top modules, import to Yosys and\n");
2021 log("reset the internal state of Verific.\n");
2022 log("\n");
2023 log("Import options:\n");
2024 log("\n");
2025 log(" -all\n");
2026 log(" Elaborate all modules, not just the hierarchy below the given top\n");
2027 log(" modules. With this option the list of modules to import is optional.\n");
2028 log("\n");
2029 log(" -gates\n");
2030 log(" Create a gate-level netlist.\n");
2031 log("\n");
2032 log(" -flatten\n");
2033 log(" Flatten the design in Verific before importing.\n");
2034 log("\n");
2035 log(" -extnets\n");
2036 log(" Resolve references to external nets by adding module ports as needed.\n");
2037 log("\n");
2038 log(" -autocover\n");
2039 log(" Generate automatic cover statements for all asserts\n");
2040 log("\n");
2041 log(" -fullinit\n");
2042 log(" Keep all register initializations, even those for non-FF registers.\n");
2043 log("\n");
2044 log(" -chparam name value \n");
2045 log(" Elaborate the specified top modules (all modules when -all given) using\n");
2046 log(" this parameter value. Modules on which this parameter does not exist will\n");
2047 log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
2048 log(" can be specified multiple times to override multiple parameters.\n");
2049 log(" String values must be passed in double quotes (\").\n");
2050 log("\n");
2051 log(" -v, -vv\n");
2052 log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
2053 log("\n");
2054 log("The following additional import options are useful for debugging the Verific\n");
2055 log("bindings (for Yosys and/or Verific developers):\n");
2056 log("\n");
2057 log(" -k\n");
2058 log(" Keep going after an unsupported verific primitive is found. The\n");
2059 log(" unsupported primitive is added as blockbox module to the design.\n");
2060 log(" This will also add all SVA related cells to the design parallel to\n");
2061 log(" the checker logic inferred by it.\n");
2062 log("\n");
2063 log(" -V\n");
2064 log(" Import Verific netlist as-is without translating to Yosys cell types. \n");
2065 log("\n");
2066 log(" -nosva\n");
2067 log(" Ignore SVA properties, do not infer checker logic.\n");
2068 log("\n");
2069 log(" -L <int>\n");
2070 log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
2071 log("\n");
2072 log(" -n\n");
2073 log(" Keep all Verific names on instances and nets. By default only\n");
2074 log(" user-declared names are preserved.\n");
2075 log("\n");
2076 log(" -d <dump_file>\n");
2077 log(" Dump the Verific netlist as a verilog file.\n");
2078 log("\n");
2079 log("\n");
2080 log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
2081 log("https://www.symbioticeda.com/seda-suite\n");
2082 log("\n");
2083 log("Contact office@symbioticeda.com for free evaluation\n");
2084 log("binaries of Symbiotic EDA Suite.\n");
2085 log("\n");
2086 }
2087 #ifdef YOSYS_ENABLE_VERIFIC
2088 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2089 {
2090 static bool set_verific_global_flags = true;
2091
2092 if (check_noverific_env())
2093 log_cmd_error("This version of Yosys is built without Verific support.\n"
2094 "\n"
2095 "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
2096 "https://www.symbioticeda.com/seda-suite\n"
2097 "\n"
2098 "Contact office@symbioticeda.com for free evaluation\n"
2099 "binaries of Symbiotic EDA Suite.\n");
2100
2101 log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
2102
2103 if (set_verific_global_flags)
2104 {
2105 Message::SetConsoleOutput(0);
2106 Message::RegisterCallBackMsg(msg_func);
2107
2108 RuntimeFlags::SetVar("db_preserve_user_nets", 1);
2109 RuntimeFlags::SetVar("db_allow_external_nets", 1);
2110 RuntimeFlags::SetVar("db_infer_wide_operators", 1);
2111
2112 RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
2113 RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
2114
2115 RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
2116 RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
2117
2118 RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
2119 RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
2120
2121 // Workaround for VIPER #13851
2122 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
2123
2124 // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
2125 Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
2126
2127 // https://github.com/YosysHQ/yosys/issues/1055
2128 RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
2129
2130 #ifndef DB_PRESERVE_INITIAL_VALUE
2131 # warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
2132 #endif
2133
2134 set_verific_global_flags = false;
2135 }
2136
2137 verific_verbose = 0;
2138 verific_sva_fsm_limit = 16;
2139
2140 const char *release_str = Message::ReleaseString();
2141 time_t release_time = Message::ReleaseDate();
2142 char *release_tmstr = ctime(&release_time);
2143
2144 if (release_str == nullptr)
2145 release_str = "(no release string)";
2146
2147 for (char *p = release_tmstr; *p; p++)
2148 if (*p == '\n') *p = 0;
2149
2150 log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
2151
2152 int argidx = 1;
2153 std::string work = "work";
2154
2155 if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
2156 args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
2157 {
2158 msg_type_t new_type;
2159
2160 if (args[argidx] == "-set-error")
2161 new_type = VERIFIC_ERROR;
2162 else if (args[argidx] == "-set-warning")
2163 new_type = VERIFIC_WARNING;
2164 else if (args[argidx] == "-set-info")
2165 new_type = VERIFIC_INFO;
2166 else if (args[argidx] == "-set-ignore")
2167 new_type = VERIFIC_IGNORE;
2168 else
2169 log_abort();
2170
2171 for (argidx++; argidx < GetSize(args); argidx++)
2172 Message::SetMessageType(args[argidx].c_str(), new_type);
2173
2174 goto check_error;
2175 }
2176
2177 if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
2178 for (argidx++; argidx < GetSize(args); argidx++)
2179 verific_incdirs.push_back(args[argidx]);
2180 goto check_error;
2181 }
2182
2183 if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
2184 for (argidx++; argidx < GetSize(args); argidx++)
2185 verific_libdirs.push_back(args[argidx]);
2186 goto check_error;
2187 }
2188
2189 if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
2190 for (argidx++; argidx < GetSize(args); argidx++) {
2191 string name = args[argidx];
2192 size_t equal = name.find('=');
2193 if (equal != std::string::npos) {
2194 string value = name.substr(equal+1);
2195 name = name.substr(0, equal);
2196 veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
2197 } else {
2198 veri_file::DefineCmdLineMacro(name.c_str());
2199 }
2200 }
2201 goto check_error;
2202 }
2203
2204 if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
2205 for (argidx++; argidx < GetSize(args); argidx++) {
2206 string name = args[argidx];
2207 veri_file::UndefineMacro(name.c_str());
2208 }
2209 goto check_error;
2210 }
2211
2212 veri_file::RemoveAllLOptions();
2213 for (; argidx < GetSize(args); argidx++)
2214 {
2215 if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
2216 work = args[++argidx];
2217 continue;
2218 }
2219 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2220 veri_file::AddLOption(args[++argidx].c_str());
2221 continue;
2222 }
2223 break;
2224 }
2225
2226 if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
2227 args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
2228 {
2229 Array file_names;
2230 unsigned verilog_mode;
2231
2232 if (args[argidx] == "-vlog95")
2233 verilog_mode = veri_file::VERILOG_95;
2234 else if (args[argidx] == "-vlog2k")
2235 verilog_mode = veri_file::VERILOG_2K;
2236 else if (args[argidx] == "-sv2005")
2237 verilog_mode = veri_file::SYSTEM_VERILOG_2005;
2238 else if (args[argidx] == "-sv2009")
2239 verilog_mode = veri_file::SYSTEM_VERILOG_2009;
2240 else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
2241 verilog_mode = veri_file::SYSTEM_VERILOG;
2242 else
2243 log_abort();
2244
2245 veri_file::DefineMacro("VERIFIC");
2246 veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
2247
2248 for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].compare(0, 2, "-D") == 0; argidx++) {
2249 std::string name = args[argidx].substr(2);
2250 if (args[argidx] == "-D") {
2251 if (++argidx >= GetSize(args))
2252 break;
2253 name = args[argidx];
2254 }
2255 size_t equal = name.find('=');
2256 if (equal != std::string::npos) {
2257 string value = name.substr(equal+1);
2258 name = name.substr(0, equal);
2259 veri_file::DefineMacro(name.c_str(), value.c_str());
2260 } else {
2261 veri_file::DefineMacro(name.c_str());
2262 }
2263 }
2264
2265 for (auto &dir : verific_incdirs)
2266 veri_file::AddIncludeDir(dir.c_str());
2267 for (auto &dir : verific_libdirs)
2268 veri_file::AddYDir(dir.c_str());
2269
2270 while (argidx < GetSize(args))
2271 file_names.Insert(args[argidx++].c_str());
2272
2273 if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
2274 log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
2275
2276 verific_import_pending = true;
2277 goto check_error;
2278 }
2279
2280 if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
2281 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
2282 for (argidx++; argidx < GetSize(args); argidx++)
2283 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
2284 log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
2285 verific_import_pending = true;
2286 goto check_error;
2287 }
2288
2289 if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
2290 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2291 for (argidx++; argidx < GetSize(args); argidx++)
2292 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
2293 log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
2294 verific_import_pending = true;
2295 goto check_error;
2296 }
2297
2298 if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
2299 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2300 for (argidx++; argidx < GetSize(args); argidx++)
2301 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
2302 log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
2303 verific_import_pending = true;
2304 goto check_error;
2305 }
2306
2307 if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
2308 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
2309 for (argidx++; argidx < GetSize(args); argidx++)
2310 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
2311 log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
2312 verific_import_pending = true;
2313 goto check_error;
2314 }
2315
2316 if (GetSize(args) > argidx && args[argidx] == "-import")
2317 {
2318 std::set<Netlist*> nl_todo, nl_done;
2319 bool mode_all = false, mode_gates = false, mode_keep = false;
2320 bool mode_nosva = false, mode_names = false, mode_verific = false;
2321 bool mode_autocover = false, mode_fullinit = false;
2322 bool flatten = false, extnets = false;
2323 string dumpfile;
2324 Map parameters(STRING_HASH);
2325
2326 for (argidx++; argidx < GetSize(args); argidx++) {
2327 if (args[argidx] == "-all") {
2328 mode_all = true;
2329 continue;
2330 }
2331 if (args[argidx] == "-gates") {
2332 mode_gates = true;
2333 continue;
2334 }
2335 if (args[argidx] == "-flatten") {
2336 flatten = true;
2337 continue;
2338 }
2339 if (args[argidx] == "-extnets") {
2340 extnets = true;
2341 continue;
2342 }
2343 if (args[argidx] == "-k") {
2344 mode_keep = true;
2345 continue;
2346 }
2347 if (args[argidx] == "-nosva") {
2348 mode_nosva = true;
2349 continue;
2350 }
2351 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2352 verific_sva_fsm_limit = atoi(args[++argidx].c_str());
2353 continue;
2354 }
2355 if (args[argidx] == "-n") {
2356 mode_names = true;
2357 continue;
2358 }
2359 if (args[argidx] == "-autocover") {
2360 mode_autocover = true;
2361 continue;
2362 }
2363 if (args[argidx] == "-fullinit") {
2364 mode_fullinit = true;
2365 continue;
2366 }
2367 if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
2368 const std::string &key = args[++argidx];
2369 const std::string &value = args[++argidx];
2370 unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
2371 1 /* force_overwrite */);
2372 if (!new_insertion)
2373 log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
2374 continue;
2375 }
2376 if (args[argidx] == "-V") {
2377 mode_verific = true;
2378 continue;
2379 }
2380 if (args[argidx] == "-v") {
2381 verific_verbose = 1;
2382 continue;
2383 }
2384 if (args[argidx] == "-vv") {
2385 verific_verbose = 2;
2386 continue;
2387 }
2388 if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
2389 dumpfile = args[++argidx];
2390 continue;
2391 }
2392 break;
2393 }
2394
2395 if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
2396 cmd_error(args, argidx, "unknown option");
2397
2398 std::set<std::string> top_mod_names;
2399
2400 if (mode_all)
2401 {
2402 log("Running hier_tree::ElaborateAll().\n");
2403
2404 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2405 VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2406
2407 Array veri_libs, vhdl_libs;
2408 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
2409 if (veri_lib) veri_libs.InsertLast(veri_lib);
2410
2411 Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
2412 Netlist *nl;
2413 int i;
2414
2415 FOREACH_ARRAY_ITEM(netlists, i, nl)
2416 nl_todo.insert(nl);
2417 delete netlists;
2418 }
2419 else
2420 {
2421 if (argidx == GetSize(args))
2422 cmd_error(args, argidx, "No top module specified.\n");
2423
2424 Array veri_modules, vhdl_units;
2425 for (; argidx < GetSize(args); argidx++)
2426 {
2427 const char *name = args[argidx].c_str();
2428 top_mod_names.insert(name);
2429 VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2430
2431 if (veri_lib) {
2432 VeriModule *veri_module = veri_lib->GetModule(name, 1);
2433 if (veri_module) {
2434 log("Adding Verilog module '%s' to elaboration queue.\n", name);
2435 veri_modules.InsertLast(veri_module);
2436 continue;
2437 }
2438
2439 // Also elaborate all root modules since they may contain bind statements
2440 MapIter mi;
2441 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
2442 if (!veri_module->IsRootModule()) continue;
2443 veri_modules.InsertLast(veri_module);
2444 }
2445 }
2446
2447 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2448 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
2449 if (vhdl_unit) {
2450 log("Adding VHDL unit '%s' to elaboration queue.\n", name);
2451 vhdl_units.InsertLast(vhdl_unit);
2452 continue;
2453 }
2454
2455 log_error("Can't find module/unit '%s'.\n", name);
2456 }
2457
2458 log("Running hier_tree::Elaborate().\n");
2459 Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
2460 Netlist *nl;
2461 int i;
2462
2463 FOREACH_ARRAY_ITEM(netlists, i, nl) {
2464 nl->AddAtt(new Att(" \\top", NULL));
2465 nl_todo.insert(nl);
2466 }
2467 delete netlists;
2468 }
2469
2470 if (!verific_error_msg.empty())
2471 goto check_error;
2472
2473 if (flatten) {
2474 for (auto nl : nl_todo)
2475 nl->Flatten();
2476 }
2477
2478 if (extnets) {
2479 VerificExtNets worker;
2480 for (auto nl : nl_todo)
2481 worker.run(nl);
2482 }
2483
2484 for (auto nl : nl_todo)
2485 nl->ChangePortBusStructures(1 /* hierarchical */);
2486
2487 if (!dumpfile.empty()) {
2488 VeriWrite veri_writer;
2489 veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign());
2490 }
2491
2492 while (!nl_todo.empty()) {
2493 Netlist *nl = *nl_todo.begin();
2494 if (nl_done.count(nl) == 0) {
2495 VerificImporter importer(mode_gates, mode_keep, mode_nosva,
2496 mode_names, mode_verific, mode_autocover, mode_fullinit);
2497 importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->Owner()->Name()));
2498 }
2499 nl_todo.erase(nl);
2500 nl_done.insert(nl);
2501 }
2502
2503 veri_file::Reset();
2504 vhdl_file::Reset();
2505 Libset::Reset();
2506 verific_incdirs.clear();
2507 verific_libdirs.clear();
2508 verific_import_pending = false;
2509 goto check_error;
2510 }
2511
2512 cmd_error(args, argidx, "Missing or unsupported mode parameter.\n");
2513
2514 check_error:
2515 if (!verific_error_msg.empty())
2516 log_error("%s\n", verific_error_msg.c_str());
2517
2518 }
2519 #else /* YOSYS_ENABLE_VERIFIC */
2520 void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
2521 log_cmd_error("This version of Yosys is built without Verific support.\n"
2522 "\n"
2523 "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
2524 "https://www.symbioticeda.com/seda-suite\n"
2525 "\n"
2526 "Contact office@symbioticeda.com for free evaluation\n"
2527 "binaries of Symbiotic EDA Suite.\n");
2528 }
2529 #endif
2530 } VerificPass;
2531
2532 struct ReadPass : public Pass {
2533 ReadPass() : Pass("read", "load HDL designs") { }
2534 void help() YS_OVERRIDE
2535 {
2536 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2537 log("\n");
2538 log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
2539 log("\n");
2540 log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
2541 log("is only available via Verific.)\n");
2542 log("\n");
2543 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2544 log("the language version (and before file names) to set additional verilog defines.\n");
2545 log("\n");
2546 log("\n");
2547 log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2548 log("\n");
2549 log("Load the specified VHDL files. (Requires Verific.)\n");
2550 log("\n");
2551 log("\n");
2552 log(" read -define <macro>[=<value>]..\n");
2553 log("\n");
2554 log("Set global Verilog/SystemVerilog defines.\n");
2555 log("\n");
2556 log("\n");
2557 log(" read -undef <macro>..\n");
2558 log("\n");
2559 log("Unset global Verilog/SystemVerilog defines.\n");
2560 log("\n");
2561 log("\n");
2562 log(" read -incdir <directory>\n");
2563 log("\n");
2564 log("Add directory to global Verilog/SystemVerilog include directories.\n");
2565 log("\n");
2566 log("\n");
2567 log(" read -verific\n");
2568 log(" read -noverific\n");
2569 log("\n");
2570 log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
2571 log("with -verific will result in an error on Yosys binaries that are built without\n");
2572 log("Verific support. The default is to use Verific if it is available.\n");
2573 log("\n");
2574 }
2575 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2576 {
2577 #ifdef YOSYS_ENABLE_VERIFIC
2578 static bool verific_available = !check_noverific_env();
2579 #else
2580 static bool verific_available = false;
2581 #endif
2582 static bool use_verific = verific_available;
2583
2584 if (args.size() < 2 || args[1][0] != '-')
2585 cmd_error(args, 1, "Missing mode parameter.\n");
2586
2587 if (args[1] == "-verific" || args[1] == "-noverific") {
2588 if (args.size() != 2)
2589 cmd_error(args, 1, "Additional arguments to -verific/-noverific.\n");
2590 if (args[1] == "-verific") {
2591 if (!verific_available)
2592 cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
2593 use_verific = true;
2594 } else {
2595 use_verific = false;
2596 }
2597 return;
2598 }
2599
2600 if (args.size() < 3)
2601 cmd_error(args, 3, "Missing file name parameter.\n");
2602
2603 if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
2604 if (use_verific) {
2605 args[0] = "verific";
2606 } else {
2607 args[0] = "read_verilog";
2608 args[1] = "-defer";
2609 }
2610 Pass::call(design, args);
2611 return;
2612 }
2613
2614 if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
2615 if (use_verific) {
2616 args[0] = "verific";
2617 } else {
2618 args[0] = "read_verilog";
2619 if (args[1] == "-formal")
2620 args.insert(args.begin()+1, std::string());
2621 args[1] = "-sv";
2622 args.insert(args.begin()+1, "-defer");
2623 }
2624 Pass::call(design, args);
2625 return;
2626 }
2627
2628 if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
2629 if (use_verific) {
2630 args[0] = "verific";
2631 Pass::call(design, args);
2632 } else {
2633 cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
2634 }
2635 return;
2636 }
2637
2638 if (args[1] == "-define") {
2639 if (use_verific) {
2640 args[0] = "verific";
2641 args[1] = "-vlog-define";
2642 Pass::call(design, args);
2643 }
2644 args[0] = "verilog_defines";
2645 args.erase(args.begin()+1, args.begin()+2);
2646 for (int i = 1; i < GetSize(args); i++)
2647 args[i] = "-D" + args[i];
2648 Pass::call(design, args);
2649 return;
2650 }
2651
2652 if (args[1] == "-undef") {
2653 if (use_verific) {
2654 args[0] = "verific";
2655 args[1] = "-vlog-undef";
2656 Pass::call(design, args);
2657 }
2658 args[0] = "verilog_defines";
2659 args.erase(args.begin()+1, args.begin()+2);
2660 for (int i = 1; i < GetSize(args); i++)
2661 args[i] = "-U" + args[i];
2662 Pass::call(design, args);
2663 return;
2664 }
2665
2666 if (args[1] == "-incdir") {
2667 if (use_verific) {
2668 args[0] = "verific";
2669 args[1] = "-vlog-incdir";
2670 Pass::call(design, args);
2671 }
2672 args[0] = "verilog_defaults";
2673 args[1] = "-add";
2674 for (int i = 2; i < GetSize(args); i++)
2675 args[i] = "-I" + args[i];
2676 Pass::call(design, args);
2677 return;
2678 }
2679
2680 cmd_error(args, 1, "Missing or unsupported mode parameter.\n");
2681 }
2682 } ReadPass;
2683
2684 PRIVATE_NAMESPACE_END