2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
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.
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.
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"
34 #include "frontends/verific/verific.h"
38 #ifdef YOSYS_ENABLE_VERIFIC
41 #pragma clang diagnostic push
42 #pragma clang diagnostic ignored "-Woverloaded-virtual"
45 #include "veri_file.h"
46 #include "vhdl_file.h"
47 #include "hier_tree.h"
48 #include "VeriModule.h"
49 #include "VeriWrite.h"
50 #include "VhdlUnits.h"
51 #include "VeriLibrary.h"
53 #if defined(YOSYSHQ_VERIFIC_INITSTATE) || defined(YOSYSHQ_VERIFIC_TEMPLATES) || defined(YOSYSHQ_VERIFIC_FORMALAPPS)
54 #include "VeriExtensions.h"
57 #ifndef YOSYSHQ_VERIFIC_API_VERSION
58 # error "Only YosysHQ flavored Verific is supported. Please contact office@yosyshq.com for commercial support for Yosys+Verific."
61 #if YOSYSHQ_VERIFIC_API_VERSION < 20210103
62 # error "Please update your version of YosysHQ flavored Verific."
66 #pragma clang diagnostic pop
69 #ifdef VERIFIC_NAMESPACE
70 using namespace Verific
;
75 #ifdef YOSYS_ENABLE_VERIFIC
79 bool verific_import_pending
;
80 string verific_error_msg
;
81 int verific_sva_fsm_limit
;
83 vector
<string
> verific_incdirs
, verific_libdirs
;
85 void msg_func(msg_type_t msg_type
, const char *message_id
, linefile_type linefile
, const char *msg
, va_list args
)
87 string message_prefix
= stringf("VERIFIC-%s [%s] ",
88 msg_type
== VERIFIC_NONE
? "NONE" :
89 msg_type
== VERIFIC_ERROR
? "ERROR" :
90 msg_type
== VERIFIC_WARNING
? "WARNING" :
91 msg_type
== VERIFIC_IGNORE
? "IGNORE" :
92 msg_type
== VERIFIC_INFO
? "INFO" :
93 msg_type
== VERIFIC_COMMENT
? "COMMENT" :
94 msg_type
== VERIFIC_PROGRAM_ERROR
? "PROGRAM_ERROR" : "UNKNOWN", message_id
);
96 string message
= linefile
? stringf("%s:%d: ", LineFile::GetFileName(linefile
), LineFile::GetLineNo(linefile
)) : "";
97 message
+= vstringf(msg
, args
);
99 if (msg_type
== VERIFIC_ERROR
|| msg_type
== VERIFIC_WARNING
|| msg_type
== VERIFIC_PROGRAM_ERROR
)
100 log_warning_noprefix("%s%s\n", message_prefix
.c_str(), message
.c_str());
102 log("%s%s\n", message_prefix
.c_str(), message
.c_str());
104 if (verific_error_msg
.empty() && (msg_type
== VERIFIC_ERROR
|| msg_type
== VERIFIC_PROGRAM_ERROR
))
105 verific_error_msg
= message
;
108 string
get_full_netlist_name(Netlist
*nl
)
110 if (nl
->NumOfRefs() == 1) {
111 Instance
*inst
= (Instance
*)nl
->GetReferences()->GetLast();
112 return get_full_netlist_name(inst
->Owner()) + "." + inst
->Name();
115 return nl
->CellBaseName();
118 // ==================================================================
120 VerificImporter::VerificImporter(bool mode_gates
, bool mode_keep
, bool mode_nosva
, bool mode_names
, bool mode_verific
, bool mode_autocover
, bool mode_fullinit
) :
121 mode_gates(mode_gates
), mode_keep(mode_keep
), mode_nosva(mode_nosva
),
122 mode_names(mode_names
), mode_verific(mode_verific
), mode_autocover(mode_autocover
),
123 mode_fullinit(mode_fullinit
)
127 RTLIL::SigBit
VerificImporter::net_map_at(Net
*net
)
129 if (net
->IsExternalTo(netlist
))
130 log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
131 get_full_netlist_name(net
->Owner()).c_str(), net
->Name(), get_full_netlist_name(netlist
).c_str());
133 return net_map
.at(net
);
136 bool is_blackbox(Netlist
*nl
)
138 if (nl
->IsBlackBox() || nl
->IsEmptyBox())
141 const char *attr
= nl
->GetAttValue("blackbox");
142 if (attr
!= nullptr && strcmp(attr
, "0"))
148 RTLIL::IdString
VerificImporter::new_verific_id(Verific::DesignObj
*obj
)
150 std::string s
= stringf("$verific$%s", obj
->Name());
152 s
+= stringf("$%s:%d", Verific::LineFile::GetFileName(obj
->Linefile()), Verific::LineFile::GetLineNo(obj
->Linefile()));
153 s
+= stringf("$%d", autoidx
++);
157 void VerificImporter::import_attributes(dict
<RTLIL::IdString
, RTLIL::Const
> &attributes
, DesignObj
*obj
, Netlist
*nl
)
163 attributes
[ID::src
] = stringf("%s:%d", LineFile::GetFileName(obj
->Linefile()), LineFile::GetLineNo(obj
->Linefile()));
165 // FIXME: Parse numeric attributes
166 FOREACH_ATTRIBUTE(obj
, mi
, attr
) {
167 if (attr
->Key()[0] == ' ' || attr
->Value() == nullptr)
169 attributes
[RTLIL::escape_id(attr
->Key())] = RTLIL::Const(std::string(attr
->Value()));
173 auto type_range
= nl
->GetTypeRange(obj
->Name());
176 if (!type_range
->IsTypeEnum())
178 if (nl
->IsFromVhdl() && strcmp(type_range
->GetTypeName(), "STD_LOGIC") == 0)
180 auto type_name
= type_range
->GetTypeName();
183 attributes
.emplace(ID::wiretype
, RTLIL::escape_id(type_name
));
187 FOREACH_MAP_ITEM(type_range
->GetEnumIdMap(), mi
, &k
, &v
) {
188 if (nl
->IsFromVerilog()) {
189 // Expect <decimal>'b<binary>
190 auto p
= strchr(v
, '\'');
195 for (auto q
= p
+2; *q
!= '\0'; q
++)
196 if (*q
!= '0' && *q
!= '1') {
202 log_error("Expected TypeRange value '%s' to be of form <decimal>'b<binary>.\n", v
);
203 attributes
.emplace(stringf("\\enum_value_%s", p
+2), RTLIL::escape_id(k
));
205 else if (nl
->IsFromVhdl()) {
206 // Expect "<binary>" or plain <binary>
211 auto q
= (char*)malloc(l
+1);
214 for(char *ptr
= q
; *ptr
; ++ptr
)*ptr
= tolower(*ptr
);
215 attributes
.emplace(stringf("\\enum_value_%s", q
), RTLIL::escape_id(k
));
218 for (; *q
!= '"'; q
++)
219 if (*q
!= '0' && *q
!= '1') {
223 if (p
&& *(q
+1) != '\0')
229 auto q
= (char*)malloc(l
+1-2);
230 strncpy(q
, p
+1, l
-2);
232 attributes
.emplace(stringf("\\enum_value_%s", q
), RTLIL::escape_id(k
));
238 log_error("Expected TypeRange value '%s' to be of form \"<binary>\" or <binary>.\n", v
);
244 RTLIL::SigSpec
VerificImporter::operatorInput(Instance
*inst
)
247 for (int i
= int(inst
->InputSize())-1; i
>= 0; i
--)
248 if (inst
->GetInputBit(i
))
249 sig
.append(net_map_at(inst
->GetInputBit(i
)));
251 sig
.append(RTLIL::State::Sz
);
255 RTLIL::SigSpec
VerificImporter::operatorInput1(Instance
*inst
)
258 for (int i
= int(inst
->Input1Size())-1; i
>= 0; i
--)
259 if (inst
->GetInput1Bit(i
))
260 sig
.append(net_map_at(inst
->GetInput1Bit(i
)));
262 sig
.append(RTLIL::State::Sz
);
266 RTLIL::SigSpec
VerificImporter::operatorInput2(Instance
*inst
)
269 for (int i
= int(inst
->Input2Size())-1; i
>= 0; i
--)
270 if (inst
->GetInput2Bit(i
))
271 sig
.append(net_map_at(inst
->GetInput2Bit(i
)));
273 sig
.append(RTLIL::State::Sz
);
277 RTLIL::SigSpec
VerificImporter::operatorInport(Instance
*inst
, const char *portname
)
279 PortBus
*portbus
= inst
->View()->GetPortBus(portname
);
282 for (unsigned i
= 0; i
< portbus
->Size(); i
++) {
283 Net
*net
= inst
->GetNet(portbus
->ElementAtIndex(i
));
286 sig
.append(RTLIL::State::S0
);
287 else if (net
->IsPwr())
288 sig
.append(RTLIL::State::S1
);
290 sig
.append(net_map_at(net
));
292 sig
.append(RTLIL::State::Sz
);
296 Port
*port
= inst
->View()->GetPort(portname
);
297 log_assert(port
!= NULL
);
298 Net
*net
= inst
->GetNet(port
);
299 return net_map_at(net
);
303 RTLIL::SigSpec
VerificImporter::operatorOutput(Instance
*inst
, const pool
<Net
*, hash_ptr_ops
> *any_all_nets
)
306 RTLIL::Wire
*dummy_wire
= NULL
;
307 for (int i
= int(inst
->OutputSize())-1; i
>= 0; i
--)
308 if (inst
->GetOutputBit(i
) && (!any_all_nets
|| !any_all_nets
->count(inst
->GetOutputBit(i
)))) {
309 sig
.append(net_map_at(inst
->GetOutputBit(i
)));
312 if (dummy_wire
== NULL
)
313 dummy_wire
= module
->addWire(new_verific_id(inst
));
316 sig
.append(RTLIL::SigSpec(dummy_wire
, dummy_wire
->width
- 1));
321 bool VerificImporter::import_netlist_instance_gates(Instance
*inst
, RTLIL::IdString inst_name
)
323 if (inst
->Type() == PRIM_AND
) {
324 module
->addAndGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
328 if (inst
->Type() == PRIM_NAND
) {
329 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
330 module
->addAndGate(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
331 module
->addNotGate(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
335 if (inst
->Type() == PRIM_OR
) {
336 module
->addOrGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
340 if (inst
->Type() == PRIM_NOR
) {
341 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
342 module
->addOrGate(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
343 module
->addNotGate(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
347 if (inst
->Type() == PRIM_XOR
) {
348 module
->addXorGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
352 if (inst
->Type() == PRIM_XNOR
) {
353 module
->addXnorGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
357 if (inst
->Type() == PRIM_BUF
) {
358 auto outnet
= inst
->GetOutput();
359 if (!any_all_nets
.count(outnet
))
360 module
->addBufGate(inst_name
, net_map_at(inst
->GetInput()), net_map_at(outnet
));
364 if (inst
->Type() == PRIM_INV
) {
365 module
->addNotGate(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
369 if (inst
->Type() == PRIM_MUX
) {
370 module
->addMuxGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetControl()), net_map_at(inst
->GetOutput()));
374 if (inst
->Type() == PRIM_TRI
) {
375 module
->addMuxGate(inst_name
, RTLIL::State::Sz
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetControl()), net_map_at(inst
->GetOutput()));
379 if (inst
->Type() == PRIM_FADD
)
381 RTLIL::SigSpec a
= net_map_at(inst
->GetInput1()), b
= net_map_at(inst
->GetInput2()), c
= net_map_at(inst
->GetCin());
382 RTLIL::SigSpec x
= inst
->GetCout() ? net_map_at(inst
->GetCout()) : module
->addWire(new_verific_id(inst
));
383 RTLIL::SigSpec y
= inst
->GetOutput() ? net_map_at(inst
->GetOutput()) : module
->addWire(new_verific_id(inst
));
384 RTLIL::SigSpec tmp1
= module
->addWire(new_verific_id(inst
));
385 RTLIL::SigSpec tmp2
= module
->addWire(new_verific_id(inst
));
386 RTLIL::SigSpec tmp3
= module
->addWire(new_verific_id(inst
));
387 module
->addXorGate(new_verific_id(inst
), a
, b
, tmp1
);
388 module
->addXorGate(inst_name
, tmp1
, c
, y
);
389 module
->addAndGate(new_verific_id(inst
), tmp1
, c
, tmp2
);
390 module
->addAndGate(new_verific_id(inst
), a
, b
, tmp3
);
391 module
->addOrGate(new_verific_id(inst
), tmp2
, tmp3
, x
);
395 if (inst
->Type() == PRIM_DFFRS
)
397 VerificClocking
clocking(this, inst
->GetClock());
398 log_assert(clocking
.disable_sig
== State::S0
);
399 log_assert(clocking
.body_net
== nullptr);
401 if (inst
->GetSet()->IsGnd() && inst
->GetReset()->IsGnd())
402 clocking
.addDff(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
403 else if (inst
->GetSet()->IsGnd())
404 clocking
.addAdff(inst_name
, net_map_at(inst
->GetReset()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), State::S0
);
405 else if (inst
->GetReset()->IsGnd())
406 clocking
.addAdff(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), State::S1
);
408 clocking
.addDffsr(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetReset()),
409 net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
416 bool VerificImporter::import_netlist_instance_cells(Instance
*inst
, RTLIL::IdString inst_name
)
418 RTLIL::Cell
*cell
= nullptr;
420 if (inst
->Type() == PRIM_AND
) {
421 cell
= module
->addAnd(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
422 import_attributes(cell
->attributes
, inst
);
426 if (inst
->Type() == PRIM_NAND
) {
427 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
428 cell
= module
->addAnd(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
429 import_attributes(cell
->attributes
, inst
);
430 cell
= module
->addNot(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
431 import_attributes(cell
->attributes
, inst
);
435 if (inst
->Type() == PRIM_OR
) {
436 cell
= module
->addOr(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
437 import_attributes(cell
->attributes
, inst
);
441 if (inst
->Type() == PRIM_NOR
) {
442 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
443 cell
= module
->addOr(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
444 import_attributes(cell
->attributes
, inst
);
445 cell
= module
->addNot(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
446 import_attributes(cell
->attributes
, inst
);
450 if (inst
->Type() == PRIM_XOR
) {
451 cell
= module
->addXor(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
452 import_attributes(cell
->attributes
, inst
);
456 if (inst
->Type() == PRIM_XNOR
) {
457 cell
= module
->addXnor(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
458 import_attributes(cell
->attributes
, inst
);
462 if (inst
->Type() == PRIM_INV
) {
463 cell
= module
->addNot(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
464 import_attributes(cell
->attributes
, inst
);
468 if (inst
->Type() == PRIM_MUX
) {
469 cell
= module
->addMux(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetControl()), net_map_at(inst
->GetOutput()));
470 import_attributes(cell
->attributes
, inst
);
474 if (inst
->Type() == PRIM_TRI
) {
475 cell
= module
->addMux(inst_name
, RTLIL::State::Sz
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetControl()), net_map_at(inst
->GetOutput()));
476 import_attributes(cell
->attributes
, inst
);
480 if (inst
->Type() == PRIM_FADD
)
482 RTLIL::SigSpec a_plus_b
= module
->addWire(new_verific_id(inst
), 2);
483 RTLIL::SigSpec y
= inst
->GetOutput() ? net_map_at(inst
->GetOutput()) : module
->addWire(new_verific_id(inst
));
485 y
.append(net_map_at(inst
->GetCout()));
486 cell
= module
->addAdd(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), a_plus_b
);
487 import_attributes(cell
->attributes
, inst
);
488 cell
= module
->addAdd(inst_name
, a_plus_b
, net_map_at(inst
->GetCin()), y
);
489 import_attributes(cell
->attributes
, inst
);
493 if (inst
->Type() == PRIM_DFFRS
)
495 VerificClocking
clocking(this, inst
->GetClock());
496 log_assert(clocking
.disable_sig
== State::S0
);
497 log_assert(clocking
.body_net
== nullptr);
499 if (inst
->GetSet()->IsGnd() && inst
->GetReset()->IsGnd())
500 cell
= clocking
.addDff(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
501 else if (inst
->GetSet()->IsGnd())
502 cell
= clocking
.addAdff(inst_name
, net_map_at(inst
->GetReset()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), RTLIL::State::S0
);
503 else if (inst
->GetReset()->IsGnd())
504 cell
= clocking
.addAdff(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), RTLIL::State::S1
);
506 cell
= clocking
.addDffsr(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetReset()),
507 net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
508 import_attributes(cell
->attributes
, inst
);
512 if (inst
->Type() == PRIM_DLATCHRS
)
514 if (inst
->GetSet()->IsGnd() && inst
->GetReset()->IsGnd())
515 cell
= module
->addDlatch(inst_name
, net_map_at(inst
->GetControl()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
517 cell
= module
->addDlatchsr(inst_name
, net_map_at(inst
->GetControl()), net_map_at(inst
->GetSet()), net_map_at(inst
->GetReset()),
518 net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
519 import_attributes(cell
->attributes
, inst
);
523 #define IN operatorInput(inst)
524 #define IN1 operatorInput1(inst)
525 #define IN2 operatorInput2(inst)
526 #define OUT operatorOutput(inst)
527 #define FILTERED_OUT operatorOutput(inst, &any_all_nets)
528 #define SIGNED inst->View()->IsSigned()
530 if (inst
->Type() == OPER_ADDER
) {
531 RTLIL::SigSpec out
= OUT
;
532 if (inst
->GetCout() != NULL
)
533 out
.append(net_map_at(inst
->GetCout()));
534 if (inst
->GetCin()->IsGnd()) {
535 cell
= module
->addAdd(inst_name
, IN1
, IN2
, out
, SIGNED
);
536 import_attributes(cell
->attributes
, inst
);
538 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
), GetSize(out
));
539 cell
= module
->addAdd(new_verific_id(inst
), IN1
, IN2
, tmp
, SIGNED
);
540 import_attributes(cell
->attributes
, inst
);
541 cell
= module
->addAdd(inst_name
, tmp
, net_map_at(inst
->GetCin()), out
, false);
542 import_attributes(cell
->attributes
, inst
);
547 if (inst
->Type() == OPER_MULTIPLIER
) {
548 cell
= module
->addMul(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
549 import_attributes(cell
->attributes
, inst
);
553 if (inst
->Type() == OPER_DIVIDER
) {
554 cell
= module
->addDiv(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
555 import_attributes(cell
->attributes
, inst
);
559 if (inst
->Type() == OPER_MODULO
) {
560 cell
= module
->addMod(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
561 import_attributes(cell
->attributes
, inst
);
565 if (inst
->Type() == OPER_REMAINDER
) {
566 cell
= module
->addMod(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
567 import_attributes(cell
->attributes
, inst
);
571 if (inst
->Type() == OPER_SHIFT_LEFT
) {
572 cell
= module
->addShl(inst_name
, IN1
, IN2
, OUT
, false);
573 import_attributes(cell
->attributes
, inst
);
577 if (inst
->Type() == OPER_ENABLED_DECODER
) {
579 vec
.append(net_map_at(inst
->GetControl()));
580 for (unsigned i
= 1; i
< inst
->OutputSize(); i
++) {
581 vec
.append(RTLIL::State::S0
);
583 cell
= module
->addShl(inst_name
, vec
, IN
, OUT
, false);
584 import_attributes(cell
->attributes
, inst
);
588 if (inst
->Type() == OPER_DECODER
) {
590 vec
.append(RTLIL::State::S1
);
591 for (unsigned i
= 1; i
< inst
->OutputSize(); i
++) {
592 vec
.append(RTLIL::State::S0
);
594 cell
= module
->addShl(inst_name
, vec
, IN
, OUT
, false);
595 import_attributes(cell
->attributes
, inst
);
599 if (inst
->Type() == OPER_SHIFT_RIGHT
) {
600 Net
*net_cin
= inst
->GetCin();
601 Net
*net_a_msb
= inst
->GetInput1Bit(0);
602 if (net_cin
->IsGnd())
603 cell
= module
->addShr(inst_name
, IN1
, IN2
, OUT
, false);
604 else if (net_cin
== net_a_msb
)
605 cell
= module
->addSshr(inst_name
, IN1
, IN2
, OUT
, true);
607 log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst
->Name());
608 import_attributes(cell
->attributes
, inst
);
612 if (inst
->Type() == OPER_REDUCE_AND
) {
613 cell
= module
->addReduceAnd(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
614 import_attributes(cell
->attributes
, inst
);
618 if (inst
->Type() == OPER_REDUCE_NAND
) {
619 Wire
*tmp
= module
->addWire(NEW_ID
);
620 cell
= module
->addReduceAnd(inst_name
, IN
, tmp
, SIGNED
);
621 module
->addNot(NEW_ID
, tmp
, net_map_at(inst
->GetOutput()));
622 import_attributes(cell
->attributes
, inst
);
626 if (inst
->Type() == OPER_REDUCE_OR
) {
627 cell
= module
->addReduceOr(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
628 import_attributes(cell
->attributes
, inst
);
632 if (inst
->Type() == OPER_REDUCE_XOR
) {
633 cell
= module
->addReduceXor(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
634 import_attributes(cell
->attributes
, inst
);
638 if (inst
->Type() == OPER_REDUCE_XNOR
) {
639 cell
= module
->addReduceXnor(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
640 import_attributes(cell
->attributes
, inst
);
644 if (inst
->Type() == OPER_REDUCE_NOR
) {
645 SigSpec t
= module
->ReduceOr(new_verific_id(inst
), IN
, SIGNED
);
646 cell
= module
->addNot(inst_name
, t
, net_map_at(inst
->GetOutput()));
647 import_attributes(cell
->attributes
, inst
);
651 if (inst
->Type() == OPER_LESSTHAN
) {
652 Net
*net_cin
= inst
->GetCin();
653 if (net_cin
->IsGnd())
654 cell
= module
->addLt(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
655 else if (net_cin
->IsPwr())
656 cell
= module
->addLe(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
658 log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst
->Name());
659 import_attributes(cell
->attributes
, inst
);
663 if (inst
->Type() == OPER_WIDE_AND
) {
664 cell
= module
->addAnd(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
665 import_attributes(cell
->attributes
, inst
);
669 if (inst
->Type() == OPER_WIDE_OR
) {
670 cell
= module
->addOr(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
671 import_attributes(cell
->attributes
, inst
);
675 if (inst
->Type() == OPER_WIDE_XOR
) {
676 cell
= module
->addXor(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
677 import_attributes(cell
->attributes
, inst
);
681 if (inst
->Type() == OPER_WIDE_XNOR
) {
682 cell
= module
->addXnor(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
683 import_attributes(cell
->attributes
, inst
);
687 if (inst
->Type() == OPER_WIDE_BUF
) {
688 cell
= module
->addPos(inst_name
, IN
, FILTERED_OUT
, SIGNED
);
689 import_attributes(cell
->attributes
, inst
);
693 if (inst
->Type() == OPER_WIDE_INV
) {
694 cell
= module
->addNot(inst_name
, IN
, OUT
, SIGNED
);
695 import_attributes(cell
->attributes
, inst
);
699 if (inst
->Type() == OPER_MINUS
) {
700 cell
= module
->addSub(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
701 import_attributes(cell
->attributes
, inst
);
705 if (inst
->Type() == OPER_UMINUS
) {
706 cell
= module
->addNeg(inst_name
, IN
, OUT
, SIGNED
);
707 import_attributes(cell
->attributes
, inst
);
711 if (inst
->Type() == OPER_EQUAL
) {
712 cell
= module
->addEq(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
713 import_attributes(cell
->attributes
, inst
);
717 if (inst
->Type() == OPER_NEQUAL
) {
718 cell
= module
->addNe(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
719 import_attributes(cell
->attributes
, inst
);
723 if (inst
->Type() == OPER_WIDE_MUX
) {
724 cell
= module
->addMux(inst_name
, IN1
, IN2
, net_map_at(inst
->GetControl()), OUT
);
725 import_attributes(cell
->attributes
, inst
);
729 if (inst
->Type() == OPER_NTO1MUX
) {
730 cell
= module
->addShr(inst_name
, IN2
, IN1
, net_map_at(inst
->GetOutput()));
731 import_attributes(cell
->attributes
, inst
);
735 if (inst
->Type() == OPER_WIDE_NTO1MUX
)
737 SigSpec data
= IN2
, out
= OUT
;
739 int wordsize_bits
= ceil_log2(GetSize(out
));
740 int wordsize
= 1 << wordsize_bits
;
742 SigSpec sel
= {IN1
, SigSpec(State::S0
, wordsize_bits
)};
745 for (int i
= 0; i
< GetSize(data
); i
+= GetSize(out
)) {
746 SigSpec d
= data
.extract(i
, GetSize(out
));
747 d
.extend_u0(wordsize
);
748 padded_data
.append(d
);
751 cell
= module
->addShr(inst_name
, padded_data
, sel
, out
);
752 import_attributes(cell
->attributes
, inst
);
756 if (inst
->Type() == OPER_SELECTOR
)
758 cell
= module
->addPmux(inst_name
, State::S0
, IN2
, IN1
, net_map_at(inst
->GetOutput()));
759 import_attributes(cell
->attributes
, inst
);
763 if (inst
->Type() == OPER_WIDE_SELECTOR
)
766 cell
= module
->addPmux(inst_name
, SigSpec(State::S0
, GetSize(out
)), IN2
, IN1
, out
);
767 import_attributes(cell
->attributes
, inst
);
771 if (inst
->Type() == OPER_WIDE_TRI
) {
772 cell
= module
->addMux(inst_name
, RTLIL::SigSpec(RTLIL::State::Sz
, inst
->OutputSize()), IN
, net_map_at(inst
->GetControl()), OUT
);
773 import_attributes(cell
->attributes
, inst
);
777 if (inst
->Type() == OPER_WIDE_DFFRS
)
779 VerificClocking
clocking(this, inst
->GetClock());
780 log_assert(clocking
.disable_sig
== State::S0
);
781 log_assert(clocking
.body_net
== nullptr);
783 RTLIL::SigSpec sig_set
= operatorInport(inst
, "set");
784 RTLIL::SigSpec sig_reset
= operatorInport(inst
, "reset");
786 if (sig_set
.is_fully_const() && !sig_set
.as_bool() && sig_reset
.is_fully_const() && !sig_reset
.as_bool())
787 cell
= clocking
.addDff(inst_name
, IN
, OUT
);
789 cell
= clocking
.addDffsr(inst_name
, sig_set
, sig_reset
, IN
, OUT
);
790 import_attributes(cell
->attributes
, inst
);
804 void VerificImporter::merge_past_ffs_clock(pool
<RTLIL::Cell
*> &candidates
, SigBit clock
, bool clock_pol
)
806 bool keep_running
= true;
811 keep_running
= false;
813 dict
<SigBit
, pool
<RTLIL::Cell
*>> dbits_db
;
816 for (auto cell
: candidates
) {
817 SigBit bit
= sigmap(cell
->getPort(ID::D
));
818 dbits_db
[bit
].insert(cell
);
822 dbits
.sort_and_unify();
824 for (auto chunk
: dbits
.chunks())
826 SigSpec sig_d
= chunk
;
828 if (chunk
.wire
== nullptr || GetSize(sig_d
) == 1)
831 SigSpec sig_q
= module
->addWire(NEW_ID
, GetSize(sig_d
));
832 RTLIL::Cell
*new_ff
= module
->addDff(NEW_ID
, clock
, sig_d
, sig_q
, clock_pol
);
835 log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d
), log_id(new_ff
));
837 for (int i
= 0; i
< GetSize(sig_d
); i
++)
838 for (auto old_ff
: dbits_db
[sig_d
[i
]])
841 log(" replacing old ff %s on bit %d.\n", log_id(old_ff
), i
);
843 SigBit old_q
= old_ff
->getPort(ID::Q
);
844 SigBit new_q
= sig_q
[i
];
846 sigmap
.add(old_q
, new_q
);
847 module
->connect(old_q
, new_q
);
848 candidates
.erase(old_ff
);
849 module
->remove(old_ff
);
856 void VerificImporter::merge_past_ffs(pool
<RTLIL::Cell
*> &candidates
)
858 dict
<pair
<SigBit
, int>, pool
<RTLIL::Cell
*>> database
;
860 for (auto cell
: candidates
)
862 SigBit clock
= cell
->getPort(ID::CLK
);
863 bool clock_pol
= cell
->getParam(ID::CLK_POLARITY
).as_bool();
864 database
[make_pair(clock
, int(clock_pol
))].insert(cell
);
867 for (auto it
: database
)
868 merge_past_ffs_clock(it
.second
, it
.first
.first
, it
.first
.second
);
871 static std::string
sha1_if_contain_spaces(std::string str
)
873 if(str
.find_first_of(' ') != std::string::npos
) {
874 std::size_t open
= str
.find_first_of('(');
875 std::size_t closed
= str
.find_last_of(')');
876 if (open
!= std::string::npos
&& closed
!= std::string::npos
) {
877 std::string content
= str
.substr(open
+ 1, closed
- open
- 1);
878 return str
.substr(0, open
+ 1) + sha1(content
) + str
.substr(closed
);
886 void VerificImporter::import_netlist(RTLIL::Design
*design
, Netlist
*nl
, std::set
<Netlist
*> &nl_todo
, bool norename
)
888 std::string netlist_name
= nl
->GetAtt(" \\top") ? nl
->CellBaseName() : nl
->Owner()->Name();
889 std::string module_name
= netlist_name
;
891 if (nl
->IsOperator() || nl
->IsPrimitive()) {
892 module_name
= "$verific$" + module_name
;
894 if (!norename
&& *nl
->Name()) {
896 module_name
+= nl
->Name();
899 module_name
= "\\" + sha1_if_contain_spaces(module_name
);
904 if (design
->has(module_name
)) {
905 if (!nl
->IsOperator() && !is_blackbox(nl
))
906 log_cmd_error("Re-definition of module `%s'.\n", netlist_name
.c_str());
910 module
= new RTLIL::Module
;
911 module
->name
= module_name
;
914 if (is_blackbox(nl
)) {
915 log("Importing blackbox module %s.\n", RTLIL::id2cstr(module
->name
));
916 module
->set_bool_attribute(ID::blackbox
);
918 log("Importing module %s.\n", RTLIL::id2cstr(module
->name
));
930 FOREACH_PORT_OF_NETLIST(nl
, mi
, port
)
936 log(" importing port %s.\n", port
->Name());
938 RTLIL::Wire
*wire
= module
->addWire(RTLIL::escape_id(port
->Name()));
939 import_attributes(wire
->attributes
, port
, nl
);
941 wire
->port_id
= nl
->IndexOf(port
) + 1;
943 if (port
->GetDir() == DIR_INOUT
|| port
->GetDir() == DIR_IN
)
944 wire
->port_input
= true;
945 if (port
->GetDir() == DIR_INOUT
|| port
->GetDir() == DIR_OUT
)
946 wire
->port_output
= true;
948 if (port
->GetNet()) {
949 net
= port
->GetNet();
950 if (net_map
.count(net
) == 0)
952 else if (wire
->port_input
)
953 module
->connect(net_map_at(net
), wire
);
955 module
->connect(wire
, net_map_at(net
));
959 FOREACH_PORTBUS_OF_NETLIST(nl
, mi
, portbus
)
962 log(" importing portbus %s.\n", portbus
->Name());
964 RTLIL::Wire
*wire
= module
->addWire(RTLIL::escape_id(portbus
->Name()), portbus
->Size());
965 wire
->start_offset
= min(portbus
->LeftIndex(), portbus
->RightIndex());
966 import_attributes(wire
->attributes
, portbus
, nl
);
968 if (portbus
->GetDir() == DIR_INOUT
|| portbus
->GetDir() == DIR_IN
)
969 wire
->port_input
= true;
970 if (portbus
->GetDir() == DIR_INOUT
|| portbus
->GetDir() == DIR_OUT
)
971 wire
->port_output
= true;
973 for (int i
= portbus
->LeftIndex();; i
+= portbus
->IsUp() ? +1 : -1) {
974 if (portbus
->ElementAtIndex(i
) && portbus
->ElementAtIndex(i
)->GetNet()) {
975 net
= portbus
->ElementAtIndex(i
)->GetNet();
976 RTLIL::SigBit
bit(wire
, i
- wire
->start_offset
);
977 if (net_map
.count(net
) == 0)
979 else if (wire
->port_input
)
980 module
->connect(net_map_at(net
), bit
);
982 module
->connect(bit
, net_map_at(net
));
984 if (i
== portbus
->RightIndex())
989 module
->fixup_ports();
991 dict
<Net
*, char, hash_ptr_ops
> init_nets
;
992 pool
<Net
*, hash_ptr_ops
> anyconst_nets
, anyseq_nets
;
993 pool
<Net
*, hash_ptr_ops
> allconst_nets
, allseq_nets
;
994 any_all_nets
.clear();
996 FOREACH_NET_OF_NETLIST(nl
, mi
, net
)
1000 RTLIL::Memory
*memory
= new RTLIL::Memory
;
1001 memory
->name
= RTLIL::escape_id(net
->Name());
1002 log_assert(module
->count_id(memory
->name
) == 0);
1003 module
->memories
[memory
->name
] = memory
;
1005 int number_of_bits
= net
->Size();
1006 number_of_bits
= 1 << ceil_log2(number_of_bits
);
1007 int bits_in_word
= number_of_bits
;
1008 FOREACH_PORTREF_OF_NET(net
, si
, pr
) {
1009 if (pr
->GetInst()->Type() == OPER_READ_PORT
) {
1010 bits_in_word
= min
<int>(bits_in_word
, pr
->GetInst()->OutputSize());
1013 if (pr
->GetInst()->Type() == OPER_WRITE_PORT
|| pr
->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT
) {
1014 bits_in_word
= min
<int>(bits_in_word
, pr
->GetInst()->Input2Size());
1017 log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
1018 net
->Name(), pr
->GetInst()->View()->Owner()->Name(), pr
->GetInst()->Name());
1021 memory
->width
= bits_in_word
;
1022 memory
->size
= number_of_bits
/ bits_in_word
;
1024 const char *ascii_initdata
= net
->GetWideInitialValue();
1025 if (ascii_initdata
) {
1026 while (*ascii_initdata
!= 0 && *ascii_initdata
!= '\'')
1028 if (*ascii_initdata
== '\'')
1030 if (*ascii_initdata
!= 0) {
1031 log_assert(*ascii_initdata
== 'b');
1034 for (int word_idx
= 0; word_idx
< memory
->size
; word_idx
++) {
1035 Const initval
= Const(State::Sx
, memory
->width
);
1036 bool initval_valid
= false;
1037 for (int bit_idx
= memory
->width
-1; bit_idx
>= 0; bit_idx
--) {
1038 if (*ascii_initdata
== 0)
1040 if (*ascii_initdata
== '0' || *ascii_initdata
== '1') {
1041 initval
[bit_idx
] = (*ascii_initdata
== '0') ? State::S0
: State::S1
;
1042 initval_valid
= true;
1046 if (initval_valid
) {
1047 RTLIL::Cell
*cell
= module
->addCell(new_verific_id(net
), ID($meminit
));
1048 cell
->parameters
[ID::WORDS
] = 1;
1049 if (net
->GetOrigTypeRange()->LeftRangeBound() < net
->GetOrigTypeRange()->RightRangeBound())
1050 cell
->setPort(ID::ADDR
, word_idx
);
1052 cell
->setPort(ID::ADDR
, memory
->size
- word_idx
- 1);
1053 cell
->setPort(ID::DATA
, initval
);
1054 cell
->parameters
[ID::MEMID
] = RTLIL::Const(memory
->name
.str());
1055 cell
->parameters
[ID::ABITS
] = 32;
1056 cell
->parameters
[ID::WIDTH
] = memory
->width
;
1057 cell
->parameters
[ID::PRIORITY
] = RTLIL::Const(autoidx
-1);
1064 if (net
->GetInitialValue())
1065 init_nets
[net
] = net
->GetInitialValue();
1067 const char *rand_const_attr
= net
->GetAttValue(" rand_const");
1068 const char *rand_attr
= net
->GetAttValue(" rand");
1070 const char *anyconst_attr
= net
->GetAttValue("anyconst");
1071 const char *anyseq_attr
= net
->GetAttValue("anyseq");
1073 const char *allconst_attr
= net
->GetAttValue("allconst");
1074 const char *allseq_attr
= net
->GetAttValue("allseq");
1076 if (rand_const_attr
!= nullptr && (!strcmp(rand_const_attr
, "1") || !strcmp(rand_const_attr
, "'1'"))) {
1077 anyconst_nets
.insert(net
);
1078 any_all_nets
.insert(net
);
1080 else if (rand_attr
!= nullptr && (!strcmp(rand_attr
, "1") || !strcmp(rand_attr
, "'1'"))) {
1081 anyseq_nets
.insert(net
);
1082 any_all_nets
.insert(net
);
1084 else if (anyconst_attr
!= nullptr && (!strcmp(anyconst_attr
, "1") || !strcmp(anyconst_attr
, "'1'"))) {
1085 anyconst_nets
.insert(net
);
1086 any_all_nets
.insert(net
);
1088 else if (anyseq_attr
!= nullptr && (!strcmp(anyseq_attr
, "1") || !strcmp(anyseq_attr
, "'1'"))) {
1089 anyseq_nets
.insert(net
);
1090 any_all_nets
.insert(net
);
1092 else if (allconst_attr
!= nullptr && (!strcmp(allconst_attr
, "1") || !strcmp(allconst_attr
, "'1'"))) {
1093 allconst_nets
.insert(net
);
1094 any_all_nets
.insert(net
);
1096 else if (allseq_attr
!= nullptr && (!strcmp(allseq_attr
, "1") || !strcmp(allseq_attr
, "'1'"))) {
1097 allseq_nets
.insert(net
);
1098 any_all_nets
.insert(net
);
1101 if (net_map
.count(net
)) {
1102 if (verific_verbose
)
1103 log(" skipping net %s.\n", net
->Name());
1110 RTLIL::IdString wire_name
= module
->uniquify(mode_names
|| net
->IsUserDeclared() ? RTLIL::escape_id(net
->Name()) : new_verific_id(net
));
1112 if (verific_verbose
)
1113 log(" importing net %s as %s.\n", net
->Name(), log_id(wire_name
));
1115 RTLIL::Wire
*wire
= module
->addWire(wire_name
);
1116 import_attributes(wire
->attributes
, net
, nl
);
1118 net_map
[net
] = wire
;
1121 FOREACH_NETBUS_OF_NETLIST(nl
, mi
, netbus
)
1123 bool found_new_net
= false;
1124 for (int i
= netbus
->LeftIndex();; i
+= netbus
->IsUp() ? +1 : -1) {
1125 net
= netbus
->ElementAtIndex(i
);
1126 if (net_map
.count(net
) == 0)
1127 found_new_net
= true;
1128 if (i
== netbus
->RightIndex())
1134 RTLIL::IdString wire_name
= module
->uniquify(mode_names
|| netbus
->IsUserDeclared() ? RTLIL::escape_id(netbus
->Name()) : new_verific_id(netbus
));
1136 if (verific_verbose
)
1137 log(" importing netbus %s as %s.\n", netbus
->Name(), log_id(wire_name
));
1139 RTLIL::Wire
*wire
= module
->addWire(wire_name
, netbus
->Size());
1140 wire
->start_offset
= min(netbus
->LeftIndex(), netbus
->RightIndex());
1142 FOREACH_NET_OF_NETBUS(netbus
, mibus
, net
) {
1144 import_attributes(wire
->attributes
, net
, nl
);
1148 RTLIL::Const initval
= Const(State::Sx
, GetSize(wire
));
1149 bool initval_valid
= false;
1151 for (int i
= netbus
->LeftIndex();; i
+= netbus
->IsUp() ? +1 : -1)
1153 if (netbus
->ElementAtIndex(i
))
1155 int bitidx
= i
- wire
->start_offset
;
1156 net
= netbus
->ElementAtIndex(i
);
1157 RTLIL::SigBit
bit(wire
, bitidx
);
1159 if (init_nets
.count(net
)) {
1160 if (init_nets
.at(net
) == '0')
1161 initval
.bits
.at(bitidx
) = State::S0
;
1162 if (init_nets
.at(net
) == '1')
1163 initval
.bits
.at(bitidx
) = State::S1
;
1164 initval_valid
= true;
1165 init_nets
.erase(net
);
1168 if (net_map
.count(net
) == 0)
1171 module
->connect(bit
, net_map_at(net
));
1174 if (i
== netbus
->RightIndex())
1179 wire
->attributes
[ID::init
] = initval
;
1183 if (verific_verbose
)
1184 log(" skipping netbus %s.\n", netbus
->Name());
1187 SigSpec anyconst_sig
;
1189 SigSpec allconst_sig
;
1192 for (int i
= netbus
->RightIndex();; i
+= netbus
->IsUp() ? -1 : +1) {
1193 net
= netbus
->ElementAtIndex(i
);
1194 if (net
!= nullptr && anyconst_nets
.count(net
)) {
1195 anyconst_sig
.append(net_map_at(net
));
1196 anyconst_nets
.erase(net
);
1198 if (net
!= nullptr && anyseq_nets
.count(net
)) {
1199 anyseq_sig
.append(net_map_at(net
));
1200 anyseq_nets
.erase(net
);
1202 if (net
!= nullptr && allconst_nets
.count(net
)) {
1203 allconst_sig
.append(net_map_at(net
));
1204 allconst_nets
.erase(net
);
1206 if (net
!= nullptr && allseq_nets
.count(net
)) {
1207 allseq_sig
.append(net_map_at(net
));
1208 allseq_nets
.erase(net
);
1210 if (i
== netbus
->LeftIndex())
1214 if (GetSize(anyconst_sig
))
1215 module
->connect(anyconst_sig
, module
->Anyconst(new_verific_id(netbus
), GetSize(anyconst_sig
)));
1217 if (GetSize(anyseq_sig
))
1218 module
->connect(anyseq_sig
, module
->Anyseq(new_verific_id(netbus
), GetSize(anyseq_sig
)));
1220 if (GetSize(allconst_sig
))
1221 module
->connect(allconst_sig
, module
->Allconst(new_verific_id(netbus
), GetSize(allconst_sig
)));
1223 if (GetSize(allseq_sig
))
1224 module
->connect(allseq_sig
, module
->Allseq(new_verific_id(netbus
), GetSize(allseq_sig
)));
1227 for (auto it
: init_nets
)
1230 SigBit bit
= net_map_at(it
.first
);
1231 log_assert(bit
.wire
);
1233 if (bit
.wire
->attributes
.count(ID::init
))
1234 initval
= bit
.wire
->attributes
.at(ID::init
);
1236 while (GetSize(initval
) < GetSize(bit
.wire
))
1237 initval
.bits
.push_back(State::Sx
);
1239 if (it
.second
== '0')
1240 initval
.bits
.at(bit
.offset
) = State::S0
;
1241 if (it
.second
== '1')
1242 initval
.bits
.at(bit
.offset
) = State::S1
;
1244 bit
.wire
->attributes
[ID::init
] = initval
;
1247 for (auto net
: anyconst_nets
)
1248 module
->connect(net_map_at(net
), module
->Anyconst(new_verific_id(net
)));
1250 for (auto net
: anyseq_nets
)
1251 module
->connect(net_map_at(net
), module
->Anyseq(new_verific_id(net
)));
1253 pool
<Instance
*, hash_ptr_ops
> sva_asserts
;
1254 pool
<Instance
*, hash_ptr_ops
> sva_assumes
;
1255 pool
<Instance
*, hash_ptr_ops
> sva_covers
;
1256 pool
<Instance
*, hash_ptr_ops
> sva_triggers
;
1258 pool
<RTLIL::Cell
*> past_ffs
;
1260 FOREACH_INSTANCE_OF_NETLIST(nl
, mi
, inst
)
1262 RTLIL::IdString inst_name
= module
->uniquify(mode_names
|| inst
->IsUserDeclared() ? RTLIL::escape_id(inst
->Name()) : new_verific_id(inst
));
1264 if (verific_verbose
)
1265 log(" importing cell %s (%s) as %s.\n", inst
->Name(), inst
->View()->Owner()->Name(), log_id(inst_name
));
1268 goto import_verific_cells
;
1270 if (inst
->Type() == PRIM_PWR
) {
1271 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::S1
);
1275 if (inst
->Type() == PRIM_GND
) {
1276 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::S0
);
1280 if (inst
->Type() == PRIM_BUF
) {
1281 auto outnet
= inst
->GetOutput();
1282 if (!any_all_nets
.count(outnet
))
1283 module
->addBufGate(inst_name
, net_map_at(inst
->GetInput()), net_map_at(outnet
));
1287 if (inst
->Type() == PRIM_X
) {
1288 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::Sx
);
1292 if (inst
->Type() == PRIM_Z
) {
1293 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::Sz
);
1297 if (inst
->Type() == OPER_READ_PORT
)
1299 RTLIL::Memory
*memory
= module
->memories
.at(RTLIL::escape_id(inst
->GetInput()->Name()), nullptr);
1301 log_error("Memory net '%s' missing, possibly no driver, use verific -flatten.\n", inst
->GetInput()->Name());
1303 int numchunks
= int(inst
->OutputSize()) / memory
->width
;
1304 int chunksbits
= ceil_log2(numchunks
);
1306 for (int i
= 0; i
< numchunks
; i
++)
1308 RTLIL::SigSpec addr
= {operatorInput1(inst
), RTLIL::Const(i
, chunksbits
)};
1309 RTLIL::SigSpec data
= operatorOutput(inst
).extract(i
* memory
->width
, memory
->width
);
1311 RTLIL::Cell
*cell
= module
->addCell(numchunks
== 1 ? inst_name
:
1312 RTLIL::IdString(stringf("%s_%d", inst_name
.c_str(), i
)), ID($memrd
));
1313 cell
->parameters
[ID::MEMID
] = memory
->name
.str();
1314 cell
->parameters
[ID::CLK_ENABLE
] = false;
1315 cell
->parameters
[ID::CLK_POLARITY
] = true;
1316 cell
->parameters
[ID::TRANSPARENT
] = false;
1317 cell
->parameters
[ID::ABITS
] = GetSize(addr
);
1318 cell
->parameters
[ID::WIDTH
] = GetSize(data
);
1319 cell
->setPort(ID::CLK
, RTLIL::State::Sx
);
1320 cell
->setPort(ID::EN
, RTLIL::State::Sx
);
1321 cell
->setPort(ID::ADDR
, addr
);
1322 cell
->setPort(ID::DATA
, data
);
1327 if (inst
->Type() == OPER_WRITE_PORT
|| inst
->Type() == OPER_CLOCKED_WRITE_PORT
)
1329 RTLIL::Memory
*memory
= module
->memories
.at(RTLIL::escape_id(inst
->GetOutput()->Name()), nullptr);
1331 log_error("Memory net '%s' missing, possibly no driver, use verific -flatten.\n", inst
->GetInput()->Name());
1332 int numchunks
= int(inst
->Input2Size()) / memory
->width
;
1333 int chunksbits
= ceil_log2(numchunks
);
1335 for (int i
= 0; i
< numchunks
; i
++)
1337 RTLIL::SigSpec addr
= {operatorInput1(inst
), RTLIL::Const(i
, chunksbits
)};
1338 RTLIL::SigSpec data
= operatorInput2(inst
).extract(i
* memory
->width
, memory
->width
);
1340 RTLIL::Cell
*cell
= module
->addCell(numchunks
== 1 ? inst_name
:
1341 RTLIL::IdString(stringf("%s_%d", inst_name
.c_str(), i
)), ID($memwr
));
1342 cell
->parameters
[ID::MEMID
] = memory
->name
.str();
1343 cell
->parameters
[ID::CLK_ENABLE
] = false;
1344 cell
->parameters
[ID::CLK_POLARITY
] = true;
1345 cell
->parameters
[ID::PRIORITY
] = 0;
1346 cell
->parameters
[ID::ABITS
] = GetSize(addr
);
1347 cell
->parameters
[ID::WIDTH
] = GetSize(data
);
1348 cell
->setPort(ID::EN
, RTLIL::SigSpec(net_map_at(inst
->GetControl())).repeat(GetSize(data
)));
1349 cell
->setPort(ID::CLK
, RTLIL::State::S0
);
1350 cell
->setPort(ID::ADDR
, addr
);
1351 cell
->setPort(ID::DATA
, data
);
1353 if (inst
->Type() == OPER_CLOCKED_WRITE_PORT
) {
1354 cell
->parameters
[ID::CLK_ENABLE
] = true;
1355 cell
->setPort(ID::CLK
, net_map_at(inst
->GetClock()));
1362 if (import_netlist_instance_cells(inst
, inst_name
))
1364 if (inst
->IsOperator() && !verific_sva_prims
.count(inst
->Type()))
1365 log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst
->View()->Owner()->Name());
1367 if (import_netlist_instance_gates(inst
, inst_name
))
1371 if (inst
->Type() == PRIM_SVA_ASSERT
|| inst
->Type() == PRIM_SVA_IMMEDIATE_ASSERT
)
1372 sva_asserts
.insert(inst
);
1374 if (inst
->Type() == PRIM_SVA_ASSUME
|| inst
->Type() == PRIM_SVA_IMMEDIATE_ASSUME
|| inst
->Type() == PRIM_SVA_RESTRICT
)
1375 sva_assumes
.insert(inst
);
1377 if (inst
->Type() == PRIM_SVA_COVER
|| inst
->Type() == PRIM_SVA_IMMEDIATE_COVER
)
1378 sva_covers
.insert(inst
);
1380 if (inst
->Type() == PRIM_SVA_TRIGGERED
)
1381 sva_triggers
.insert(inst
);
1383 if (inst
->Type() == OPER_SVA_STABLE
)
1385 VerificClocking
clocking(this, inst
->GetInput2Bit(0));
1386 log_assert(clocking
.disable_sig
== State::S0
);
1387 log_assert(clocking
.body_net
== nullptr);
1389 log_assert(inst
->Input1Size() == inst
->OutputSize());
1391 SigSpec sig_d
, sig_q
, sig_o
;
1392 sig_q
= module
->addWire(new_verific_id(inst
), inst
->Input1Size());
1394 for (int i
= int(inst
->Input1Size())-1; i
>= 0; i
--){
1395 sig_d
.append(net_map_at(inst
->GetInput1Bit(i
)));
1396 sig_o
.append(net_map_at(inst
->GetOutputBit(i
)));
1399 if (verific_verbose
) {
1400 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1401 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1402 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1403 log_signal(sig_d
), log_signal(sig_q
), log_signal(sig_o
));
1406 clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
);
1407 module
->addXnor(new_verific_id(inst
), sig_d
, sig_q
, sig_o
);
1413 if (inst
->Type() == PRIM_SVA_STABLE
)
1415 VerificClocking
clocking(this, inst
->GetInput2());
1416 log_assert(clocking
.disable_sig
== State::S0
);
1417 log_assert(clocking
.body_net
== nullptr);
1419 SigSpec sig_d
= net_map_at(inst
->GetInput1());
1420 SigSpec sig_o
= net_map_at(inst
->GetOutput());
1421 SigSpec sig_q
= module
->addWire(new_verific_id(inst
));
1423 if (verific_verbose
) {
1424 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1425 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1426 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1427 log_signal(sig_d
), log_signal(sig_q
), log_signal(sig_o
));
1430 clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
);
1431 module
->addXnor(new_verific_id(inst
), sig_d
, sig_q
, sig_o
);
1437 if (inst
->Type() == PRIM_SVA_PAST
)
1439 VerificClocking
clocking(this, inst
->GetInput2());
1440 log_assert(clocking
.disable_sig
== State::S0
);
1441 log_assert(clocking
.body_net
== nullptr);
1443 SigBit sig_d
= net_map_at(inst
->GetInput1());
1444 SigBit sig_q
= net_map_at(inst
->GetOutput());
1446 if (verific_verbose
)
1447 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1448 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1450 past_ffs
.insert(clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
));
1456 if ((inst
->Type() == PRIM_SVA_ROSE
|| inst
->Type() == PRIM_SVA_FELL
))
1458 VerificClocking
clocking(this, inst
->GetInput2());
1459 log_assert(clocking
.disable_sig
== State::S0
);
1460 log_assert(clocking
.body_net
== nullptr);
1462 SigBit sig_d
= net_map_at(inst
->GetInput1());
1463 SigBit sig_o
= net_map_at(inst
->GetOutput());
1464 SigBit sig_q
= module
->addWire(new_verific_id(inst
));
1466 if (verific_verbose
)
1467 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1468 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1470 clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
);
1471 module
->addEq(new_verific_id(inst
), {sig_q
, sig_d
}, Const(inst
->Type() == PRIM_SVA_ROSE
? 1 : 2, 2), sig_o
);
1477 #ifdef YOSYSHQ_VERIFIC_INITSTATE
1478 if (inst
->Type() == PRIM_YOSYSHQ_INITSTATE
)
1480 SigBit initstate
= module
->Initstate(new_verific_id(inst
));
1481 SigBit sig_o
= net_map_at(inst
->GetOutput());
1482 module
->connect(sig_o
, initstate
);
1488 if (!mode_keep
&& verific_sva_prims
.count(inst
->Type())) {
1489 if (verific_verbose
)
1490 log(" skipping SVA cell in non k-mode\n");
1494 if (inst
->Type() == PRIM_HDL_ASSERTION
)
1496 SigBit cond
= net_map_at(inst
->GetInput());
1498 if (verific_verbose
)
1499 log(" assert condition %s.\n", log_signal(cond
));
1501 const char *assume_attr
= nullptr; // inst->GetAttValue("assume");
1503 Cell
*cell
= nullptr;
1504 if (assume_attr
!= nullptr && !strcmp(assume_attr
, "1"))
1505 cell
= module
->addAssume(new_verific_id(inst
), cond
, State::S1
);
1507 cell
= module
->addAssert(new_verific_id(inst
), cond
, State::S1
);
1509 import_attributes(cell
->attributes
, inst
);
1513 if (inst
->IsPrimitive())
1516 log_error("Unsupported Verific primitive %s of type %s\n", inst
->Name(), inst
->View()->Owner()->Name());
1518 if (!verific_sva_prims
.count(inst
->Type()))
1519 log_warning("Unsupported Verific primitive %s of type %s\n", inst
->Name(), inst
->View()->Owner()->Name());
1522 import_verific_cells
:
1523 nl_todo
.insert(inst
->View());
1525 std::string inst_type
= inst
->View()->Owner()->Name();
1527 if (inst
->View()->IsOperator() || inst
->View()->IsPrimitive()) {
1528 inst_type
= "$verific$" + inst_type
;
1530 if (*inst
->View()->Name()) {
1532 inst_type
+= inst
->View()->Name();
1535 inst_type
= "\\" + sha1_if_contain_spaces(inst_type
);
1538 RTLIL::Cell
*cell
= module
->addCell(inst_name
, inst_type
);
1540 if (inst
->IsPrimitive() && mode_keep
)
1541 cell
->attributes
[ID::keep
] = 1;
1543 dict
<IdString
, vector
<SigBit
>> cell_port_conns
;
1545 if (verific_verbose
)
1546 log(" ports in verific db:\n");
1548 FOREACH_PORTREF_OF_INST(inst
, mi2
, pr
) {
1549 if (verific_verbose
)
1550 log(" .%s(%s)\n", pr
->GetPort()->Name(), pr
->GetNet()->Name());
1551 const char *port_name
= pr
->GetPort()->Name();
1552 int port_offset
= 0;
1553 if (pr
->GetPort()->Bus()) {
1554 port_name
= pr
->GetPort()->Bus()->Name();
1555 port_offset
= pr
->GetPort()->Bus()->IndexOf(pr
->GetPort()) -
1556 min(pr
->GetPort()->Bus()->LeftIndex(), pr
->GetPort()->Bus()->RightIndex());
1558 IdString port_name_id
= RTLIL::escape_id(port_name
);
1559 auto &sigvec
= cell_port_conns
[port_name_id
];
1560 if (GetSize(sigvec
) <= port_offset
) {
1561 SigSpec zwires
= module
->addWire(new_verific_id(inst
), port_offset
+1-GetSize(sigvec
));
1562 for (auto bit
: zwires
)
1563 sigvec
.push_back(bit
);
1565 sigvec
[port_offset
] = net_map_at(pr
->GetNet());
1568 if (verific_verbose
)
1569 log(" ports in yosys db:\n");
1571 for (auto &it
: cell_port_conns
) {
1572 if (verific_verbose
)
1573 log(" .%s(%s)\n", log_id(it
.first
), log_signal(it
.second
));
1574 cell
->setPort(it
.first
, it
.second
);
1580 for (auto inst
: sva_asserts
) {
1582 verific_import_sva_cover(this, inst
);
1583 verific_import_sva_assert(this, inst
);
1586 for (auto inst
: sva_assumes
)
1587 verific_import_sva_assume(this, inst
);
1589 for (auto inst
: sva_covers
)
1590 verific_import_sva_cover(this, inst
);
1592 for (auto inst
: sva_triggers
)
1593 verific_import_sva_trigger(this, inst
);
1595 merge_past_ffs(past_ffs
);
1600 pool
<SigBit
> non_ff_bits
;
1603 ff_types
.setup_internals_ff();
1604 ff_types
.setup_stdcells_mem();
1606 for (auto cell
: module
->cells())
1608 if (ff_types
.cell_known(cell
->type
))
1611 for (auto conn
: cell
->connections())
1613 if (!cell
->output(conn
.first
))
1616 for (auto bit
: conn
.second
)
1617 if (bit
.wire
!= nullptr)
1618 non_ff_bits
.insert(bit
);
1622 for (auto wire
: module
->wires())
1624 if (!wire
->attributes
.count(ID::init
))
1627 Const
&initval
= wire
->attributes
.at(ID::init
);
1628 for (int i
= 0; i
< GetSize(initval
); i
++)
1630 if (initval
[i
] != State::S0
&& initval
[i
] != State::S1
)
1633 if (non_ff_bits
.count(SigBit(wire
, i
)))
1634 initval
[i
] = State::Sx
;
1637 if (initval
.is_fully_undef())
1638 wire
->attributes
.erase(ID::init
);
1643 // ==================================================================
1645 VerificClocking::VerificClocking(VerificImporter
*importer
, Net
*net
, bool sva_at_only
)
1647 module
= importer
->module
;
1649 log_assert(importer
!= nullptr);
1650 log_assert(net
!= nullptr);
1652 Instance
*inst
= net
->Driver();
1654 if (inst
!= nullptr && inst
->Type() == PRIM_SVA_AT
)
1656 net
= inst
->GetInput1();
1657 body_net
= inst
->GetInput2();
1659 inst
= net
->Driver();
1661 Instance
*body_inst
= body_net
->Driver();
1662 if (body_inst
!= nullptr && body_inst
->Type() == PRIM_SVA_DISABLE_IFF
) {
1663 disable_net
= body_inst
->GetInput1();
1664 disable_sig
= importer
->net_map_at(disable_net
);
1665 body_net
= body_inst
->GetInput2();
1674 // Use while() instead of if() to work around VIPER #13453
1675 while (inst
!= nullptr && inst
->Type() == PRIM_SVA_POSEDGE
)
1677 net
= inst
->GetInput();
1678 inst
= net
->Driver();;
1681 if (inst
!= nullptr && inst
->Type() == PRIM_INV
)
1683 net
= inst
->GetInput();
1684 inst
= net
->Driver();;
1688 // Detect clock-enable circuit
1690 if (inst
== nullptr || inst
->Type() != PRIM_AND
)
1693 Net
*net_dlatch
= inst
->GetInput1();
1694 Instance
*inst_dlatch
= net_dlatch
->Driver();
1696 if (inst_dlatch
== nullptr || inst_dlatch
->Type() != PRIM_DLATCHRS
)
1699 if (!inst_dlatch
->GetSet()->IsGnd() || !inst_dlatch
->GetReset()->IsGnd())
1702 Net
*net_enable
= inst_dlatch
->GetInput();
1703 Net
*net_not_clock
= inst_dlatch
->GetControl();
1705 if (net_enable
== nullptr || net_not_clock
== nullptr)
1708 Instance
*inst_not_clock
= net_not_clock
->Driver();
1710 if (inst_not_clock
== nullptr || inst_not_clock
->Type() != PRIM_INV
)
1713 Net
*net_clock1
= inst_not_clock
->GetInput();
1714 Net
*net_clock2
= inst
->GetInput2();
1716 if (net_clock1
== nullptr || net_clock1
!= net_clock2
)
1719 enable_net
= net_enable
;
1720 enable_sig
= importer
->net_map_at(enable_net
);
1723 inst
= net
->Driver();;
1726 // Detect condition expression
1728 if (body_net
== nullptr)
1731 Instance
*inst_mux
= body_net
->Driver();
1733 if (inst_mux
== nullptr || inst_mux
->Type() != PRIM_MUX
)
1736 if (!inst_mux
->GetInput1()->IsPwr())
1739 Net
*sva_net
= inst_mux
->GetInput2();
1740 if (!verific_is_sva_net(importer
, sva_net
))
1744 cond_net
= inst_mux
->GetControl();
1748 clock_sig
= importer
->net_map_at(clock_net
);
1750 const char *gclk_attr
= clock_net
->GetAttValue("gclk");
1751 if (gclk_attr
!= nullptr && (!strcmp(gclk_attr
, "1") || !strcmp(gclk_attr
, "'1'")))
1755 Cell
*VerificClocking::addDff(IdString name
, SigSpec sig_d
, SigSpec sig_q
, Const init_value
)
1757 log_assert(GetSize(sig_d
) == GetSize(sig_q
));
1759 if (GetSize(init_value
) != 0) {
1760 log_assert(GetSize(sig_q
) == GetSize(init_value
));
1761 if (sig_q
.is_wire()) {
1762 sig_q
.as_wire()->attributes
[ID::init
] = init_value
;
1764 Wire
*w
= module
->addWire(NEW_ID
, GetSize(sig_q
));
1765 w
->attributes
[ID::init
] = init_value
;
1766 module
->connect(sig_q
, w
);
1771 if (enable_sig
!= State::S1
)
1772 sig_d
= module
->Mux(NEW_ID
, sig_q
, sig_d
, enable_sig
);
1774 if (disable_sig
!= State::S0
) {
1775 log_assert(gclk
== false);
1776 log_assert(GetSize(sig_q
) == GetSize(init_value
));
1777 return module
->addAdff(name
, clock_sig
, disable_sig
, sig_d
, sig_q
, init_value
, posedge
);
1781 return module
->addFf(name
, sig_d
, sig_q
);
1783 return module
->addDff(name
, clock_sig
, sig_d
, sig_q
, posedge
);
1786 Cell
*VerificClocking::addAdff(IdString name
, RTLIL::SigSpec sig_arst
, SigSpec sig_d
, SigSpec sig_q
, Const arst_value
)
1788 log_assert(gclk
== false);
1789 log_assert(disable_sig
== State::S0
);
1791 if (enable_sig
!= State::S1
)
1792 sig_d
= module
->Mux(NEW_ID
, sig_q
, sig_d
, enable_sig
);
1794 return module
->addAdff(name
, clock_sig
, sig_arst
, sig_d
, sig_q
, arst_value
, posedge
);
1797 Cell
*VerificClocking::addDffsr(IdString name
, RTLIL::SigSpec sig_set
, RTLIL::SigSpec sig_clr
, SigSpec sig_d
, SigSpec sig_q
)
1799 log_assert(gclk
== false);
1800 log_assert(disable_sig
== State::S0
);
1802 if (enable_sig
!= State::S1
)
1803 sig_d
= module
->Mux(NEW_ID
, sig_q
, sig_d
, enable_sig
);
1805 return module
->addDffsr(name
, clock_sig
, sig_set
, sig_clr
, sig_d
, sig_q
, posedge
);
1808 // ==================================================================
1810 struct VerificExtNets
1812 int portname_cnt
= 0;
1814 // a map from Net to the same Net one level up in the design hierarchy
1815 std::map
<Net
*, Net
*> net_level_up_drive_up
;
1816 std::map
<Net
*, Net
*> net_level_up_drive_down
;
1818 Net
*route_up(Net
*net
, bool drive_up
, Net
*final_net
= nullptr)
1820 auto &net_level_up
= drive_up
? net_level_up_drive_up
: net_level_up_drive_down
;
1822 if (net_level_up
.count(net
) == 0)
1824 Netlist
*nl
= net
->Owner();
1826 // Simply return if Netlist is not unique
1827 log_assert(nl
->NumOfRefs() == 1);
1829 Instance
*up_inst
= (Instance
*)nl
->GetReferences()->GetLast();
1830 Netlist
*up_nl
= up_inst
->Owner();
1833 string name
= stringf("___extnets_%d", portname_cnt
++);
1834 Port
*new_port
= new Port(name
.c_str(), drive_up
? DIR_OUT
: DIR_IN
);
1836 net
->Connect(new_port
);
1838 // create new Net in up Netlist
1839 Net
*new_net
= final_net
;
1840 if (new_net
== nullptr || new_net
->Owner() != up_nl
) {
1841 new_net
= new Net(name
.c_str());
1842 up_nl
->Add(new_net
);
1844 up_inst
->Connect(new_port
, new_net
);
1846 net_level_up
[net
] = new_net
;
1849 return net_level_up
.at(net
);
1852 Net
*route_up(Net
*net
, bool drive_up
, Netlist
*dest
, Net
*final_net
= nullptr)
1854 while (net
->Owner() != dest
)
1855 net
= route_up(net
, drive_up
, final_net
);
1856 if (final_net
!= nullptr)
1857 log_assert(net
== final_net
);
1861 Netlist
*find_common_ancestor(Netlist
*A
, Netlist
*B
)
1863 std::set
<Netlist
*> ancestors_of_A
;
1865 Netlist
*cursor
= A
;
1867 ancestors_of_A
.insert(cursor
);
1868 if (cursor
->NumOfRefs() != 1)
1870 cursor
= ((Instance
*)cursor
->GetReferences()->GetLast())->Owner();
1875 if (ancestors_of_A
.count(cursor
))
1877 if (cursor
->NumOfRefs() != 1)
1879 cursor
= ((Instance
*)cursor
->GetReferences()->GetLast())->Owner();
1882 log_error("No common ancestor found between %s and %s.\n", get_full_netlist_name(A
).c_str(), get_full_netlist_name(B
).c_str());
1885 void run(Netlist
*nl
)
1891 vector
<tuple
<Instance
*, Port
*, Net
*>> todo_connect
;
1893 FOREACH_INSTANCE_OF_NETLIST(nl
, mi
, inst
)
1896 FOREACH_INSTANCE_OF_NETLIST(nl
, mi
, inst
)
1897 FOREACH_PORTREF_OF_INST(inst
, mi2
, pr
)
1899 Port
*port
= pr
->GetPort();
1900 Net
*net
= pr
->GetNet();
1902 if (!net
->IsExternalTo(nl
))
1905 if (verific_verbose
)
1906 log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl
).c_str(), inst
->Name(), port
->Name());
1908 Netlist
*ext_nl
= net
->Owner();
1910 if (verific_verbose
)
1911 log(" external net owner: %s\n", get_full_netlist_name(ext_nl
).c_str());
1913 Netlist
*ca_nl
= find_common_ancestor(nl
, ext_nl
);
1915 if (verific_verbose
)
1916 log(" common ancestor: %s\n", get_full_netlist_name(ca_nl
).c_str());
1918 Net
*ca_net
= route_up(net
, !port
->IsOutput(), ca_nl
);
1919 Net
*new_net
= ca_net
;
1923 if (verific_verbose
)
1924 log(" net in common ancestor: %s\n", ca_net
->Name());
1926 string name
= stringf("___extnets_%d", portname_cnt
++);
1927 new_net
= new Net(name
.c_str());
1930 Net
*n
= route_up(new_net
, port
->IsOutput(), ca_nl
, ca_net
);
1931 log_assert(n
== ca_net
);
1934 if (verific_verbose
)
1935 log(" new local net: %s\n", new_net
->Name());
1937 log_assert(!new_net
->IsExternalTo(nl
));
1938 todo_connect
.push_back(tuple
<Instance
*, Port
*, Net
*>(inst
, port
, new_net
));
1941 for (auto it
: todo_connect
) {
1942 get
<0>(it
)->Disconnect(get
<1>(it
));
1943 get
<0>(it
)->Connect(get
<1>(it
), get
<2>(it
));
1948 void verific_import(Design
*design
, const std::map
<std::string
,std::string
> ¶meters
, std::string top
)
1950 verific_sva_fsm_limit
= 16;
1952 std::set
<Netlist
*> nl_todo
, nl_done
;
1954 VhdlLibrary
*vhdl_lib
= vhdl_file::GetLibrary("work", 1);
1955 VeriLibrary
*veri_lib
= veri_file::GetLibrary("work", 1);
1956 Array
*netlists
= NULL
;
1957 Array veri_libs
, vhdl_libs
;
1958 if (vhdl_lib
) vhdl_libs
.InsertLast(vhdl_lib
);
1959 if (veri_lib
) veri_libs
.InsertLast(veri_lib
);
1961 Map
verific_params(STRING_HASH
);
1962 for (const auto &i
: parameters
)
1963 verific_params
.Insert(i
.first
.c_str(), i
.second
.c_str());
1965 #ifdef YOSYSHQ_VERIFIC_INITSTATE
1966 InitialAssertionRewriter rw
;
1967 rw
.RegisterCallBack();
1970 netlists
= hier_tree::ElaborateAll(&veri_libs
, &vhdl_libs
, &verific_params
);
1973 Array veri_modules
, vhdl_units
;
1976 VeriModule
*veri_module
= veri_lib
->GetModule(top
.c_str(), 1);
1978 veri_modules
.InsertLast(veri_module
);
1981 // Also elaborate all root modules since they may contain bind statements
1983 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib
, mi
, veri_module
) {
1984 if (!veri_module
->IsRootModule()) continue;
1985 veri_modules
.InsertLast(veri_module
);
1990 VhdlDesignUnit
*vhdl_unit
= vhdl_lib
->GetPrimUnit(top
.c_str());
1992 vhdl_units
.InsertLast(vhdl_unit
);
1995 netlists
= hier_tree::Elaborate(&veri_modules
, &vhdl_units
, &verific_params
);
2001 FOREACH_ARRAY_ITEM(netlists
, i
, nl
) {
2002 if (top
.empty() && nl
->CellBaseName() != top
)
2004 nl
->AddAtt(new Att(" \\top", NULL
));
2010 if (!verific_error_msg
.empty())
2011 log_error("%s\n", verific_error_msg
.c_str());
2013 for (auto nl
: nl_todo
)
2014 nl
->ChangePortBusStructures(1 /* hierarchical */);
2016 VerificExtNets worker
;
2017 for (auto nl
: nl_todo
)
2020 while (!nl_todo
.empty()) {
2021 Netlist
*nl
= *nl_todo
.begin();
2022 if (nl_done
.count(nl
) == 0) {
2023 VerificImporter
importer(false, false, false, false, false, false, false);
2024 importer
.import_netlist(design
, nl
, nl_todo
, nl
->Owner()->Name() == top
);
2033 verific_incdirs
.clear();
2034 verific_libdirs
.clear();
2035 verific_import_pending
= false;
2037 if (!verific_error_msg
.empty())
2038 log_error("%s\n", verific_error_msg
.c_str());
2042 #endif /* YOSYS_ENABLE_VERIFIC */
2044 PRIVATE_NAMESPACE_BEGIN
2046 #ifdef YOSYS_ENABLE_VERIFIC
2047 bool check_noverific_env()
2049 const char *e
= getenv("YOSYS_NOVERIFIC");
2058 struct VerificPass
: public Pass
{
2059 VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
2060 void help() override
2062 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2064 log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
2066 log("Load the specified Verilog/SystemVerilog files into Verific.\n");
2068 log("All files specified in one call to this command are one compilation unit.\n");
2069 log("Files passed to different calls to this command are treated as belonging to\n");
2070 log("different compilation units.\n");
2072 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2073 log("the language version (and before file names) to set additional verilog defines.\n");
2074 log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
2077 log(" verific -formal <verilog-file>..\n");
2079 log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
2082 log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2084 log("Load the specified VHDL files into Verific.\n");
2087 log(" verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>\n");
2089 log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
2090 log("(default library when -work is not present: \"work\")\n");
2093 log(" verific [-L <libname>] {-sv|-vhdl|...} <hdl-file>\n");
2095 log("Look up external definitions in the specified library.\n");
2096 log("(-L may be used more than once)\n");
2099 log(" verific -vlog-incdir <directory>..\n");
2101 log("Add Verilog include directories.\n");
2104 log(" verific -vlog-libdir <directory>..\n");
2106 log("Add Verilog library directories. Verific will search in this directories to\n");
2107 log("find undefined modules.\n");
2110 log(" verific -vlog-define <macro>[=<value>]..\n");
2112 log("Add Verilog defines.\n");
2115 log(" verific -vlog-undef <macro>..\n");
2117 log("Remove Verilog defines previously set with -vlog-define.\n");
2120 log(" verific -set-error <msg_id>..\n");
2121 log(" verific -set-warning <msg_id>..\n");
2122 log(" verific -set-info <msg_id>..\n");
2123 log(" verific -set-ignore <msg_id>..\n");
2125 log("Set message severity. <msg_id> is the string in square brackets when a message\n");
2126 log("is printed, such as VERI-1209.\n");
2129 log(" verific -import [options] <top-module>..\n");
2131 log("Elaborate the design for the specified top modules, import to Yosys and\n");
2132 log("reset the internal state of Verific.\n");
2134 log("Import options:\n");
2137 log(" Elaborate all modules, not just the hierarchy below the given top\n");
2138 log(" modules. With this option the list of modules to import is optional.\n");
2141 log(" Create a gate-level netlist.\n");
2144 log(" Flatten the design in Verific before importing.\n");
2147 log(" Resolve references to external nets by adding module ports as needed.\n");
2149 log(" -autocover\n");
2150 log(" Generate automatic cover statements for all asserts\n");
2152 log(" -fullinit\n");
2153 log(" Keep all register initializations, even those for non-FF registers.\n");
2155 log(" -chparam name value \n");
2156 log(" Elaborate the specified top modules (all modules when -all given) using\n");
2157 log(" this parameter value. Modules on which this parameter does not exist will\n");
2158 log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
2159 log(" can be specified multiple times to override multiple parameters.\n");
2160 log(" String values must be passed in double quotes (\").\n");
2163 log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
2165 log("The following additional import options are useful for debugging the Verific\n");
2166 log("bindings (for Yosys and/or Verific developers):\n");
2169 log(" Keep going after an unsupported verific primitive is found. The\n");
2170 log(" unsupported primitive is added as blockbox module to the design.\n");
2171 log(" This will also add all SVA related cells to the design parallel to\n");
2172 log(" the checker logic inferred by it.\n");
2175 log(" Import Verific netlist as-is without translating to Yosys cell types. \n");
2178 log(" Ignore SVA properties, do not infer checker logic.\n");
2181 log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
2184 log(" Keep all Verific names on instances and nets. By default only\n");
2185 log(" user-declared names are preserved.\n");
2187 log(" -d <dump_file>\n");
2188 log(" Dump the Verific netlist as a verilog file.\n");
2191 log(" verific [-work <libname>] -pp [options] <filename> [<module>]..\n");
2193 log("Pretty print design (or just module) to the specified file from the\n");
2194 log("specified library. (default library when -work is not present: \"work\")\n");
2196 log("Pretty print options:\n");
2199 log(" Save output for Verilog/SystemVerilog design modules (default).\n");
2202 log(" Save output for VHDL design units.\n");
2205 log(" verific -app <application>..\n");
2207 log("Execute YosysHQ formal application on loaded Verilog files.\n");
2209 log("Application options:\n");
2211 log(" -module <module>\n");
2212 log(" Run formal application only on specified module.\n");
2214 log(" -blacklist <filename[:lineno]>\n");
2215 log(" Do not run application on modules from files that match the filename\n");
2216 log(" or filename and line number if provided in such format.\n");
2217 log(" Parameter can also contain comma separated list of file locations.\n");
2219 log(" -blfile <file>\n");
2220 log(" Do not run application on locations specified in file, they can represent filename\n");
2221 log(" or filename and location in file.\n");
2223 log("Applications:\n");
2225 #if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_FORMALAPPS)
2226 VerificFormalApplications vfa
;
2227 log("%s\n",vfa
.GetHelp().c_str());
2229 log(" WARNING: Applications only available in commercial build.\n");
2234 log(" verific -template <name> <top_module>..\n");
2236 log("Generate template for specified top module of loaded design.\n");
2238 log("Template options:\n");
2241 log(" Specifies output file for generated template, by default output is stdout\n");
2243 log(" -chparam name value \n");
2244 log(" Generate template using this parameter value. Otherwise default parameter\n");
2245 log(" values will be used for templat generate functionality. This option\n");
2246 log(" can be specified multiple times to override multiple parameters.\n");
2247 log(" String values must be passed in double quotes (\").\n");
2249 log("Templates:\n");
2251 #if defined(YOSYS_ENABLE_VERIFIC) && defined(YOSYSHQ_VERIFIC_TEMPLATES)
2252 VerificTemplateGenerator vfg
;
2253 log("%s\n",vfg
.GetHelp().c_str());
2255 log(" WARNING: Templates only available in commercial build.\n");
2258 log("Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n");
2259 log("https://www.yosyshq.com/\n");
2261 log("Contact office@yosyshq.com for free evaluation\n");
2262 log("binaries of YosysHQ Tabby CAD Suite.\n");
2265 #ifdef YOSYS_ENABLE_VERIFIC
2266 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) override
2268 static bool set_verific_global_flags
= true;
2270 if (check_noverific_env())
2271 log_cmd_error("This version of Yosys is built without Verific support.\n"
2273 "Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n"
2274 "https://www.yosyshq.com/\n"
2276 "Contact office@yosyshq.com for free evaluation\n"
2277 "binaries of YosysHQ Tabby CAD Suite.\n");
2279 log_header(design
, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
2281 if (set_verific_global_flags
)
2283 Message::SetConsoleOutput(0);
2284 Message::RegisterCallBackMsg(msg_func
);
2286 RuntimeFlags::SetVar("db_preserve_user_nets", 1);
2287 RuntimeFlags::SetVar("db_allow_external_nets", 1);
2288 RuntimeFlags::SetVar("db_infer_wide_operators", 1);
2290 RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
2291 RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
2293 RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
2294 RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
2296 RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
2297 RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
2299 RuntimeFlags::SetVar("veri_preserve_assignments", 1);
2300 RuntimeFlags::SetVar("vhdl_preserve_assignments", 1);
2302 RuntimeFlags::SetVar("veri_preserve_comments",1);
2303 //RuntimeFlags::SetVar("vhdl_preserve_comments",1);
2305 // Workaround for VIPER #13851
2306 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
2308 // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
2309 Message::SetMessageType("VERI-1063", VERIFIC_ERROR
);
2311 // https://github.com/YosysHQ/yosys/issues/1055
2312 RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
2314 #ifndef DB_PRESERVE_INITIAL_VALUE
2315 # warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
2318 set_verific_global_flags
= false;
2321 verific_verbose
= 0;
2322 verific_sva_fsm_limit
= 16;
2324 const char *release_str
= Message::ReleaseString();
2325 time_t release_time
= Message::ReleaseDate();
2326 char *release_tmstr
= ctime(&release_time
);
2328 if (release_str
== nullptr)
2329 release_str
= "(no release string)";
2331 for (char *p
= release_tmstr
; *p
; p
++)
2332 if (*p
== '\n') *p
= 0;
2334 log("Built with Verific %s, released at %s.\n", release_str
, release_tmstr
);
2337 std::string work
= "work";
2339 if (GetSize(args
) > argidx
&& (args
[argidx
] == "-set-error" || args
[argidx
] == "-set-warning" ||
2340 args
[argidx
] == "-set-info" || args
[argidx
] == "-set-ignore"))
2342 msg_type_t new_type
;
2344 if (args
[argidx
] == "-set-error")
2345 new_type
= VERIFIC_ERROR
;
2346 else if (args
[argidx
] == "-set-warning")
2347 new_type
= VERIFIC_WARNING
;
2348 else if (args
[argidx
] == "-set-info")
2349 new_type
= VERIFIC_INFO
;
2350 else if (args
[argidx
] == "-set-ignore")
2351 new_type
= VERIFIC_IGNORE
;
2355 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2356 Message::SetMessageType(args
[argidx
].c_str(), new_type
);
2361 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-incdir") {
2362 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2363 verific_incdirs
.push_back(args
[argidx
]);
2367 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-libdir") {
2368 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2369 verific_libdirs
.push_back(args
[argidx
]);
2373 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-define") {
2374 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2375 string name
= args
[argidx
];
2376 size_t equal
= name
.find('=');
2377 if (equal
!= std::string::npos
) {
2378 string value
= name
.substr(equal
+1);
2379 name
= name
.substr(0, equal
);
2380 veri_file::DefineCmdLineMacro(name
.c_str(), value
.c_str());
2382 veri_file::DefineCmdLineMacro(name
.c_str());
2388 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-undef") {
2389 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2390 string name
= args
[argidx
];
2391 veri_file::UndefineMacro(name
.c_str());
2396 veri_file::RemoveAllLOptions();
2397 for (; argidx
< GetSize(args
); argidx
++)
2399 if (args
[argidx
] == "-work" && argidx
+1 < GetSize(args
)) {
2400 work
= args
[++argidx
];
2403 if (args
[argidx
] == "-L" && argidx
+1 < GetSize(args
)) {
2404 veri_file::AddLOption(args
[++argidx
].c_str());
2410 if (GetSize(args
) > argidx
&& (args
[argidx
] == "-vlog95" || args
[argidx
] == "-vlog2k" || args
[argidx
] == "-sv2005" ||
2411 args
[argidx
] == "-sv2009" || args
[argidx
] == "-sv2012" || args
[argidx
] == "-sv" || args
[argidx
] == "-formal"))
2414 unsigned verilog_mode
;
2416 if (args
[argidx
] == "-vlog95")
2417 verilog_mode
= veri_file::VERILOG_95
;
2418 else if (args
[argidx
] == "-vlog2k")
2419 verilog_mode
= veri_file::VERILOG_2K
;
2420 else if (args
[argidx
] == "-sv2005")
2421 verilog_mode
= veri_file::SYSTEM_VERILOG_2005
;
2422 else if (args
[argidx
] == "-sv2009")
2423 verilog_mode
= veri_file::SYSTEM_VERILOG_2009
;
2424 else if (args
[argidx
] == "-sv2012" || args
[argidx
] == "-sv" || args
[argidx
] == "-formal")
2425 verilog_mode
= veri_file::SYSTEM_VERILOG
;
2429 veri_file::DefineMacro("VERIFIC");
2430 veri_file::DefineMacro(args
[argidx
] == "-formal" ? "FORMAL" : "SYNTHESIS");
2432 for (argidx
++; argidx
< GetSize(args
) && GetSize(args
[argidx
]) >= 2 && args
[argidx
].compare(0, 2, "-D") == 0; argidx
++) {
2433 std::string name
= args
[argidx
].substr(2);
2434 if (args
[argidx
] == "-D") {
2435 if (++argidx
>= GetSize(args
))
2437 name
= args
[argidx
];
2439 size_t equal
= name
.find('=');
2440 if (equal
!= std::string::npos
) {
2441 string value
= name
.substr(equal
+1);
2442 name
= name
.substr(0, equal
);
2443 veri_file::DefineMacro(name
.c_str(), value
.c_str());
2445 veri_file::DefineMacro(name
.c_str());
2449 for (auto &dir
: verific_incdirs
)
2450 veri_file::AddIncludeDir(dir
.c_str());
2451 for (auto &dir
: verific_libdirs
)
2452 veri_file::AddYDir(dir
.c_str());
2454 while (argidx
< GetSize(args
))
2455 file_names
.Insert(args
[argidx
++].c_str());
2457 if (!veri_file::AnalyzeMultipleFiles(&file_names
, verilog_mode
, work
.c_str(), veri_file::MFCU
)) {
2458 verific_error_msg
.clear();
2459 log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
2462 verific_import_pending
= true;
2466 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vhdl87") {
2467 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
2468 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2469 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_87
))
2470 log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args
[argidx
].c_str());
2471 verific_import_pending
= true;
2475 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vhdl93") {
2476 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2477 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2478 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_93
))
2479 log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args
[argidx
].c_str());
2480 verific_import_pending
= true;
2484 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vhdl2k") {
2485 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2486 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2487 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_2K
))
2488 log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args
[argidx
].c_str());
2489 verific_import_pending
= true;
2493 if (GetSize(args
) > argidx
&& (args
[argidx
] == "-vhdl2008" || args
[argidx
] == "-vhdl")) {
2494 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
2495 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2496 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_2008
))
2497 log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args
[argidx
].c_str());
2498 verific_import_pending
= true;
2502 #ifdef YOSYSHQ_VERIFIC_FORMALAPPS
2503 if (argidx
< GetSize(args
) && args
[argidx
] == "-app")
2505 if (!(argidx
+1 < GetSize(args
)))
2506 cmd_error(args
, argidx
, "No formal application specified.\n");
2508 VerificFormalApplications vfa
;
2509 auto apps
= vfa
.GetApps();
2510 std::string app
= args
[++argidx
];
2511 std::vector
<std::string
> blacklists
;
2512 if (apps
.find(app
) == apps
.end())
2513 log_cmd_error("Application '%s' does not exist.\n", app
.c_str());
2515 FormalApplication
*application
= apps
[app
];
2516 application
->setLogger([](std::string msg
) { log("%s",msg
.c_str()); } );
2517 VeriModule
*selected_module
= nullptr;
2519 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2521 if (application
->checkParams(args
, argidx
, error
)) {
2523 cmd_error(args
, argidx
, error
);
2527 if (args
[argidx
] == "-module" && argidx
< GetSize(args
)) {
2528 if (!(argidx
+1 < GetSize(args
)))
2529 cmd_error(args
, argidx
+1, "No module name specified.\n");
2530 std::string module
= args
[++argidx
];
2531 VeriLibrary
* veri_lib
= veri_file::GetLibrary(work
.c_str(), 1);
2532 selected_module
= veri_lib
? veri_lib
->GetModule(module
.c_str(), 1) : nullptr;
2533 if (!selected_module
) {
2534 log_error("Can't find module '%s'.\n", module
.c_str());
2538 if (args
[argidx
] == "-blacklist" && argidx
< GetSize(args
)) {
2539 if (!(argidx
+1 < GetSize(args
)))
2540 cmd_error(args
, argidx
+1, "No blacklist specified.\n");
2542 std::string line
= args
[++argidx
];
2544 while (!(p
= next_token(line
, ",\t\r\n ")).empty())
2545 blacklists
.push_back(p
);
2548 if (args
[argidx
] == "-blfile" && argidx
< GetSize(args
)) {
2549 if (!(argidx
+1 < GetSize(args
)))
2550 cmd_error(args
, argidx
+1, "No blacklist file specified.\n");
2551 std::string fn
= args
[++argidx
];
2552 std::ifstream
f(fn
);
2554 log_cmd_error("Can't open blacklist file '%s'!\n", fn
.c_str());
2557 while (std::getline(f
, line
)) {
2558 while (!(p
= next_token(line
, ",\t\r\n ")).empty())
2559 blacklists
.push_back(p
);
2565 if (argidx
< GetSize(args
))
2566 cmd_error(args
, argidx
, "unknown option/parameter");
2568 application
->setBlacklists(&blacklists
);
2569 application
->setSingleModuleMode(selected_module
!=nullptr);
2571 const char *err
= application
->validate();
2573 cmd_error(args
, argidx
, err
);
2576 VeriLibrary
*veri_lib
= veri_file::GetLibrary(work
.c_str(), 1);
2577 log("Running formal application '%s'.\n", app
.c_str());
2579 if (selected_module
) {
2581 if (!application
->execute(selected_module
, out
))
2582 log_error("%s", out
.c_str());
2585 VeriModule
*module
;
2586 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib
, mi
, module
) {
2588 if (!application
->execute(module
, out
)) {
2589 log_error("%s", out
.c_str());
2597 if (argidx
< GetSize(args
) && args
[argidx
] == "-pp")
2599 const char* filename
= nullptr;
2600 const char* module
= nullptr;
2601 bool mode_vhdl
= false;
2602 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2603 if (args
[argidx
] == "-vhdl") {
2607 if (args
[argidx
] == "-verilog") {
2612 if (args
[argidx
].compare(0, 1, "-") == 0) {
2613 cmd_error(args
, argidx
, "unknown option");
2618 filename
= args
[argidx
].c_str();
2622 log_cmd_error("Only one module can be specified.\n");
2623 module
= args
[argidx
].c_str();
2626 if (argidx
< GetSize(args
))
2627 cmd_error(args
, argidx
, "unknown option/parameter");
2630 log_cmd_error("Filname must be specified.\n");
2633 vhdl_file::PrettyPrint(filename
, module
, work
.c_str());
2635 veri_file::PrettyPrint(filename
, module
, work
.c_str());
2639 #ifdef YOSYSHQ_VERIFIC_TEMPLATES
2640 if (argidx
< GetSize(args
) && args
[argidx
] == "-template")
2642 if (!(argidx
+1 < GetSize(args
)))
2643 cmd_error(args
, argidx
+1, "No template type specified.\n");
2645 VerificTemplateGenerator vfg
;
2646 auto gens
= vfg
.GetGenerators();
2647 std::string app
= args
[++argidx
];
2648 if (gens
.find(app
) == gens
.end())
2649 log_cmd_error("Template generator '%s' does not exist.\n", app
.c_str());
2650 TemplateGenerator
*generator
= gens
[app
];
2651 if (!(argidx
+1 < GetSize(args
)))
2652 cmd_error(args
, argidx
+1, "No top module specified.\n");
2653 generator
->setLogger([](std::string msg
) { log("%s",msg
.c_str()); } );
2655 std::string module
= args
[++argidx
];
2656 VeriLibrary
* veri_lib
= veri_file::GetLibrary(work
.c_str(), 1);
2657 VeriModule
*veri_module
= veri_lib
? veri_lib
->GetModule(module
.c_str(), 1) : nullptr;
2659 log_error("Can't find module/unit '%s'.\n", module
.c_str());
2662 log("Template '%s' is running for module '%s'.\n", app
.c_str(),module
.c_str());
2664 Map
parameters(STRING_HASH
);
2665 const char *out_filename
= nullptr;
2667 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2669 if (generator
->checkParams(args
, argidx
, error
)) {
2671 cmd_error(args
, argidx
, error
);
2675 if (args
[argidx
] == "-chparam" && argidx
< GetSize(args
)) {
2676 if (!(argidx
+1 < GetSize(args
)))
2677 cmd_error(args
, argidx
+1, "No param name specified.\n");
2678 if (!(argidx
+2 < GetSize(args
)))
2679 cmd_error(args
, argidx
+2, "No param value specified.\n");
2681 const std::string
&key
= args
[++argidx
];
2682 const std::string
&value
= args
[++argidx
];
2683 unsigned new_insertion
= parameters
.Insert(key
.c_str(), value
.c_str(),
2684 1 /* force_overwrite */);
2686 log_warning_noprefix("-chparam %s already specified: overwriting.\n", key
.c_str());
2690 if (args
[argidx
] == "-out" && argidx
< GetSize(args
)) {
2691 if (!(argidx
+1 < GetSize(args
)))
2692 cmd_error(args
, argidx
+1, "No output file specified.\n");
2693 out_filename
= args
[++argidx
].c_str();
2699 if (argidx
< GetSize(args
))
2700 cmd_error(args
, argidx
, "unknown option/parameter");
2702 const char *err
= generator
->validate();
2704 cmd_error(args
, argidx
, err
);
2707 if (!generator
->generate(veri_module
, val
, ¶meters
))
2708 log_error("%s", val
.c_str());
2712 of
= fopen(out_filename
, "w");
2714 log_error("Can't open '%s' for writing: %s\n", out_filename
, strerror(errno
));
2715 log("Writing output to '%s'\n",out_filename
);
2717 fprintf(of
, "%s\n",val
.c_str());
2724 if (GetSize(args
) > argidx
&& args
[argidx
] == "-import")
2726 std::set
<Netlist
*> nl_todo
, nl_done
;
2727 bool mode_all
= false, mode_gates
= false, mode_keep
= false;
2728 bool mode_nosva
= false, mode_names
= false, mode_verific
= false;
2729 bool mode_autocover
= false, mode_fullinit
= false;
2730 bool flatten
= false, extnets
= false;
2732 Map
parameters(STRING_HASH
);
2734 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2735 if (args
[argidx
] == "-all") {
2739 if (args
[argidx
] == "-gates") {
2743 if (args
[argidx
] == "-flatten") {
2747 if (args
[argidx
] == "-extnets") {
2751 if (args
[argidx
] == "-k") {
2755 if (args
[argidx
] == "-nosva") {
2759 if (args
[argidx
] == "-L" && argidx
+1 < GetSize(args
)) {
2760 verific_sva_fsm_limit
= atoi(args
[++argidx
].c_str());
2763 if (args
[argidx
] == "-n") {
2767 if (args
[argidx
] == "-autocover") {
2768 mode_autocover
= true;
2771 if (args
[argidx
] == "-fullinit") {
2772 mode_fullinit
= true;
2775 if (args
[argidx
] == "-chparam" && argidx
+2 < GetSize(args
)) {
2776 const std::string
&key
= args
[++argidx
];
2777 const std::string
&value
= args
[++argidx
];
2778 unsigned new_insertion
= parameters
.Insert(key
.c_str(), value
.c_str(),
2779 1 /* force_overwrite */);
2781 log_warning_noprefix("-chparam %s already specified: overwriting.\n", key
.c_str());
2784 if (args
[argidx
] == "-V") {
2785 mode_verific
= true;
2788 if (args
[argidx
] == "-v") {
2789 verific_verbose
= 1;
2792 if (args
[argidx
] == "-vv") {
2793 verific_verbose
= 2;
2796 if (args
[argidx
] == "-d" && argidx
+1 < GetSize(args
)) {
2797 dumpfile
= args
[++argidx
];
2803 if (argidx
> GetSize(args
) && args
[argidx
].compare(0, 1, "-") == 0)
2804 cmd_error(args
, argidx
, "unknown option");
2806 std::set
<std::string
> top_mod_names
;
2808 #ifdef YOSYSHQ_VERIFIC_INITSTATE
2809 InitialAssertionRewriter rw
;
2810 rw
.RegisterCallBack();
2814 log("Running hier_tree::ElaborateAll().\n");
2816 VhdlLibrary
*vhdl_lib
= vhdl_file::GetLibrary(work
.c_str(), 1);
2817 VeriLibrary
*veri_lib
= veri_file::GetLibrary(work
.c_str(), 1);
2819 Array veri_libs
, vhdl_libs
;
2820 if (vhdl_lib
) vhdl_libs
.InsertLast(vhdl_lib
);
2821 if (veri_lib
) veri_libs
.InsertLast(veri_lib
);
2823 Array
*netlists
= hier_tree::ElaborateAll(&veri_libs
, &vhdl_libs
, ¶meters
);
2827 FOREACH_ARRAY_ITEM(netlists
, i
, nl
)
2833 if (argidx
== GetSize(args
))
2834 cmd_error(args
, argidx
, "No top module specified.\n");
2836 VeriLibrary
* veri_lib
= veri_file::GetLibrary(work
.c_str(), 1);
2837 VhdlLibrary
*vhdl_lib
= vhdl_file::GetLibrary(work
.c_str(), 1);
2839 Array veri_modules
, vhdl_units
;
2840 for (; argidx
< GetSize(args
); argidx
++)
2842 const char *name
= args
[argidx
].c_str();
2843 top_mod_names
.insert(name
);
2845 VeriModule
*veri_module
= veri_lib
? veri_lib
->GetModule(name
, 1) : nullptr;
2847 log("Adding Verilog module '%s' to elaboration queue.\n", name
);
2848 veri_modules
.InsertLast(veri_module
);
2852 VhdlDesignUnit
*vhdl_unit
= vhdl_lib
? vhdl_lib
->GetPrimUnit(name
) : nullptr;
2854 log("Adding VHDL unit '%s' to elaboration queue.\n", name
);
2855 vhdl_units
.InsertLast(vhdl_unit
);
2859 log_error("Can't find module/unit '%s'.\n", name
);
2863 // Also elaborate all root modules since they may contain bind statements
2865 VeriModule
*veri_module
;
2866 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib
, mi
, veri_module
) {
2867 if (!veri_module
->IsRootModule()) continue;
2868 veri_modules
.InsertLast(veri_module
);
2872 log("Running hier_tree::Elaborate().\n");
2873 Array
*netlists
= hier_tree::Elaborate(&veri_modules
, &vhdl_units
, ¶meters
);
2877 FOREACH_ARRAY_ITEM(netlists
, i
, nl
) {
2878 nl
->AddAtt(new Att(" \\top", NULL
));
2884 if (!verific_error_msg
.empty())
2888 for (auto nl
: nl_todo
)
2893 VerificExtNets worker
;
2894 for (auto nl
: nl_todo
)
2898 for (auto nl
: nl_todo
)
2899 nl
->ChangePortBusStructures(1 /* hierarchical */);
2901 if (!dumpfile
.empty()) {
2902 VeriWrite veri_writer
;
2903 veri_writer
.WriteFile(dumpfile
.c_str(), Netlist::PresentDesign());
2906 while (!nl_todo
.empty()) {
2907 Netlist
*nl
= *nl_todo
.begin();
2908 if (nl_done
.count(nl
) == 0) {
2909 VerificImporter
importer(mode_gates
, mode_keep
, mode_nosva
,
2910 mode_names
, mode_verific
, mode_autocover
, mode_fullinit
);
2911 importer
.import_netlist(design
, nl
, nl_todo
, top_mod_names
.count(nl
->Owner()->Name()));
2920 verific_incdirs
.clear();
2921 verific_libdirs
.clear();
2922 verific_import_pending
= false;
2926 cmd_error(args
, argidx
, "Missing or unsupported mode parameter.\n");
2929 if (!verific_error_msg
.empty())
2930 log_error("%s\n", verific_error_msg
.c_str());
2933 #else /* YOSYS_ENABLE_VERIFIC */
2934 void execute(std::vector
<std::string
>, RTLIL::Design
*) override
{
2935 log_cmd_error("This version of Yosys is built without Verific support.\n"
2937 "Use YosysHQ Tabby CAD Suite if you need Yosys+Verific.\n"
2938 "https://www.yosyshq.com/\n"
2940 "Contact office@yosyshq.com for free evaluation\n"
2941 "binaries of YosysHQ Tabby CAD Suite.\n");
2946 struct ReadPass
: public Pass
{
2947 ReadPass() : Pass("read", "load HDL designs") { }
2948 void help() override
2950 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2952 log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
2954 log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
2955 log("is only available via Verific.)\n");
2957 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2958 log("the language version (and before file names) to set additional verilog defines.\n");
2961 log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2963 log("Load the specified VHDL files. (Requires Verific.)\n");
2966 log(" read -define <macro>[=<value>]..\n");
2968 log("Set global Verilog/SystemVerilog defines.\n");
2971 log(" read -undef <macro>..\n");
2973 log("Unset global Verilog/SystemVerilog defines.\n");
2976 log(" read -incdir <directory>\n");
2978 log("Add directory to global Verilog/SystemVerilog include directories.\n");
2981 log(" read -verific\n");
2982 log(" read -noverific\n");
2984 log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
2985 log("with -verific will result in an error on Yosys binaries that are built without\n");
2986 log("Verific support. The default is to use Verific if it is available.\n");
2989 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) override
2991 #ifdef YOSYS_ENABLE_VERIFIC
2992 static bool verific_available
= !check_noverific_env();
2994 static bool verific_available
= false;
2996 static bool use_verific
= verific_available
;
2998 if (args
.size() < 2 || args
[1][0] != '-')
2999 cmd_error(args
, 1, "Missing mode parameter.\n");
3001 if (args
[1] == "-verific" || args
[1] == "-noverific") {
3002 if (args
.size() != 2)
3003 cmd_error(args
, 1, "Additional arguments to -verific/-noverific.\n");
3004 if (args
[1] == "-verific") {
3005 if (!verific_available
)
3006 cmd_error(args
, 1, "This version of Yosys is built without Verific support.\n");
3009 use_verific
= false;
3014 if (args
.size() < 3)
3015 cmd_error(args
, 3, "Missing file name parameter.\n");
3017 if (args
[1] == "-vlog95" || args
[1] == "-vlog2k") {
3019 args
[0] = "verific";
3021 args
[0] = "read_verilog";
3024 Pass::call(design
, args
);
3028 if (args
[1] == "-sv2005" || args
[1] == "-sv2009" || args
[1] == "-sv2012" || args
[1] == "-sv" || args
[1] == "-formal") {
3030 args
[0] = "verific";
3032 args
[0] = "read_verilog";
3033 if (args
[1] == "-formal")
3034 args
.insert(args
.begin()+1, std::string());
3036 args
.insert(args
.begin()+1, "-defer");
3038 Pass::call(design
, args
);
3042 if (args
[1] == "-vhdl87" || args
[1] == "-vhdl93" || args
[1] == "-vhdl2k" || args
[1] == "-vhdl2008" || args
[1] == "-vhdl") {
3044 args
[0] = "verific";
3045 Pass::call(design
, args
);
3047 cmd_error(args
, 1, "This version of Yosys is built without Verific support.\n");
3052 if (args
[1] == "-define") {
3054 args
[0] = "verific";
3055 args
[1] = "-vlog-define";
3056 Pass::call(design
, args
);
3058 args
[0] = "verilog_defines";
3059 args
.erase(args
.begin()+1, args
.begin()+2);
3060 for (int i
= 1; i
< GetSize(args
); i
++)
3061 args
[i
] = "-D" + args
[i
];
3062 Pass::call(design
, args
);
3066 if (args
[1] == "-undef") {
3068 args
[0] = "verific";
3069 args
[1] = "-vlog-undef";
3070 Pass::call(design
, args
);
3072 args
[0] = "verilog_defines";
3073 args
.erase(args
.begin()+1, args
.begin()+2);
3074 for (int i
= 1; i
< GetSize(args
); i
++)
3075 args
[i
] = "-U" + args
[i
];
3076 Pass::call(design
, args
);
3080 if (args
[1] == "-incdir") {
3082 args
[0] = "verific";
3083 args
[1] = "-vlog-incdir";
3084 Pass::call(design
, args
);
3086 args
[0] = "verilog_defaults";
3088 for (int i
= 2; i
< GetSize(args
); i
++)
3089 args
[i
] = "-I" + args
[i
];
3090 Pass::call(design
, args
);
3094 cmd_error(args
, 1, "Missing or unsupported mode parameter.\n");
3098 PRIVATE_NAMESPACE_END