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