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