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"
24 PRIVATE_NAMESPACE_BEGIN
26 struct ChformalPass
: public Pass
{
27 ChformalPass() : Pass("chformal", "change formal constraints of the design") { }
28 void help() YS_OVERRIDE
30 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
32 log(" chformal [types] [mode] [options] [selection]\n");
34 log("Make changes to the formal constraints of the design. The [types] options\n");
35 log("the type of constraint to operate on. If none of the following options are given,\n");
36 log("the command will operate on all constraint types:\n");
38 log(" -assert $assert cells, representing assert(...) constraints\n");
39 log(" -assume $assume cells, representing assume(...) constraints\n");
40 log(" -live $live cells, representing assert(s_eventually ...)\n");
41 log(" -fair $fair cells, representing assume(s_eventually ...)\n");
42 log(" -cover $cover cells, representing cover() statements\n");
44 log("Exactly one of the following modes must be specified:\n");
47 log(" remove the cells and thus constraints from the design\n");
50 log(" bypass FFs that only delay the activation of a constraint\n");
53 log(" delay activation of the constraint by <N> clock cycles\n");
56 log(" ignore activation of the constraint in the first <N> clock cycles\n");
58 log(" -assert2assume\n");
59 log(" -assume2assert\n");
62 log(" change the roles of cells as indicated. these options can be combined\n");
65 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
67 bool assert2assume
= false;
68 bool assume2assert
= false;
69 bool live2fair
= false;
70 bool fair2live
= false;
72 pool
<IdString
> constr_types
;
77 for (argidx
= 1; argidx
< args
.size(); argidx
++)
79 if (args
[argidx
] == "-assert") {
80 constr_types
.insert("$assert");
83 if (args
[argidx
] == "-assume") {
84 constr_types
.insert("$assume");
87 if (args
[argidx
] == "-live") {
88 constr_types
.insert("$live");
91 if (args
[argidx
] == "-fair") {
92 constr_types
.insert("$fair");
95 if (args
[argidx
] == "-cover") {
96 constr_types
.insert("$cover");
99 if (mode
== 0 && args
[argidx
] == "-remove") {
103 if (mode
== 0 && args
[argidx
] == "-early") {
107 if (mode
== 0 && args
[argidx
] == "-delay" && argidx
+1 < args
.size()) {
109 mode_arg
= atoi(args
[++argidx
].c_str());
112 if (mode
== 0 && args
[argidx
] == "-skip" && argidx
+1 < args
.size()) {
114 mode_arg
= atoi(args
[++argidx
].c_str());
117 if ((mode
== 0 || mode
== 'c') && args
[argidx
] == "-assert2assume") {
118 assert2assume
= true;
122 if ((mode
== 0 || mode
== 'c') && args
[argidx
] == "-assume2assert") {
123 assume2assert
= true;
127 if ((mode
== 0 || mode
== 'c') && args
[argidx
] == "-live2fair") {
132 if ((mode
== 0 || mode
== 'c') && args
[argidx
] == "-fair2live") {
139 extra_args(args
, argidx
, design
);
141 if (constr_types
.empty()) {
142 constr_types
.insert("$assert");
143 constr_types
.insert("$assume");
144 constr_types
.insert("$live");
145 constr_types
.insert("$fair");
146 constr_types
.insert("$cover");
150 log_cmd_error("Mode option is missing.\n");
152 for (auto module
: design
->selected_modules())
154 vector
<Cell
*> constr_cells
;
156 for (auto cell
: module
->selected_cells())
157 if (constr_types
.count(cell
->type
))
158 constr_cells
.push_back(cell
);
162 for (auto cell
: constr_cells
)
163 module
->remove(cell
);
168 SigMap
sigmap(module
);
169 dict
<SigBit
, pair
<SigBit
, pair
<SigBit
, bool>>> ffmap
;
170 pool
<SigBit
> init_zero
, init_one
;
172 for (auto wire
: module
->wires())
174 if (wire
->attributes
.count("\\init") == 0)
177 SigSpec initsig
= sigmap(wire
);
178 Const initval
= wire
->attributes
.at("\\init");
180 for (int i
= 0; i
< GetSize(initsig
) && i
< GetSize(initval
); i
++) {
181 if (initval
[i
] == State::S0
)
182 init_zero
.insert(initsig
[i
]);
183 if (initval
[i
] == State::S1
)
184 init_one
.insert(initsig
[i
]);
188 for (auto cell
: module
->selected_cells())
190 if (cell
->type
== "$ff") {
191 SigSpec D
= sigmap(cell
->getPort("\\D"));
192 SigSpec Q
= sigmap(cell
->getPort("\\Q"));
193 for (int i
= 0; i
< GetSize(D
); i
++)
194 ffmap
[Q
[i
]] = make_pair(D
[i
], make_pair(State::Sm
, false));
196 if (cell
->type
== "$dff") {
197 SigSpec D
= sigmap(cell
->getPort("\\D"));
198 SigSpec Q
= sigmap(cell
->getPort("\\Q"));
199 SigSpec C
= sigmap(cell
->getPort("\\CLK"));
200 bool clockpol
= cell
->getParam("\\CLK_POLARITY").as_bool();
201 for (int i
= 0; i
< GetSize(D
); i
++)
202 ffmap
[Q
[i
]] = make_pair(D
[i
], make_pair(C
, clockpol
));
206 for (auto cell
: constr_cells
)
209 SigSpec A
= sigmap(cell
->getPort("\\A"));
210 SigSpec EN
= sigmap(cell
->getPort("\\EN"));
212 if (ffmap
.count(A
) == 0 || ffmap
.count(EN
) == 0)
215 if (!init_zero
.count(EN
)) {
216 if (cell
->type
== "$cover") break;
217 if (cell
->type
.in("$assert", "$assume") && !init_one
.count(A
)) break;
220 const auto &A_map
= ffmap
.at(A
);
221 const auto &EN_map
= ffmap
.at(EN
);
223 if (A_map
.second
!= EN_map
.second
)
226 cell
->setPort("\\A", A_map
.first
);
227 cell
->setPort("\\EN", EN_map
.first
);
233 for (auto cell
: constr_cells
)
234 for (int i
= 0; i
< mode_arg
; i
++)
236 SigSpec orig_a
= cell
->getPort("\\A");
237 SigSpec orig_en
= cell
->getPort("\\EN");
239 Wire
*new_a
= module
->addWire(NEW_ID
);
240 Wire
*new_en
= module
->addWire(NEW_ID
);
241 new_en
->attributes
["\\init"] = State::S0
;
243 module
->addFf(NEW_ID
, orig_a
, new_a
);
244 module
->addFf(NEW_ID
, orig_en
, new_en
);
246 cell
->setPort("\\A", new_a
);
247 cell
->setPort("\\EN", new_en
);
253 SigSpec en
= State::S1
;
255 for (int i
= 0; i
< mode_arg
; i
++) {
256 Wire
*w
= module
->addWire(NEW_ID
);
257 w
->attributes
["\\init"] = State::S0
;
258 module
->addFf(NEW_ID
, en
, w
);
262 for (auto cell
: constr_cells
)
263 cell
->setPort("\\EN", module
->LogicAnd(NEW_ID
, en
, cell
->getPort("\\EN")));
268 for (auto cell
: constr_cells
)
269 if (assert2assume
&& cell
->type
== "$assert")
270 cell
->type
= "$assume";
271 else if (assume2assert
&& cell
->type
== "$assume")
272 cell
->type
= "$assert";
273 else if (live2fair
&& cell
->type
== "$live")
274 cell
->type
= "$fair";
275 else if (fair2live
&& cell
->type
== "$fair")
276 cell
->type
= "$live";
282 PRIVATE_NAMESPACE_END