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