projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
verific: no help() when no YOSYS_ENABLE_VERIFIC
[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())
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_OR) {
543 cell = module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
544 import_attributes(cell->attributes, inst);
545 return true;
546 }
547
548 if (inst->Type() == OPER_REDUCE_XOR) {
549 cell = module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
550 import_attributes(cell->attributes, inst);
551 return true;
552 }
553
554 if (inst->Type() == OPER_REDUCE_XNOR) {
555 cell = module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
556 import_attributes(cell->attributes, inst);
557 return true;
558 }
559
560 if (inst->Type() == OPER_REDUCE_NOR) {
561 SigSpec t = module->ReduceOr(new_verific_id(inst), IN, SIGNED);
562 cell = module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
563 import_attributes(cell->attributes, inst);
564 return true;
565 }
566
567 if (inst->Type() == OPER_LESSTHAN) {
568 Net *net_cin = inst->GetCin();
569 if (net_cin->IsGnd())
570 cell = module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
571 else if (net_cin->IsPwr())
572 cell = module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
573 else
574 log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
575 import_attributes(cell->attributes, inst);
576 return true;
577 }
578
579 if (inst->Type() == OPER_WIDE_AND) {
580 cell = module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
581 import_attributes(cell->attributes, inst);
582 return true;
583 }
584
585 if (inst->Type() == OPER_WIDE_OR) {
586 cell = module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
587 import_attributes(cell->attributes, inst);
588 return true;
589 }
590
591 if (inst->Type() == OPER_WIDE_XOR) {
592 cell = module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
593 import_attributes(cell->attributes, inst);
594 return true;
595 }
596
597 if (inst->Type() == OPER_WIDE_XNOR) {
598 cell = module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
599 import_attributes(cell->attributes, inst);
600 return true;
601 }
602
603 if (inst->Type() == OPER_WIDE_BUF) {
604 cell = module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
605 import_attributes(cell->attributes, inst);
606 return true;
607 }
608
609 if (inst->Type() == OPER_WIDE_INV) {
610 cell = module->addNot(inst_name, IN, OUT, SIGNED);
611 import_attributes(cell->attributes, inst);
612 return true;
613 }
614
615 if (inst->Type() == OPER_MINUS) {
616 cell = module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
617 import_attributes(cell->attributes, inst);
618 return true;
619 }
620
621 if (inst->Type() == OPER_UMINUS) {
622 cell = module->addNeg(inst_name, IN, OUT, SIGNED);
623 import_attributes(cell->attributes, inst);
624 return true;
625 }
626
627 if (inst->Type() == OPER_EQUAL) {
628 cell = module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
629 import_attributes(cell->attributes, inst);
630 return true;
631 }
632
633 if (inst->Type() == OPER_NEQUAL) {
634 cell = module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
635 import_attributes(cell->attributes, inst);
636 return true;
637 }
638
639 if (inst->Type() == OPER_WIDE_MUX) {
640 cell = module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
641 import_attributes(cell->attributes, inst);
642 return true;
643 }
644
645 if (inst->Type() == OPER_NTO1MUX) {
646 cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
647 import_attributes(cell->attributes, inst);
648 return true;
649 }
650
651 if (inst->Type() == OPER_WIDE_NTO1MUX)
652 {
653 SigSpec data = IN2, out = OUT;
654
655 int wordsize_bits = ceil_log2(GetSize(out));
656 int wordsize = 1 << wordsize_bits;
657
658 SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)};
659
660 SigSpec padded_data;
661 for (int i = 0; i < GetSize(data); i += GetSize(out)) {
662 SigSpec d = data.extract(i, GetSize(out));
663 d.extend_u0(wordsize);
664 padded_data.append(d);
665 }
666
667 cell = module->addShr(inst_name, padded_data, sel, out);
668 import_attributes(cell->attributes, inst);
669 return true;
670 }
671
672 if (inst->Type() == OPER_SELECTOR)
673 {
674 cell = module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
675 import_attributes(cell->attributes, inst);
676 return true;
677 }
678
679 if (inst->Type() == OPER_WIDE_SELECTOR)
680 {
681 SigSpec out = OUT;
682 cell = module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
683 import_attributes(cell->attributes, inst);
684 return true;
685 }
686
687 if (inst->Type() == OPER_WIDE_TRI) {
688 cell = module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
689 import_attributes(cell->attributes, inst);
690 return true;
691 }
692
693 if (inst->Type() == OPER_WIDE_DFFRS)
694 {
695 VerificClocking clocking(this, inst->GetClock());
696 log_assert(clocking.disable_sig == State::S0);
697 log_assert(clocking.body_net == nullptr);
698
699 RTLIL::SigSpec sig_set = operatorInport(inst, "set");
700 RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
701
702 if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
703 cell = clocking.addDff(inst_name, IN, OUT);
704 else
705 cell = clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
706 import_attributes(cell->attributes, inst);
707
708 return true;
709 }
710
711 #undef IN
712 #undef IN1
713 #undef IN2
714 #undef OUT
715 #undef SIGNED
716
717 return false;
718 }
719
720 void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
721 {
722 bool keep_running = true;
723 SigMap sigmap;
724
725 while (keep_running)
726 {
727 keep_running = false;
728
729 dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
730 SigSpec dbits;
731
732 for (auto cell : candidates) {
733 SigBit bit = sigmap(cell->getPort("\\D"));
734 dbits_db[bit].insert(cell);
735 dbits.append(bit);
736 }
737
738 dbits.sort_and_unify();
739
740 for (auto chunk : dbits.chunks())
741 {
742 SigSpec sig_d = chunk;
743
744 if (chunk.wire == nullptr || GetSize(sig_d) == 1)
745 continue;
746
747 SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
748 RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);
749
750 if (verific_verbose)
751 log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
752
753 for (int i = 0; i < GetSize(sig_d); i++)
754 for (auto old_ff : dbits_db[sig_d[i]])
755 {
756 if (verific_verbose)
757 log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i);
758
759 SigBit old_q = old_ff->getPort("\\Q");
760 SigBit new_q = sig_q[i];
761
762 sigmap.add(old_q, new_q);
763 module->connect(old_q, new_q);
764 candidates.erase(old_ff);
765 module->remove(old_ff);
766 keep_running = true;
767 }
768 }
769 }
770 }
771
772 void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
773 {
774 dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
775
776 for (auto cell : candidates)
777 {
778 SigBit clock = cell->getPort("\\CLK");
779 bool clock_pol = cell->getParam("\\CLK_POLARITY").as_bool();
780 database[make_pair(clock, int(clock_pol))].insert(cell);
781 }
782
783 for (auto it : database)
784 merge_past_ffs_clock(it.second, it.first.first, it.first.second);
785 }
786
787 void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo)
788 {
789 std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
790 std::string module_name = netlist_name;
791
792 if (nl->IsOperator()) {
793 module_name = "$verific$" + module_name;
794 } else {
795 if (*nl->Name()) {
796 module_name += "(";
797 module_name += nl->Name();
798 module_name += ")";
799 }
800 module_name = "\\" + module_name;
801 }
802
803 netlist = nl;
804
805 if (design->has(module_name)) {
806 if (!nl->IsOperator() && !is_blackbox(nl))
807 log_cmd_error("Re-definition of module `%s'.\n", netlist_name.c_str());
808 return;
809 }
810
811 module = new RTLIL::Module;
812 module->name = module_name;
813 design->add(module);
814
815 if (is_blackbox(nl)) {
816 log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
817 module->set_bool_attribute("\\blackbox");
818 } else {
819 log("Importing module %s.\n", RTLIL::id2cstr(module->name));
820 }
821
822 SetIter si;
823 MapIter mi, mi2;
824 Port *port;
825 PortBus *portbus;
826 Net *net;
827 NetBus *netbus;
828 Instance *inst;
829 PortRef *pr;
830
831 FOREACH_PORT_OF_NETLIST(nl, mi, port)
832 {
833 if (port->Bus())
834 continue;
835
836 if (verific_verbose)
837 log(" importing port %s.\n", port->Name());
838
839 RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
840 import_attributes(wire->attributes, port);
841
842 wire->port_id = nl->IndexOf(port) + 1;
843
844 if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
845 wire->port_input = true;
846 if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
847 wire->port_output = true;
848
849 if (port->GetNet()) {
850 net = port->GetNet();
851 if (net_map.count(net) == 0)
852 net_map[net] = wire;
853 else if (wire->port_input)
854 module->connect(net_map_at(net), wire);
855 else
856 module->connect(wire, net_map_at(net));
857 }
858 }
859
860 FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
861 {
862 if (verific_verbose)
863 log(" importing portbus %s.\n", portbus->Name());
864
865 RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
866 wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
867 import_attributes(wire->attributes, portbus);
868
869 if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
870 wire->port_input = true;
871 if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
872 wire->port_output = true;
873
874 for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
875 if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
876 net = portbus->ElementAtIndex(i)->GetNet();
877 RTLIL::SigBit bit(wire, i - wire->start_offset);
878 if (net_map.count(net) == 0)
879 net_map[net] = bit;
880 else if (wire->port_input)
881 module->connect(net_map_at(net), bit);
882 else
883 module->connect(bit, net_map_at(net));
884 }
885 if (i == portbus->RightIndex())
886 break;
887 }
888 }
889
890 module->fixup_ports();
891
892 dict<Net*, char, hash_ptr_ops> init_nets;
893 pool<Net*, hash_ptr_ops> anyconst_nets, anyseq_nets;
894 pool<Net*, hash_ptr_ops> allconst_nets, allseq_nets;
895 any_all_nets.clear();
896
897 FOREACH_NET_OF_NETLIST(nl, mi, net)
898 {
899 if (net->IsRamNet())
900 {
901 RTLIL::Memory *memory = new RTLIL::Memory;
902 memory->name = RTLIL::escape_id(net->Name());
903 log_assert(module->count_id(memory->name) == 0);
904 module->memories[memory->name] = memory;
905
906 int number_of_bits = net->Size();
907 int bits_in_word = number_of_bits;
908 FOREACH_PORTREF_OF_NET(net, si, pr) {
909 if (pr->GetInst()->Type() == OPER_READ_PORT) {
910 bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
911 continue;
912 }
913 if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
914 bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
915 continue;
916 }
917 log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
918 net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
919 }
920
921 memory->width = bits_in_word;
922 memory->size = number_of_bits / bits_in_word;
923
924 const char *ascii_initdata = net->GetWideInitialValue();
925 if (ascii_initdata) {
926 while (*ascii_initdata != 0 && *ascii_initdata != '\'')
927 ascii_initdata++;
928 if (*ascii_initdata == '\'')
929 ascii_initdata++;
930 if (*ascii_initdata != 0) {
931 log_assert(*ascii_initdata == 'b');
932 ascii_initdata++;
933 }
934 for (int word_idx = 0; word_idx < memory->size; word_idx++) {
935 Const initval = Const(State::Sx, memory->width);
936 bool initval_valid = false;
937 for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
938 if (*ascii_initdata == 0)
939 break;
940 if (*ascii_initdata == '0' || *ascii_initdata == '1') {
941 initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
942 initval_valid = true;
943 }
944 ascii_initdata++;
945 }
946 if (initval_valid) {
947 RTLIL::Cell *cell = module->addCell(new_verific_id(net), "$meminit");
948 cell->parameters["\\WORDS"] = 1;
949 if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
950 cell->setPort("\\ADDR", word_idx);
951 else
952 cell->setPort("\\ADDR", memory->size - word_idx - 1);
953 cell->setPort("\\DATA", initval);
954 cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str());
955 cell->parameters["\\ABITS"] = 32;
956 cell->parameters["\\WIDTH"] = memory->width;
957 cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1);
958 }
959 }
960 }
961 continue;
962 }
963
964 if (net->GetInitialValue())
965 init_nets[net] = net->GetInitialValue();
966
967 const char *rand_const_attr = net->GetAttValue(" rand_const");
968 const char *rand_attr = net->GetAttValue(" rand");
969
970 const char *anyconst_attr = net->GetAttValue("anyconst");
971 const char *anyseq_attr = net->GetAttValue("anyseq");
972
973 const char *allconst_attr = net->GetAttValue("allconst");
974 const char *allseq_attr = net->GetAttValue("allseq");
975
976 if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) {
977 anyconst_nets.insert(net);
978 any_all_nets.insert(net);
979 }
980 else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) {
981 anyseq_nets.insert(net);
982 any_all_nets.insert(net);
983 }
984 else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) {
985 anyconst_nets.insert(net);
986 any_all_nets.insert(net);
987 }
988 else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) {
989 anyseq_nets.insert(net);
990 any_all_nets.insert(net);
991 }
992 else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) {
993 allconst_nets.insert(net);
994 any_all_nets.insert(net);
995 }
996 else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'"))) {
997 allseq_nets.insert(net);
998 any_all_nets.insert(net);
999 }
1000
1001 if (net_map.count(net)) {
1002 if (verific_verbose)
1003 log(" skipping net %s.\n", net->Name());
1004 continue;
1005 }
1006
1007 if (net->Bus())
1008 continue;
1009
1010 RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : new_verific_id(net));
1011
1012 if (verific_verbose)
1013 log(" importing net %s as %s.\n", net->Name(), log_id(wire_name));
1014
1015 RTLIL::Wire *wire = module->addWire(wire_name);
1016 import_attributes(wire->attributes, net);
1017
1018 net_map[net] = wire;
1019 }
1020
1021 FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
1022 {
1023 bool found_new_net = false;
1024 for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
1025 net = netbus->ElementAtIndex(i);
1026 if (net_map.count(net) == 0)
1027 found_new_net = true;
1028 if (i == netbus->RightIndex())
1029 break;
1030 }
1031
1032 if (found_new_net)
1033 {
1034 RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : new_verific_id(netbus));
1035
1036 if (verific_verbose)
1037 log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
1038
1039 RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
1040 wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
1041 import_attributes(wire->attributes, netbus);
1042
1043 RTLIL::Const initval = Const(State::Sx, GetSize(wire));
1044 bool initval_valid = false;
1045
1046 for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
1047 {
1048 if (netbus->ElementAtIndex(i))
1049 {
1050 int bitidx = i - wire->start_offset;
1051 net = netbus->ElementAtIndex(i);
1052 RTLIL::SigBit bit(wire, bitidx);
1053
1054 if (init_nets.count(net)) {
1055 if (init_nets.at(net) == '0')
1056 initval.bits.at(bitidx) = State::S0;
1057 if (init_nets.at(net) == '1')
1058 initval.bits.at(bitidx) = State::S1;
1059 initval_valid = true;
1060 init_nets.erase(net);
1061 }
1062
1063 if (net_map.count(net) == 0)
1064 net_map[net] = bit;
1065 else
1066 module->connect(bit, net_map_at(net));
1067 }
1068
1069 if (i == netbus->RightIndex())
1070 break;
1071 }
1072
1073 if (initval_valid)
1074 wire->attributes["\\init"] = initval;
1075 }
1076 else
1077 {
1078 if (verific_verbose)
1079 log(" skipping netbus %s.\n", netbus->Name());
1080 }
1081
1082 SigSpec anyconst_sig;
1083 SigSpec anyseq_sig;
1084 SigSpec allconst_sig;
1085 SigSpec allseq_sig;
1086
1087 for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
1088 net = netbus->ElementAtIndex(i);
1089 if (net != nullptr && anyconst_nets.count(net)) {
1090 anyconst_sig.append(net_map_at(net));
1091 anyconst_nets.erase(net);
1092 }
1093 if (net != nullptr && anyseq_nets.count(net)) {
1094 anyseq_sig.append(net_map_at(net));
1095 anyseq_nets.erase(net);
1096 }
1097 if (net != nullptr && allconst_nets.count(net)) {
1098 allconst_sig.append(net_map_at(net));
1099 allconst_nets.erase(net);
1100 }
1101 if (net != nullptr && allseq_nets.count(net)) {
1102 allseq_sig.append(net_map_at(net));
1103 allseq_nets.erase(net);
1104 }
1105 if (i == netbus->LeftIndex())
1106 break;
1107 }
1108
1109 if (GetSize(anyconst_sig))
1110 module->connect(anyconst_sig, module->Anyconst(new_verific_id(netbus), GetSize(anyconst_sig)));
1111
1112 if (GetSize(anyseq_sig))
1113 module->connect(anyseq_sig, module->Anyseq(new_verific_id(netbus), GetSize(anyseq_sig)));
1114
1115 if (GetSize(allconst_sig))
1116 module->connect(allconst_sig, module->Allconst(new_verific_id(netbus), GetSize(allconst_sig)));
1117
1118 if (GetSize(allseq_sig))
1119 module->connect(allseq_sig, module->Allseq(new_verific_id(netbus), GetSize(allseq_sig)));
1120 }
1121
1122 for (auto it : init_nets)
1123 {
1124 Const initval;
1125 SigBit bit = net_map_at(it.first);
1126 log_assert(bit.wire);
1127
1128 if (bit.wire->attributes.count("\\init"))
1129 initval = bit.wire->attributes.at("\\init");
1130
1131 while (GetSize(initval) < GetSize(bit.wire))
1132 initval.bits.push_back(State::Sx);
1133
1134 if (it.second == '0')
1135 initval.bits.at(bit.offset) = State::S0;
1136 if (it.second == '1')
1137 initval.bits.at(bit.offset) = State::S1;
1138
1139 bit.wire->attributes["\\init"] = initval;
1140 }
1141
1142 for (auto net : anyconst_nets)
1143 module->connect(net_map_at(net), module->Anyconst(new_verific_id(net)));
1144
1145 for (auto net : anyseq_nets)
1146 module->connect(net_map_at(net), module->Anyseq(new_verific_id(net)));
1147
1148 pool<Instance*, hash_ptr_ops> sva_asserts;
1149 pool<Instance*, hash_ptr_ops> sva_assumes;
1150 pool<Instance*, hash_ptr_ops> sva_covers;
1151 pool<Instance*, hash_ptr_ops> sva_triggers;
1152
1153 pool<RTLIL::Cell*> past_ffs;
1154
1155 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1156 {
1157 RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : new_verific_id(inst));
1158
1159 if (verific_verbose)
1160 log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
1161
1162 if (mode_verific)
1163 goto import_verific_cells;
1164
1165 if (inst->Type() == PRIM_PWR) {
1166 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
1167 continue;
1168 }
1169
1170 if (inst->Type() == PRIM_GND) {
1171 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
1172 continue;
1173 }
1174
1175 if (inst->Type() == PRIM_BUF) {
1176 auto outnet = inst->GetOutput();
1177 if (!any_all_nets.count(outnet))
1178 module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
1179 continue;
1180 }
1181
1182 if (inst->Type() == PRIM_X) {
1183 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
1184 continue;
1185 }
1186
1187 if (inst->Type() == PRIM_Z) {
1188 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
1189 continue;
1190 }
1191
1192 if (inst->Type() == OPER_READ_PORT)
1193 {
1194 RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
1195 int numchunks = int(inst->OutputSize()) / memory->width;
1196 int chunksbits = ceil_log2(numchunks);
1197
1198 if ((numchunks * memory->width) != int(inst->OutputSize()) || (numchunks & (numchunks - 1)) != 0)
1199 log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
1200
1201 for (int i = 0; i < numchunks; i++)
1202 {
1203 RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
1204 RTLIL::SigSpec data = operatorOutput(inst).extract(i * memory->width, memory->width);
1205
1206 RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
1207 RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memrd");
1208 cell->parameters["\\MEMID"] = memory->name.str();
1209 cell->parameters["\\CLK_ENABLE"] = false;
1210 cell->parameters["\\CLK_POLARITY"] = true;
1211 cell->parameters["\\TRANSPARENT"] = false;
1212 cell->parameters["\\ABITS"] = GetSize(addr);
1213 cell->parameters["\\WIDTH"] = GetSize(data);
1214 cell->setPort("\\CLK", RTLIL::State::Sx);
1215 cell->setPort("\\EN", RTLIL::State::Sx);
1216 cell->setPort("\\ADDR", addr);
1217 cell->setPort("\\DATA", data);
1218 }
1219 continue;
1220 }
1221
1222 if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
1223 {
1224 RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
1225 int numchunks = int(inst->Input2Size()) / memory->width;
1226 int chunksbits = ceil_log2(numchunks);
1227
1228 if ((numchunks * memory->width) != int(inst->Input2Size()) || (numchunks & (numchunks - 1)) != 0)
1229 log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetOutput()->Name());
1230
1231 for (int i = 0; i < numchunks; i++)
1232 {
1233 RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
1234 RTLIL::SigSpec data = operatorInput2(inst).extract(i * memory->width, memory->width);
1235
1236 RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
1237 RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memwr");
1238 cell->parameters["\\MEMID"] = memory->name.str();
1239 cell->parameters["\\CLK_ENABLE"] = false;
1240 cell->parameters["\\CLK_POLARITY"] = true;
1241 cell->parameters["\\PRIORITY"] = 0;
1242 cell->parameters["\\ABITS"] = GetSize(addr);
1243 cell->parameters["\\WIDTH"] = GetSize(data);
1244 cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
1245 cell->setPort("\\CLK", RTLIL::State::S0);
1246 cell->setPort("\\ADDR", addr);
1247 cell->setPort("\\DATA", data);
1248
1249 if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
1250 cell->parameters["\\CLK_ENABLE"] = true;
1251 cell->setPort("\\CLK", net_map_at(inst->GetClock()));
1252 }
1253 }
1254 continue;
1255 }
1256
1257 if (!mode_gates) {
1258 if (import_netlist_instance_cells(inst, inst_name))
1259 continue;
1260 if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
1261 log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
1262 } else {
1263 if (import_netlist_instance_gates(inst, inst_name))
1264 continue;
1265 }
1266
1267 if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
1268 sva_asserts.insert(inst);
1269
1270 if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_RESTRICT)
1271 sva_assumes.insert(inst);
1272
1273 if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
1274 sva_covers.insert(inst);
1275
1276 if (inst->Type() == PRIM_SVA_TRIGGERED)
1277 sva_triggers.insert(inst);
1278
1279 if (inst->Type() == OPER_SVA_STABLE)
1280 {
1281 VerificClocking clocking(this, inst->GetInput2Bit(0));
1282 log_assert(clocking.disable_sig == State::S0);
1283 log_assert(clocking.body_net == nullptr);
1284
1285 log_assert(inst->Input1Size() == inst->OutputSize());
1286
1287 SigSpec sig_d, sig_q, sig_o;
1288 sig_q = module->addWire(new_verific_id(inst), inst->Input1Size());
1289
1290 for (int i = int(inst->Input1Size())-1; i >= 0; i--){
1291 sig_d.append(net_map_at(inst->GetInput1Bit(i)));
1292 sig_o.append(net_map_at(inst->GetOutputBit(i)));
1293 }
1294
1295 if (verific_verbose) {
1296 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1297 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1298 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1299 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1300 }
1301
1302 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1303 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1304
1305 if (!mode_keep)
1306 continue;
1307 }
1308
1309 if (inst->Type() == PRIM_SVA_STABLE)
1310 {
1311 VerificClocking clocking(this, inst->GetInput2());
1312 log_assert(clocking.disable_sig == State::S0);
1313 log_assert(clocking.body_net == nullptr);
1314
1315 SigSpec sig_d = net_map_at(inst->GetInput1());
1316 SigSpec sig_o = net_map_at(inst->GetOutput());
1317 SigSpec sig_q = module->addWire(new_verific_id(inst));
1318
1319 if (verific_verbose) {
1320 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1321 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1322 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1323 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1324 }
1325
1326 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1327 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1328
1329 if (!mode_keep)
1330 continue;
1331 }
1332
1333 if (inst->Type() == PRIM_SVA_PAST)
1334 {
1335 VerificClocking clocking(this, inst->GetInput2());
1336 log_assert(clocking.disable_sig == State::S0);
1337 log_assert(clocking.body_net == nullptr);
1338
1339 SigBit sig_d = net_map_at(inst->GetInput1());
1340 SigBit sig_q = net_map_at(inst->GetOutput());
1341
1342 if (verific_verbose)
1343 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1344 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1345
1346 past_ffs.insert(clocking.addDff(new_verific_id(inst), sig_d, sig_q));
1347
1348 if (!mode_keep)
1349 continue;
1350 }
1351
1352 if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
1353 {
1354 VerificClocking clocking(this, inst->GetInput2());
1355 log_assert(clocking.disable_sig == State::S0);
1356 log_assert(clocking.body_net == nullptr);
1357
1358 SigBit sig_d = net_map_at(inst->GetInput1());
1359 SigBit sig_o = net_map_at(inst->GetOutput());
1360 SigBit sig_q = module->addWire(new_verific_id(inst));
1361
1362 if (verific_verbose)
1363 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1364 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1365
1366 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1367 module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
1368
1369 if (!mode_keep)
1370 continue;
1371 }
1372
1373 if (!mode_keep && verific_sva_prims.count(inst->Type())) {
1374 if (verific_verbose)
1375 log(" skipping SVA cell in non k-mode\n");
1376 continue;
1377 }
1378
1379 if (inst->Type() == PRIM_HDL_ASSERTION)
1380 {
1381 SigBit cond = net_map_at(inst->GetInput());
1382
1383 if (verific_verbose)
1384 log(" assert condition %s.\n", log_signal(cond));
1385
1386 const char *assume_attr = nullptr; // inst->GetAttValue("assume");
1387
1388 Cell *cell = nullptr;
1389 if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
1390 cell = module->addAssume(new_verific_id(inst), cond, State::S1);
1391 else
1392 cell = module->addAssert(new_verific_id(inst), cond, State::S1);
1393
1394 import_attributes(cell->attributes, inst);
1395 continue;
1396 }
1397
1398 if (inst->IsPrimitive())
1399 {
1400 if (!mode_keep)
1401 log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1402
1403 if (!verific_sva_prims.count(inst->Type()))
1404 log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1405 }
1406
1407 import_verific_cells:
1408 nl_todo.insert(inst->View());
1409
1410 std::string inst_type = inst->View()->Owner()->Name();
1411
1412 if (inst->View()->IsOperator()) {
1413 inst_type = "$verific$" + inst_type;
1414 } else {
1415 if (*inst->View()->Name()) {
1416 inst_type += "(";
1417 inst_type += inst->View()->Name();
1418 inst_type += ")";
1419 }
1420 inst_type = "\\" + inst_type;
1421 }
1422
1423 RTLIL::Cell *cell = module->addCell(inst_name, inst_type);
1424
1425 if (inst->IsPrimitive() && mode_keep)
1426 cell->attributes["\\keep"] = 1;
1427
1428 dict<IdString, vector<SigBit>> cell_port_conns;
1429
1430 if (verific_verbose)
1431 log(" ports in verific db:\n");
1432
1433 FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
1434 if (verific_verbose)
1435 log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
1436 const char *port_name = pr->GetPort()->Name();
1437 int port_offset = 0;
1438 if (pr->GetPort()->Bus()) {
1439 port_name = pr->GetPort()->Bus()->Name();
1440 port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
1441 min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
1442 }
1443 IdString port_name_id = RTLIL::escape_id(port_name);
1444 auto &sigvec = cell_port_conns[port_name_id];
1445 if (GetSize(sigvec) <= port_offset) {
1446 SigSpec zwires = module->addWire(new_verific_id(inst), port_offset+1-GetSize(sigvec));
1447 for (auto bit : zwires)
1448 sigvec.push_back(bit);
1449 }
1450 sigvec[port_offset] = net_map_at(pr->GetNet());
1451 }
1452
1453 if (verific_verbose)
1454 log(" ports in yosys db:\n");
1455
1456 for (auto &it : cell_port_conns) {
1457 if (verific_verbose)
1458 log(" .%s(%s)\n", log_id(it.first), log_signal(it.second));
1459 cell->setPort(it.first, it.second);
1460 }
1461 }
1462
1463 if (!mode_nosva)
1464 {
1465 for (auto inst : sva_asserts) {
1466 if (mode_autocover)
1467 verific_import_sva_cover(this, inst);
1468 verific_import_sva_assert(this, inst);
1469 }
1470
1471 for (auto inst : sva_assumes)
1472 verific_import_sva_assume(this, inst);
1473
1474 for (auto inst : sva_covers)
1475 verific_import_sva_cover(this, inst);
1476
1477 for (auto inst : sva_triggers)
1478 verific_import_sva_trigger(this, inst);
1479
1480 merge_past_ffs(past_ffs);
1481 }
1482
1483 if (!mode_fullinit)
1484 {
1485 pool<SigBit> non_ff_bits;
1486 CellTypes ff_types;
1487
1488 ff_types.setup_internals_ff();
1489 ff_types.setup_stdcells_mem();
1490
1491 for (auto cell : module->cells())
1492 {
1493 if (ff_types.cell_known(cell->type))
1494 continue;
1495
1496 for (auto conn : cell->connections())
1497 {
1498 if (!cell->output(conn.first))
1499 continue;
1500
1501 for (auto bit : conn.second)
1502 if (bit.wire != nullptr)
1503 non_ff_bits.insert(bit);
1504 }
1505 }
1506
1507 for (auto wire : module->wires())
1508 {
1509 if (!wire->attributes.count("\\init"))
1510 continue;
1511
1512 Const &initval = wire->attributes.at("\\init");
1513 for (int i = 0; i < GetSize(initval); i++)
1514 {
1515 if (initval[i] != State::S0 && initval[i] != State::S1)
1516 continue;
1517
1518 if (non_ff_bits.count(SigBit(wire, i)))
1519 initval[i] = State::Sx;
1520 }
1521
1522 if (initval.is_fully_undef())
1523 wire->attributes.erase("\\init");
1524 }
1525 }
1526 }
1527
1528 // ==================================================================
1529
1530 VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
1531 {
1532 module = importer->module;
1533
1534 log_assert(importer != nullptr);
1535 log_assert(net != nullptr);
1536
1537 Instance *inst = net->Driver();
1538
1539 if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
1540 {
1541 net = inst->GetInput1();
1542 body_net = inst->GetInput2();
1543
1544 inst = net->Driver();
1545
1546 Instance *body_inst = body_net->Driver();
1547 if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) {
1548 disable_net = body_inst->GetInput1();
1549 disable_sig = importer->net_map_at(disable_net);
1550 body_net = body_inst->GetInput2();
1551 }
1552 }
1553 else
1554 {
1555 if (sva_at_only)
1556 return;
1557 }
1558
1559 // Use while() instead of if() to work around VIPER #13453
1560 while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
1561 {
1562 net = inst->GetInput();
1563 inst = net->Driver();;
1564 }
1565
1566 if (inst != nullptr && inst->Type() == PRIM_INV)
1567 {
1568 net = inst->GetInput();
1569 inst = net->Driver();;
1570 posedge = false;
1571 }
1572
1573 // Detect clock-enable circuit
1574 do {
1575 if (inst == nullptr || inst->Type() != PRIM_AND)
1576 break;
1577
1578 Net *net_dlatch = inst->GetInput1();
1579 Instance *inst_dlatch = net_dlatch->Driver();
1580
1581 if (inst_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS)
1582 break;
1583
1584 if (!inst_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd())
1585 break;
1586
1587 Net *net_enable = inst_dlatch->GetInput();
1588 Net *net_not_clock = inst_dlatch->GetControl();
1589
1590 if (net_enable == nullptr || net_not_clock == nullptr)
1591 break;
1592
1593 Instance *inst_not_clock = net_not_clock->Driver();
1594
1595 if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV)
1596 break;
1597
1598 Net *net_clock1 = inst_not_clock->GetInput();
1599 Net *net_clock2 = inst->GetInput2();
1600
1601 if (net_clock1 == nullptr || net_clock1 != net_clock2)
1602 break;
1603
1604 enable_net = net_enable;
1605 enable_sig = importer->net_map_at(enable_net);
1606
1607 net = net_clock1;
1608 inst = net->Driver();;
1609 } while (0);
1610
1611 // Detect condition expression
1612 do {
1613 if (body_net == nullptr)
1614 break;
1615
1616 Instance *inst_mux = body_net->Driver();
1617
1618 if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
1619 break;
1620
1621 if (!inst_mux->GetInput1()->IsPwr())
1622 break;
1623
1624 Net *sva_net = inst_mux->GetInput2();
1625 if (!verific_is_sva_net(importer, sva_net))
1626 break;
1627
1628 body_net = sva_net;
1629 cond_net = inst_mux->GetControl();
1630 } while (0);
1631
1632 clock_net = net;
1633 clock_sig = importer->net_map_at(clock_net);
1634
1635 const char *gclk_attr = clock_net->GetAttValue("gclk");
1636 if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'")))
1637 gclk = true;
1638 }
1639
1640 Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
1641 {
1642 log_assert(GetSize(sig_d) == GetSize(sig_q));
1643
1644 if (GetSize(init_value) != 0) {
1645 log_assert(GetSize(sig_q) == GetSize(init_value));
1646 if (sig_q.is_wire()) {
1647 sig_q.as_wire()->attributes["\\init"] = init_value;
1648 } else {
1649 Wire *w = module->addWire(NEW_ID, GetSize(sig_q));
1650 w->attributes["\\init"] = init_value;
1651 module->connect(sig_q, w);
1652 sig_q = w;
1653 }
1654 }
1655
1656 if (enable_sig != State::S1)
1657 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1658
1659 if (disable_sig != State::S0) {
1660 log_assert(gclk == false);
1661 log_assert(GetSize(sig_q) == GetSize(init_value));
1662 return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
1663 }
1664
1665 if (gclk)
1666 return module->addFf(name, sig_d, sig_q);
1667
1668 return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
1669 }
1670
1671 Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
1672 {
1673 log_assert(gclk == false);
1674 log_assert(disable_sig == State::S0);
1675
1676 if (enable_sig != State::S1)
1677 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1678
1679 return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge);
1680 }
1681
1682 Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
1683 {
1684 log_assert(gclk == false);
1685 log_assert(disable_sig == State::S0);
1686
1687 if (enable_sig != State::S1)
1688 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1689
1690 return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
1691 }
1692
1693 // ==================================================================
1694
1695 struct VerificExtNets
1696 {
1697 int portname_cnt = 0;
1698
1699 // a map from Net to the same Net one level up in the design hierarchy
1700 std::map<Net*, Net*> net_level_up_drive_up;
1701 std::map<Net*, Net*> net_level_up_drive_down;
1702
1703 Net *route_up(Net *net, bool drive_up, Net *final_net = nullptr)
1704 {
1705 auto &net_level_up = drive_up ? net_level_up_drive_up : net_level_up_drive_down;
1706
1707 if (net_level_up.count(net) == 0)
1708 {
1709 Netlist *nl = net->Owner();
1710
1711 // Simply return if Netlist is not unique
1712 log_assert(nl->NumOfRefs() == 1);
1713
1714 Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
1715 Netlist *up_nl = up_inst->Owner();
1716
1717 // create new Port
1718 string name = stringf("___extnets_%d", portname_cnt++);
1719 Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN);
1720 nl->Add(new_port);
1721 net->Connect(new_port);
1722
1723 // create new Net in up Netlist
1724 Net *new_net = final_net;
1725 if (new_net == nullptr || new_net->Owner() != up_nl) {
1726 new_net = new Net(name.c_str());
1727 up_nl->Add(new_net);
1728 }
1729 up_inst->Connect(new_port, new_net);
1730
1731 net_level_up[net] = new_net;
1732 }
1733
1734 return net_level_up.at(net);
1735 }
1736
1737 Net *route_up(Net *net, bool drive_up, Netlist *dest, Net *final_net = nullptr)
1738 {
1739 while (net->Owner() != dest)
1740 net = route_up(net, drive_up, final_net);
1741 if (final_net != nullptr)
1742 log_assert(net == final_net);
1743 return net;
1744 }
1745
1746 Netlist *find_common_ancestor(Netlist *A, Netlist *B)
1747 {
1748 std::set<Netlist*> ancestors_of_A;
1749
1750 Netlist *cursor = A;
1751 while (1) {
1752 ancestors_of_A.insert(cursor);
1753 if (cursor->NumOfRefs() != 1)
1754 break;
1755 cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
1756 }
1757
1758 cursor = B;
1759 while (1) {
1760 if (ancestors_of_A.count(cursor))
1761 return cursor;
1762 if (cursor->NumOfRefs() != 1)
1763 break;
1764 cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
1765 }
1766
1767 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());
1768 }
1769
1770 void run(Netlist *nl)
1771 {
1772 MapIter mi, mi2;
1773 Instance *inst;
1774 PortRef *pr;
1775
1776 vector<tuple<Instance*, Port*, Net*>> todo_connect;
1777
1778 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1779 run(inst->View());
1780
1781 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1782 FOREACH_PORTREF_OF_INST(inst, mi2, pr)
1783 {
1784 Port *port = pr->GetPort();
1785 Net *net = pr->GetNet();
1786
1787 if (!net->IsExternalTo(nl))
1788 continue;
1789
1790 if (verific_verbose)
1791 log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
1792
1793 Netlist *ext_nl = net->Owner();
1794
1795 if (verific_verbose)
1796 log(" external net owner: %s\n", get_full_netlist_name(ext_nl).c_str());
1797
1798 Netlist *ca_nl = find_common_ancestor(nl, ext_nl);
1799
1800 if (verific_verbose)
1801 log(" common ancestor: %s\n", get_full_netlist_name(ca_nl).c_str());
1802
1803 Net *ca_net = route_up(net, !port->IsOutput(), ca_nl);
1804 Net *new_net = ca_net;
1805
1806 if (ca_nl != nl)
1807 {
1808 if (verific_verbose)
1809 log(" net in common ancestor: %s\n", ca_net->Name());
1810
1811 string name = stringf("___extnets_%d", portname_cnt++);
1812 new_net = new Net(name.c_str());
1813 nl->Add(new_net);
1814
1815 Net *n YS_ATTRIBUTE(unused) = route_up(new_net, port->IsOutput(), ca_nl, ca_net);
1816 log_assert(n == ca_net);
1817 }
1818
1819 if (verific_verbose)
1820 log(" new local net: %s\n", new_net->Name());
1821
1822 log_assert(!new_net->IsExternalTo(nl));
1823 todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, new_net));
1824 }
1825
1826 for (auto it : todo_connect) {
1827 get<0>(it)->Disconnect(get<1>(it));
1828 get<0>(it)->Connect(get<1>(it), get<2>(it));
1829 }
1830 }
1831 };
1832
1833 void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
1834 {
1835 verific_sva_fsm_limit = 16;
1836
1837 std::set<Netlist*> nl_todo, nl_done;
1838
1839 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
1840 VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
1841 Array *netlists = NULL;
1842 Array veri_libs, vhdl_libs;
1843 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
1844 if (veri_lib) veri_libs.InsertLast(veri_lib);
1845
1846 Map verific_params(STRING_HASH);
1847 for (const auto &i : parameters)
1848 verific_params.Insert(i.first.c_str(), i.second.c_str());
1849
1850 if (top.empty()) {
1851 netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
1852 }
1853 else {
1854 Array veri_modules, vhdl_units;
1855
1856 if (veri_lib) {
1857 VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
1858 if (veri_module) {
1859 veri_modules.InsertLast(veri_module);
1860 }
1861
1862 // Also elaborate all root modules since they may contain bind statements
1863 MapIter mi;
1864 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
1865 if (!veri_module->IsRootModule()) continue;
1866 veri_modules.InsertLast(veri_module);
1867 }
1868 }
1869
1870 if (vhdl_lib) {
1871 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
1872 if (vhdl_unit)
1873 vhdl_units.InsertLast(vhdl_unit);
1874 }
1875
1876 netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
1877 }
1878
1879 Netlist *nl;
1880 int i;
1881
1882 FOREACH_ARRAY_ITEM(netlists, i, nl) {
1883 if (top.empty() && nl->CellBaseName() != top)
1884 continue;
1885 nl->AddAtt(new Att(" \\top", NULL));
1886 nl_todo.insert(nl);
1887 }
1888
1889 delete netlists;
1890
1891 if (!verific_error_msg.empty())
1892 log_error("%s\n", verific_error_msg.c_str());
1893
1894 VerificExtNets worker;
1895 for (auto nl : nl_todo)
1896 worker.run(nl);
1897
1898 while (!nl_todo.empty()) {
1899 Netlist *nl = *nl_todo.begin();
1900 if (nl_done.count(nl) == 0) {
1901 VerificImporter importer(false, false, false, false, false, false, false);
1902 importer.import_netlist(design, nl, nl_todo);
1903 }
1904 nl_todo.erase(nl);
1905 nl_done.insert(nl);
1906 }
1907
1908 veri_file::Reset();
1909 vhdl_file::Reset();
1910 Libset::Reset();
1911 verific_incdirs.clear();
1912 verific_libdirs.clear();
1913 verific_import_pending = false;
1914
1915 if (!verific_error_msg.empty())
1916 log_error("%s\n", verific_error_msg.c_str());
1917 }
1918
1919 YOSYS_NAMESPACE_END
1920 #endif /* YOSYS_ENABLE_VERIFIC */
1921
1922 PRIVATE_NAMESPACE_BEGIN
1923
1924 #ifdef YOSYS_ENABLE_VERIFIC
1925 bool check_noverific_env()
1926 {
1927 const char *e = getenv("YOSYS_NOVERIFIC");
1928 if (e == nullptr)
1929 return false;
1930 if (atoi(e) == 0)
1931 return false;
1932 return true;
1933 }
1934 #endif
1935
1936 struct VerificPass : public Pass {
1937 VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
1938 void help() YS_OVERRIDE
1939 {
1940 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1941 log("\n");
1942 log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
1943 log("\n");
1944 log("Load the specified Verilog/SystemVerilog files into Verific.\n");
1945 log("\n");
1946 log("All files specified in one call to this command are one compilation unit.\n");
1947 log("Files passed to different calls to this command are treated as belonging to\n");
1948 log("different compilation units.\n");
1949 log("\n");
1950 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
1951 log("the language version (and before file names) to set additional verilog defines.\n");
1952 log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
1953 log("\n");
1954 log("\n");
1955 log(" verific -formal <verilog-file>..\n");
1956 log("\n");
1957 log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
1958 log("\n");
1959 log("\n");
1960 log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
1961 log("\n");
1962 log("Load the specified VHDL files into Verific.\n");
1963 log("\n");
1964 log("\n");
1965 log(" verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>\n");
1966 log("\n");
1967 log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
1968 log("(default library when -work is not present: \"work\")\n");
1969 log("\n");
1970 log("\n");
1971 log(" verific [-L <libname>] {-sv|-vhdl|...} <hdl-file>\n");
1972 log("\n");
1973 log("Look up external definitions in the specified library.\n");
1974 log("(-L may be used more than once)\n");
1975 log("\n");
1976 log("\n");
1977 log(" verific -vlog-incdir <directory>..\n");
1978 log("\n");
1979 log("Add Verilog include directories.\n");
1980 log("\n");
1981 log("\n");
1982 log(" verific -vlog-libdir <directory>..\n");
1983 log("\n");
1984 log("Add Verilog library directories. Verific will search in this directories to\n");
1985 log("find undefined modules.\n");
1986 log("\n");
1987 log("\n");
1988 log(" verific -vlog-define <macro>[=<value>]..\n");
1989 log("\n");
1990 log("Add Verilog defines.\n");
1991 log("\n");
1992 log("\n");
1993 log(" verific -vlog-undef <macro>..\n");
1994 log("\n");
1995 log("Remove Verilog defines previously set with -vlog-define.\n");
1996 log("\n");
1997 log("\n");
1998 log(" verific -set-error <msg_id>..\n");
1999 log(" verific -set-warning <msg_id>..\n");
2000 log(" verific -set-info <msg_id>..\n");
2001 log(" verific -set-ignore <msg_id>..\n");
2002 log("\n");
2003 log("Set message severity. <msg_id> is the string in square brackets when a message\n");
2004 log("is printed, such as VERI-1209.\n");
2005 log("\n");
2006 log("\n");
2007 log(" verific -import [options] <top-module>..\n");
2008 log("\n");
2009 log("Elaborate the design for the specified top modules, import to Yosys and\n");
2010 log("reset the internal state of Verific.\n");
2011 log("\n");
2012 log("Import options:\n");
2013 log("\n");
2014 log(" -all\n");
2015 log(" Elaborate all modules, not just the hierarchy below the given top\n");
2016 log(" modules. With this option the list of modules to import is optional.\n");
2017 log("\n");
2018 log(" -gates\n");
2019 log(" Create a gate-level netlist.\n");
2020 log("\n");
2021 log(" -flatten\n");
2022 log(" Flatten the design in Verific before importing.\n");
2023 log("\n");
2024 log(" -extnets\n");
2025 log(" Resolve references to external nets by adding module ports as needed.\n");
2026 log("\n");
2027 log(" -autocover\n");
2028 log(" Generate automatic cover statements for all asserts\n");
2029 log("\n");
2030 log(" -fullinit\n");
2031 log(" Keep all register initializations, even those for non-FF registers.\n");
2032 log("\n");
2033 log(" -chparam name value \n");
2034 log(" Elaborate the specified top modules (all modules when -all given) using\n");
2035 log(" this parameter value. Modules on which this parameter does not exist will\n");
2036 log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
2037 log(" can be specified multiple times to override multiple parameters.\n");
2038 log(" String values must be passed in double quotes (\").\n");
2039 log("\n");
2040 log(" -v, -vv\n");
2041 log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
2042 log("\n");
2043 log("The following additional import options are useful for debugging the Verific\n");
2044 log("bindings (for Yosys and/or Verific developers):\n");
2045 log("\n");
2046 log(" -k\n");
2047 log(" Keep going after an unsupported verific primitive is found. The\n");
2048 log(" unsupported primitive is added as blockbox module to the design.\n");
2049 log(" This will also add all SVA related cells to the design parallel to\n");
2050 log(" the checker logic inferred by it.\n");
2051 log("\n");
2052 log(" -V\n");
2053 log(" Import Verific netlist as-is without translating to Yosys cell types. \n");
2054 log("\n");
2055 log(" -nosva\n");
2056 log(" Ignore SVA properties, do not infer checker logic.\n");
2057 log("\n");
2058 log(" -L <int>\n");
2059 log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
2060 log("\n");
2061 log(" -n\n");
2062 log(" Keep all Verific names on instances and nets. By default only\n");
2063 log(" user-declared names are preserved.\n");
2064 log("\n");
2065 log(" -d <dump_file>\n");
2066 log(" Dump the Verific netlist as a verilog file.\n");
2067 log("\n");
2068 log("Visit http://verific.com/ for more information on Verific.\n");
2069 log("\n");
2070 }
2071 #ifdef YOSYS_ENABLE_VERIFIC
2072 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2073 {
2074 static bool set_verific_global_flags = true;
2075
2076 if (check_noverific_env())
2077 log_cmd_error("This version of Yosys is built without Verific support.\n");
2078
2079 log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
2080
2081 if (set_verific_global_flags)
2082 {
2083 Message::SetConsoleOutput(0);
2084 Message::RegisterCallBackMsg(msg_func);
2085
2086 RuntimeFlags::SetVar("db_preserve_user_nets", 1);
2087 RuntimeFlags::SetVar("db_allow_external_nets", 1);
2088 RuntimeFlags::SetVar("db_infer_wide_operators", 1);
2089
2090 RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
2091 RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
2092
2093 RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
2094 RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
2095
2096 RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
2097 RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
2098
2099 // Workaround for VIPER #13851
2100 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
2101
2102 // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
2103 Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
2104
2105 // https://github.com/YosysHQ/yosys/issues/1055
2106 RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
2107
2108 #ifndef DB_PRESERVE_INITIAL_VALUE
2109 # warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
2110 #endif
2111
2112 set_verific_global_flags = false;
2113 }
2114
2115 verific_verbose = 0;
2116 verific_sva_fsm_limit = 16;
2117
2118 const char *release_str = Message::ReleaseString();
2119 time_t release_time = Message::ReleaseDate();
2120 char *release_tmstr = ctime(&release_time);
2121
2122 if (release_str == nullptr)
2123 release_str = "(no release string)";
2124
2125 for (char *p = release_tmstr; *p; p++)
2126 if (*p == '\n') *p = 0;
2127
2128 log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
2129
2130 int argidx = 1;
2131 std::string work = "work";
2132
2133 if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
2134 args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
2135 {
2136 msg_type_t new_type;
2137
2138 if (args[argidx] == "-set-error")
2139 new_type = VERIFIC_ERROR;
2140 else if (args[argidx] == "-set-warning")
2141 new_type = VERIFIC_WARNING;
2142 else if (args[argidx] == "-set-info")
2143 new_type = VERIFIC_INFO;
2144 else if (args[argidx] == "-set-ignore")
2145 new_type = VERIFIC_IGNORE;
2146 else
2147 log_abort();
2148
2149 for (argidx++; argidx < GetSize(args); argidx++)
2150 Message::SetMessageType(args[argidx].c_str(), new_type);
2151
2152 goto check_error;
2153 }
2154
2155 if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
2156 for (argidx++; argidx < GetSize(args); argidx++)
2157 verific_incdirs.push_back(args[argidx]);
2158 goto check_error;
2159 }
2160
2161 if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
2162 for (argidx++; argidx < GetSize(args); argidx++)
2163 verific_libdirs.push_back(args[argidx]);
2164 goto check_error;
2165 }
2166
2167 if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
2168 for (argidx++; argidx < GetSize(args); argidx++) {
2169 string name = args[argidx];
2170 size_t equal = name.find('=');
2171 if (equal != std::string::npos) {
2172 string value = name.substr(equal+1);
2173 name = name.substr(0, equal);
2174 veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
2175 } else {
2176 veri_file::DefineCmdLineMacro(name.c_str());
2177 }
2178 }
2179 goto check_error;
2180 }
2181
2182 if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
2183 for (argidx++; argidx < GetSize(args); argidx++) {
2184 string name = args[argidx];
2185 veri_file::UndefineMacro(name.c_str());
2186 }
2187 goto check_error;
2188 }
2189
2190 veri_file::RemoveAllLOptions();
2191 for (; argidx < GetSize(args); argidx++)
2192 {
2193 if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
2194 work = args[++argidx];
2195 continue;
2196 }
2197 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2198 veri_file::AddLOption(args[++argidx].c_str());
2199 continue;
2200 }
2201 break;
2202 }
2203
2204 if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
2205 args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
2206 {
2207 Array file_names;
2208 unsigned verilog_mode;
2209
2210 if (args[argidx] == "-vlog95")
2211 verilog_mode = veri_file::VERILOG_95;
2212 else if (args[argidx] == "-vlog2k")
2213 verilog_mode = veri_file::VERILOG_2K;
2214 else if (args[argidx] == "-sv2005")
2215 verilog_mode = veri_file::SYSTEM_VERILOG_2005;
2216 else if (args[argidx] == "-sv2009")
2217 verilog_mode = veri_file::SYSTEM_VERILOG_2009;
2218 else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
2219 verilog_mode = veri_file::SYSTEM_VERILOG;
2220 else
2221 log_abort();
2222
2223 veri_file::DefineMacro("VERIFIC");
2224 veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
2225
2226 for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].compare(0, 2, "-D") == 0; argidx++) {
2227 std::string name = args[argidx].substr(2);
2228 if (args[argidx] == "-D") {
2229 if (++argidx >= GetSize(args))
2230 break;
2231 name = args[argidx];
2232 }
2233 size_t equal = name.find('=');
2234 if (equal != std::string::npos) {
2235 string value = name.substr(equal+1);
2236 name = name.substr(0, equal);
2237 veri_file::DefineMacro(name.c_str(), value.c_str());
2238 } else {
2239 veri_file::DefineMacro(name.c_str());
2240 }
2241 }
2242
2243 for (auto &dir : verific_incdirs)
2244 veri_file::AddIncludeDir(dir.c_str());
2245 for (auto &dir : verific_libdirs)
2246 veri_file::AddYDir(dir.c_str());
2247
2248 while (argidx < GetSize(args))
2249 file_names.Insert(args[argidx++].c_str());
2250
2251 if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
2252 log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
2253
2254 verific_import_pending = true;
2255 goto check_error;
2256 }
2257
2258 if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
2259 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
2260 for (argidx++; argidx < GetSize(args); argidx++)
2261 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
2262 log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
2263 verific_import_pending = true;
2264 goto check_error;
2265 }
2266
2267 if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
2268 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2269 for (argidx++; argidx < GetSize(args); argidx++)
2270 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
2271 log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
2272 verific_import_pending = true;
2273 goto check_error;
2274 }
2275
2276 if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
2277 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2278 for (argidx++; argidx < GetSize(args); argidx++)
2279 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
2280 log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
2281 verific_import_pending = true;
2282 goto check_error;
2283 }
2284
2285 if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
2286 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
2287 for (argidx++; argidx < GetSize(args); argidx++)
2288 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
2289 log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
2290 verific_import_pending = true;
2291 goto check_error;
2292 }
2293
2294 if (GetSize(args) > argidx && args[argidx] == "-import")
2295 {
2296 std::set<Netlist*> nl_todo, nl_done;
2297 bool mode_all = false, mode_gates = false, mode_keep = false;
2298 bool mode_nosva = false, mode_names = false, mode_verific = false;
2299 bool mode_autocover = false, mode_fullinit = false;
2300 bool flatten = false, extnets = false;
2301 string dumpfile;
2302 Map parameters(STRING_HASH);
2303
2304 for (argidx++; argidx < GetSize(args); argidx++) {
2305 if (args[argidx] == "-all") {
2306 mode_all = true;
2307 continue;
2308 }
2309 if (args[argidx] == "-gates") {
2310 mode_gates = true;
2311 continue;
2312 }
2313 if (args[argidx] == "-flatten") {
2314 flatten = true;
2315 continue;
2316 }
2317 if (args[argidx] == "-extnets") {
2318 extnets = true;
2319 continue;
2320 }
2321 if (args[argidx] == "-k") {
2322 mode_keep = true;
2323 continue;
2324 }
2325 if (args[argidx] == "-nosva") {
2326 mode_nosva = true;
2327 continue;
2328 }
2329 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2330 verific_sva_fsm_limit = atoi(args[++argidx].c_str());
2331 continue;
2332 }
2333 if (args[argidx] == "-n") {
2334 mode_names = true;
2335 continue;
2336 }
2337 if (args[argidx] == "-autocover") {
2338 mode_autocover = true;
2339 continue;
2340 }
2341 if (args[argidx] == "-fullinit") {
2342 mode_fullinit = true;
2343 continue;
2344 }
2345 if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
2346 const std::string &key = args[++argidx];
2347 const std::string &value = args[++argidx];
2348 unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
2349 1 /* force_overwrite */);
2350 if (!new_insertion)
2351 log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
2352 continue;
2353 }
2354 if (args[argidx] == "-V") {
2355 mode_verific = true;
2356 continue;
2357 }
2358 if (args[argidx] == "-v") {
2359 verific_verbose = 1;
2360 continue;
2361 }
2362 if (args[argidx] == "-vv") {
2363 verific_verbose = 2;
2364 continue;
2365 }
2366 if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
2367 dumpfile = args[++argidx];
2368 continue;
2369 }
2370 break;
2371 }
2372
2373 if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
2374 cmd_error(args, argidx, "unknown option");
2375
2376 if (mode_all)
2377 {
2378 log("Running hier_tree::ElaborateAll().\n");
2379
2380 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2381 VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2382
2383 Array veri_libs, vhdl_libs;
2384 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
2385 if (veri_lib) veri_libs.InsertLast(veri_lib);
2386
2387 Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
2388 Netlist *nl;
2389 int i;
2390
2391 FOREACH_ARRAY_ITEM(netlists, i, nl)
2392 nl_todo.insert(nl);
2393 delete netlists;
2394 }
2395 else
2396 {
2397 if (argidx == GetSize(args))
2398 cmd_error(args, argidx, "No top module specified.\n");
2399
2400 Array veri_modules, vhdl_units;
2401 for (; argidx < GetSize(args); argidx++)
2402 {
2403 const char *name = args[argidx].c_str();
2404 VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2405
2406 if (veri_lib) {
2407 VeriModule *veri_module = veri_lib->GetModule(name, 1);
2408 if (veri_module) {
2409 log("Adding Verilog module '%s' to elaboration queue.\n", name);
2410 veri_modules.InsertLast(veri_module);
2411 continue;
2412 }
2413
2414 // Also elaborate all root modules since they may contain bind statements
2415 MapIter mi;
2416 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
2417 if (!veri_module->IsRootModule()) continue;
2418 veri_modules.InsertLast(veri_module);
2419 }
2420 }
2421
2422 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2423 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
2424 if (vhdl_unit) {
2425 log("Adding VHDL unit '%s' to elaboration queue.\n", name);
2426 vhdl_units.InsertLast(vhdl_unit);
2427 continue;
2428 }
2429
2430 log_error("Can't find module/unit '%s'.\n", name);
2431 }
2432
2433 log("Running hier_tree::Elaborate().\n");
2434 Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
2435 Netlist *nl;
2436 int i;
2437
2438 FOREACH_ARRAY_ITEM(netlists, i, nl) {
2439 nl->AddAtt(new Att(" \\top", NULL));
2440 nl_todo.insert(nl);
2441 }
2442 delete netlists;
2443 }
2444
2445 if (!verific_error_msg.empty())
2446 goto check_error;
2447
2448 if (flatten) {
2449 for (auto nl : nl_todo)
2450 nl->Flatten();
2451 }
2452
2453 if (extnets) {
2454 VerificExtNets worker;
2455 for (auto nl : nl_todo)
2456 worker.run(nl);
2457 }
2458
2459 if (!dumpfile.empty()) {
2460 VeriWrite veri_writer;
2461 veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign());
2462 }
2463
2464 while (!nl_todo.empty()) {
2465 Netlist *nl = *nl_todo.begin();
2466 if (nl_done.count(nl) == 0) {
2467 VerificImporter importer(mode_gates, mode_keep, mode_nosva,
2468 mode_names, mode_verific, mode_autocover, mode_fullinit);
2469 importer.import_netlist(design, nl, nl_todo);
2470 }
2471 nl_todo.erase(nl);
2472 nl_done.insert(nl);
2473 }
2474
2475 veri_file::Reset();
2476 vhdl_file::Reset();
2477 Libset::Reset();
2478 verific_incdirs.clear();
2479 verific_libdirs.clear();
2480 verific_import_pending = false;
2481 goto check_error;
2482 }
2483
2484 cmd_error(args, argidx, "Missing or unsupported mode parameter.\n");
2485
2486 check_error:
2487 if (!verific_error_msg.empty())
2488 log_error("%s\n", verific_error_msg.c_str());
2489
2490 }
2491 #else /* YOSYS_ENABLE_VERIFIC */
2492 void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
2493 log_cmd_error("This version of Yosys is built without Verific support.\n");
2494 }
2495 #endif
2496 } VerificPass;
2497
2498 struct ReadPass : public Pass {
2499 ReadPass() : Pass("read", "load HDL designs") { }
2500 void help() YS_OVERRIDE
2501 {
2502 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2503 log("\n");
2504 log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
2505 log("\n");
2506 log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
2507 log("is only available via Verific.)\n");
2508 log("\n");
2509 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2510 log("the language version (and before file names) to set additional verilog defines.\n");
2511 log("\n");
2512 log("\n");
2513 log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2514 log("\n");
2515 log("Load the specified VHDL files. (Requires Verific.)\n");
2516 log("\n");
2517 log("\n");
2518 log(" read -define <macro>[=<value>]..\n");
2519 log("\n");
2520 log("Set global Verilog/SystemVerilog defines.\n");
2521 log("\n");
2522 log("\n");
2523 log(" read -undef <macro>..\n");
2524 log("\n");
2525 log("Unset global Verilog/SystemVerilog defines.\n");
2526 log("\n");
2527 log("\n");
2528 log(" read -incdir <directory>\n");
2529 log("\n");
2530 log("Add directory to global Verilog/SystemVerilog include directories.\n");
2531 log("\n");
2532 log("\n");
2533 log(" read -verific\n");
2534 log(" read -noverific\n");
2535 log("\n");
2536 log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
2537 log("with -verific will result in an error on Yosys binaries that are built without\n");
2538 log("Verific support. The default is to use Verific if it is available.\n");
2539 log("\n");
2540 }
2541 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2542 {
2543 #ifdef YOSYS_ENABLE_VERIFIC
2544 static bool verific_available = !check_noverific_env();
2545 #else
2546 static bool verific_available = false;
2547 #endif
2548 static bool use_verific = verific_available;
2549
2550 if (args.size() < 2 || args[1][0] != '-')
2551 cmd_error(args, 1, "Missing mode parameter.\n");
2552
2553 if (args[1] == "-verific" || args[1] == "-noverific") {
2554 if (args.size() != 2)
2555 cmd_error(args, 1, "Additional arguments to -verific/-noverific.\n");
2556 if (args[1] == "-verific") {
2557 if (!verific_available)
2558 cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
2559 use_verific = true;
2560 } else {
2561 use_verific = false;
2562 }
2563 return;
2564 }
2565
2566 if (args.size() < 3)
2567 cmd_error(args, 3, "Missing file name parameter.\n");
2568
2569 if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
2570 if (use_verific) {
2571 args[0] = "verific";
2572 } else {
2573 args[0] = "read_verilog";
2574 args[1] = "-defer";
2575 }
2576 Pass::call(design, args);
2577 return;
2578 }
2579
2580 if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
2581 if (use_verific) {
2582 args[0] = "verific";
2583 } else {
2584 args[0] = "read_verilog";
2585 if (args[1] == "-formal")
2586 args.insert(args.begin()+1, std::string());
2587 args[1] = "-sv";
2588 args.insert(args.begin()+1, "-defer");
2589 }
2590 Pass::call(design, args);
2591 return;
2592 }
2593
2594 if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
2595 if (use_verific) {
2596 args[0] = "verific";
2597 Pass::call(design, args);
2598 } else {
2599 cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
2600 }
2601 return;
2602 }
2603
2604 if (args[1] == "-define") {
2605 if (use_verific) {
2606 args[0] = "verific";
2607 args[1] = "-vlog-define";
2608 Pass::call(design, args);
2609 }
2610 args[0] = "verilog_defines";
2611 args.erase(args.begin()+1, args.begin()+2);
2612 for (int i = 1; i < GetSize(args); i++)
2613 args[i] = "-D" + args[i];
2614 Pass::call(design, args);
2615 return;
2616 }
2617
2618 if (args[1] == "-undef") {
2619 if (use_verific) {
2620 args[0] = "verific";
2621 args[1] = "-vlog-undef";
2622 Pass::call(design, args);
2623 }
2624 args[0] = "verilog_defines";
2625 args.erase(args.begin()+1, args.begin()+2);
2626 for (int i = 1; i < GetSize(args); i++)
2627 args[i] = "-U" + args[i];
2628 Pass::call(design, args);
2629 return;
2630 }
2631
2632 if (args[1] == "-incdir") {
2633 if (use_verific) {
2634 args[0] = "verific";
2635 args[1] = "-vlog-incdir";
2636 Pass::call(design, args);
2637 }
2638 args[0] = "verilog_defaults";
2639 args[1] = "-add";
2640 for (int i = 2; i < GetSize(args); i++)
2641 args[i] = "-I" + args[i];
2642 Pass::call(design, args);
2643 return;
2644 }
2645
2646 cmd_error(args, 1, "Missing or unsupported mode parameter.\n");
2647 }
2648 } ReadPass;
2649
2650 PRIVATE_NAMESPACE_END