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