mirror of https://github.com/YosysHQ/yosys.git
WIP docs: Proto log_help
Define `PrettyHelp` class with methods for declaring different parts of help message. Currently able to produce standard help messages as expected. Updates chformal to use (only) the new help_v2. Currently makes use of a global static to track the current help context, allowing register.h to live in blissful ignorance and instead rely on help_v2 implementations calling `auto *help = PrettyHelp::get_current();` and `return true;` to minimise impact on rebuilds (i.e. not requiring every source file to be recompiled).
This commit is contained in:
Krystine Sherwin
parent
4f0abe4924
commit
9cbb17061d
1
Makefile
1
Makefile
|
|
@ -610,6 +610,7 @@ $(eval $(call add_include_file,frontends/blif/blifparse.h))
|
|||
$(eval $(call add_include_file,backends/rtlil/rtlil_backend.h))
|
||||
|
||||
OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o
|
||||
OBJS += kernel/log_help.o
|
||||
OBJS += kernel/binding.o kernel/tclapi.o
|
||||
OBJS += kernel/cellaigs.o kernel/celledges.o kernel/cost.o kernel/satgen.o kernel/scopeinfo.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o kernel/fmt.o kernel/sexpr.o
|
||||
OBJS += kernel/drivertools.o kernel/functional.o
|
||||
|
|
|
|||
|
|
@ -0,0 +1,116 @@
|
|||
/*
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Copyright (C) 2025 Krystine Dawn <krystinedawn@yosyshq.com>
|
||||
*
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
*
|
||||
*/
|
||||
|
||||
#include "kernel/log_help.h"
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
|
||||
#define MAX_LINE_LEN 80
|
||||
void log_pass_str(const std::string &pass_str, std::string indent_str, bool leading_newline=false) {
|
||||
if (pass_str.empty())
|
||||
return;
|
||||
std::istringstream iss(pass_str);
|
||||
if (leading_newline)
|
||||
log("\n");
|
||||
for (std::string line; std::getline(iss, line);) {
|
||||
log("%s", indent_str.c_str());
|
||||
auto curr_len = indent_str.length();
|
||||
std::istringstream lss(line);
|
||||
for (std::string word; std::getline(lss, word, ' ');) {
|
||||
while (word[0] == '`' && word.back() == '`')
|
||||
word = word.substr(1, word.length()-2);
|
||||
if (curr_len + word.length() >= MAX_LINE_LEN-1) {
|
||||
curr_len = 0;
|
||||
log("\n%s", indent_str.c_str());
|
||||
}
|
||||
if (word.length()) {
|
||||
log("%s ", word.c_str());
|
||||
curr_len += word.length() + 1;
|
||||
}
|
||||
}
|
||||
log("\n");
|
||||
}
|
||||
}
|
||||
void log_pass_str(const std::string &pass_str, int indent=0, bool leading_newline=false) {
|
||||
std::string indent_str(indent*4, ' ');
|
||||
log_pass_str(pass_str, indent_str, leading_newline);
|
||||
}
|
||||
|
||||
PrettyHelp *current_help = nullptr;
|
||||
|
||||
PrettyHelp::PrettyHelp()
|
||||
{
|
||||
prior = current_help;
|
||||
current_help = this;
|
||||
}
|
||||
|
||||
PrettyHelp::~PrettyHelp()
|
||||
{
|
||||
current_help = prior;
|
||||
}
|
||||
|
||||
PrettyHelp *PrettyHelp::get_current()
|
||||
{
|
||||
if (current_help != nullptr)
|
||||
return current_help;
|
||||
else
|
||||
return new PrettyHelp();
|
||||
}
|
||||
|
||||
bool PrettyHelp::has_content()
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
void PrettyHelp::usage(const string &usage)
|
||||
{
|
||||
log_pass_str(usage, current_indent+1, true);
|
||||
log("\n");
|
||||
}
|
||||
|
||||
void PrettyHelp::option(const string &option, const string &description)
|
||||
{
|
||||
log_pass_str(option, current_indent);
|
||||
if (description.length()) {
|
||||
log_pass_str(description, current_indent+1);
|
||||
log("\n");
|
||||
}
|
||||
}
|
||||
|
||||
void PrettyHelp::codeblock(const string &code, const string &)
|
||||
{
|
||||
log("%s\n", code.c_str());
|
||||
}
|
||||
|
||||
void PrettyHelp::paragraph(const string &text)
|
||||
{
|
||||
log_pass_str(text, current_indent);
|
||||
log("\n");
|
||||
}
|
||||
|
||||
void PrettyHelp::optiongroup(const string &)
|
||||
{
|
||||
current_indent += 1;
|
||||
}
|
||||
|
||||
void PrettyHelp::endgroup()
|
||||
{
|
||||
current_indent -= 1;
|
||||
log_assert(current_indent >= 0);
|
||||
}
|
||||
|
|
@ -0,0 +1,51 @@
|
|||
/*
|
||||
* yosys -- Yosys Open SYnthesis Suite
|
||||
*
|
||||
* Copyright (C) 2025 Krystine Dawn <krystinedawn@yosyshq.com>
|
||||
*
|
||||
* Permission to use, copy, modify, and/or distribute this software for any
|
||||
* purpose with or without fee is hereby granted, provided that the above
|
||||
* copyright notice and this permission notice appear in all copies.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
||||
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
||||
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
||||
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
||||
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
||||
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
||||
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
||||
*
|
||||
*/
|
||||
|
||||
#ifndef LOG_HELP_H
|
||||
#define LOG_HELP_H
|
||||
|
||||
#include "kernel/yosys_common.h"
|
||||
#include "kernel/json.h"
|
||||
|
||||
YOSYS_NAMESPACE_BEGIN
|
||||
|
||||
class PrettyHelp
|
||||
{
|
||||
PrettyHelp *prior = nullptr;
|
||||
int current_indent = 0;
|
||||
public:
|
||||
PrettyHelp();
|
||||
~PrettyHelp();
|
||||
|
||||
static PrettyHelp *get_current();
|
||||
|
||||
bool has_content();
|
||||
|
||||
void usage(const string &usage);
|
||||
void option(const string &option, const string &description = "");
|
||||
void codeblock(const string &code, const string &language = "none");
|
||||
void paragraph(const string &text);
|
||||
|
||||
void optiongroup(const string &group = "");
|
||||
void endgroup();
|
||||
};
|
||||
|
||||
YOSYS_NAMESPACE_END
|
||||
|
||||
#endif
|
||||
|
|
@ -20,6 +20,7 @@
|
|||
#include "kernel/yosys.h"
|
||||
#include "kernel/satgen.h"
|
||||
#include "kernel/json.h"
|
||||
#include "kernel/log_help.h"
|
||||
|
||||
#include <string.h>
|
||||
#include <stdlib.h>
|
||||
|
|
@ -99,7 +100,7 @@ std::map<std::string, Backend*> backend_register;
|
|||
|
||||
std::vector<std::string> Frontend::next_args;
|
||||
|
||||
Pass::Pass(std::string name, std::string short_help, const vector<std::string> doc_string, const vector<PassUsageBlock> usages) : pass_name(name), short_help(short_help), doc_string(doc_string), pass_usages(usages)
|
||||
Pass::Pass(std::string name, std::string short_help) : pass_name(name), short_help(short_help)
|
||||
{
|
||||
next_queued_pass = first_queued_pass;
|
||||
first_queued_pass = this;
|
||||
|
|
@ -172,79 +173,20 @@ void Pass::post_execute(Pass::pre_post_exec_state_t state)
|
|||
current_pass->runtime_ns -= time_ns;
|
||||
}
|
||||
|
||||
#define MAX_LINE_LEN 80
|
||||
void log_pass_str(const std::string &pass_str, std::string indent_str, bool leading_newline=false) {
|
||||
if (pass_str.empty())
|
||||
return;
|
||||
std::istringstream iss(pass_str);
|
||||
if (leading_newline)
|
||||
log("\n");
|
||||
for (std::string line; std::getline(iss, line);) {
|
||||
log("%s", indent_str.c_str());
|
||||
auto curr_len = indent_str.length();
|
||||
std::istringstream lss(line);
|
||||
for (std::string word; std::getline(lss, word, ' ');) {
|
||||
while (word[0] == '`' && word.back() == '`')
|
||||
word = word.substr(1, word.length()-2);
|
||||
if (curr_len + word.length() >= MAX_LINE_LEN-1) {
|
||||
curr_len = 0;
|
||||
log("\n%s", indent_str.c_str());
|
||||
}
|
||||
if (word.length()) {
|
||||
log("%s ", word.c_str());
|
||||
curr_len += word.length() + 1;
|
||||
}
|
||||
}
|
||||
log("\n");
|
||||
}
|
||||
}
|
||||
void log_pass_str(const std::string &pass_str, int indent=0, bool leading_newline=false) {
|
||||
std::string indent_str(indent*4, ' ');
|
||||
log_pass_str(pass_str, indent_str, leading_newline);
|
||||
}
|
||||
|
||||
void Pass::help()
|
||||
{
|
||||
if (HasUsages()) {
|
||||
for (auto usage : pass_usages) {
|
||||
log_pass_str(usage.signature, 1, true);
|
||||
log_pass_str(usage.description, 0, true);
|
||||
for (auto option : usage.options) {
|
||||
log_pass_str(option.keyword, 1, true);
|
||||
log_pass_str(option.description, 2, false);
|
||||
}
|
||||
log_pass_str(usage.postscript, 0, true);
|
||||
}
|
||||
log("\n");
|
||||
} else if (HasDocstring()) {
|
||||
log("\n");
|
||||
auto print_empty = true;
|
||||
for (auto doc_line : doc_string) {
|
||||
if (doc_line.find("..") == 0 && doc_line.find(":: ") != std::string::npos) {
|
||||
auto command_pos = doc_line.find(":: ");
|
||||
auto command_str = doc_line.substr(0, command_pos);
|
||||
if (command_str.compare(".. cmd:usage") == 0) {
|
||||
log_pass_str(doc_line.substr(command_pos+3), 1);
|
||||
} else {
|
||||
print_empty = false;
|
||||
}
|
||||
} else if (doc_line.length()) {
|
||||
std::size_t first_pos = doc_line.find_first_not_of(" \t");
|
||||
auto indent_str = doc_line.substr(0, first_pos);
|
||||
log_pass_str(doc_line, indent_str);
|
||||
print_empty = true;
|
||||
} else if (print_empty) {
|
||||
log("\n");
|
||||
}
|
||||
}
|
||||
log("\n");
|
||||
} else {
|
||||
if (!help_v2()) {
|
||||
log("\n");
|
||||
log("No help message for command `%s'.\n", pass_name.c_str());
|
||||
log("\n");
|
||||
}
|
||||
}
|
||||
|
||||
bool Pass::help_v2()
|
||||
{
|
||||
return false;
|
||||
}
|
||||
|
||||
void Pass::clear_flags()
|
||||
{
|
||||
}
|
||||
|
|
@ -975,13 +917,12 @@ struct HelpPass : public Pass {
|
|||
if (name.compare("verific") != 0 && name.find("chformal") == string::npos) continue;
|
||||
auto pass = it.second;
|
||||
auto title = pass->short_help;
|
||||
vector<PassUsageBlock> usages;
|
||||
auto experimental_flag = pass->experimental_flag;
|
||||
|
||||
if (pass->HasUsages() || pass->HasDocstring()) {
|
||||
for (auto usage : pass->pass_usages)
|
||||
usages.push_back(usage);
|
||||
} else {
|
||||
auto cmd_help = PrettyHelp();
|
||||
auto has_pretty_help = pass->help_v2();
|
||||
|
||||
if (!has_pretty_help) {
|
||||
enum PassUsageState {
|
||||
PUState_signature,
|
||||
PUState_description,
|
||||
|
|
@ -1029,7 +970,7 @@ struct HelpPass : public Pass {
|
|||
|
||||
if (NewUsage) {
|
||||
current_state = PUState_signature;
|
||||
usages.push_back({});
|
||||
// usages.push_back({});
|
||||
def_strip_count = first_pos;
|
||||
catch_verific = false;
|
||||
} else if (IsDedent) {
|
||||
|
|
@ -1042,19 +983,19 @@ struct HelpPass : public Pass {
|
|||
|
||||
if (IsDefinition && IsIndent && !catch_verific) {
|
||||
current_state = PUState_options;
|
||||
usages.back().options.push_back(PassOption({stripped_line, ""}));
|
||||
// usages.back().options.push_back(PassOption({stripped_line, ""}));
|
||||
def_strip_count = first_pos;
|
||||
} else {
|
||||
string *desc_str;
|
||||
if (current_state == PUState_signature) {
|
||||
desc_str = &(usages.back().signature);
|
||||
// desc_str = &(usages.back().signature);
|
||||
blank_count += 1;
|
||||
} else if (current_state == PUState_description) {
|
||||
desc_str = &(usages.back().description);
|
||||
// desc_str = &(usages.back().description);
|
||||
} else if (current_state == PUState_options) {
|
||||
desc_str = &(usages.back().options.back().description);
|
||||
// desc_str = &(usages.back().options.back().description);
|
||||
} else if (current_state == PUState_postscript) {
|
||||
desc_str = &(usages.back().postscript);
|
||||
// desc_str = &(usages.back().postscript);
|
||||
} else {
|
||||
log_abort();
|
||||
}
|
||||
|
|
@ -1075,28 +1016,7 @@ struct HelpPass : public Pass {
|
|||
// write to json
|
||||
json.name(name.c_str()); json.begin_object();
|
||||
json.entry("title", title);
|
||||
if (pass->HasDocstring()) {
|
||||
json.entry("content", pass->doc_string);
|
||||
}
|
||||
if (usages.size()) {
|
||||
json.name("usages"); json.begin_array();
|
||||
for (auto usage : usages) {
|
||||
json.begin_object();
|
||||
json.entry("signature", usage.signature);
|
||||
json.entry("description", usage.description);
|
||||
json.name("options"); json.begin_array();
|
||||
for (auto option : usage.options) {
|
||||
json.begin_array();
|
||||
json.value(option.keyword);
|
||||
json.value(option.description);
|
||||
json.end_array();
|
||||
}
|
||||
json.end_array();
|
||||
json.entry("postscript", usage.postscript);
|
||||
json.end_object();
|
||||
}
|
||||
json.end_array();
|
||||
}
|
||||
// json.entry("content", cmd_help);
|
||||
json.entry("experimental_flag", experimental_flag);
|
||||
json.end_object();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -25,29 +25,14 @@
|
|||
|
||||
YOSYS_NAMESPACE_BEGIN
|
||||
|
||||
struct PassOption {
|
||||
string keyword;
|
||||
string description;
|
||||
};
|
||||
|
||||
struct PassUsageBlock {
|
||||
string signature = "";
|
||||
string description = "";
|
||||
vector<PassOption> options = {};
|
||||
string postscript = "";
|
||||
};
|
||||
|
||||
struct Pass
|
||||
{
|
||||
std::string pass_name, short_help;
|
||||
const vector<std::string> doc_string;
|
||||
const vector<PassUsageBlock> pass_usages;
|
||||
Pass(std::string name, std::string short_help = "** document me **",
|
||||
const vector<std::string> doc_string = {},
|
||||
const vector<PassUsageBlock> usages = {});
|
||||
Pass(std::string name, std::string short_help = "** document me **");
|
||||
virtual ~Pass();
|
||||
|
||||
virtual void help();
|
||||
virtual bool help_v2();
|
||||
virtual void clear_flags();
|
||||
virtual void execute(std::vector<std::string> args, RTLIL::Design *design) = 0;
|
||||
|
||||
|
|
@ -59,14 +44,6 @@ struct Pass
|
|||
experimental_flag = true;
|
||||
}
|
||||
|
||||
bool HasUsages() {
|
||||
return !pass_usages.empty();
|
||||
}
|
||||
|
||||
bool HasDocstring() {
|
||||
return !doc_string.empty();
|
||||
}
|
||||
|
||||
struct pre_post_exec_state_t {
|
||||
Pass *parent_pass;
|
||||
int64_t begin_ns;
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@
|
|||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/sigtools.h"
|
||||
#include "kernel/log_help.h"
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
|
@ -69,183 +70,59 @@ static bool is_triggered_check_cell(RTLIL::Cell * cell)
|
|||
return cell->type == ID($check) && cell->getParam(ID(TRG_ENABLE)).as_bool();
|
||||
}
|
||||
|
||||
struct ChformalPassStruct : public Pass {
|
||||
ChformalPassStruct() : Pass("chformal_struct", "change formal constraints of the design", {}, {
|
||||
{
|
||||
.signature = "chformal [types] [mode] [options] [selection]",
|
||||
.description = "Make changes to the formal constraints of the design. The [types] options the type of "
|
||||
"constraint to operate on. If none of the following options are given, the command "
|
||||
"will operate on all constraint types:",
|
||||
.options = {
|
||||
{"-assert $assert cells, representing assert(...) constraints"
|
||||
"\n-assume $assume cells, representing assume(...) constraints"
|
||||
"\n-live $live cells, representing assert(s_eventually ...)"
|
||||
"\n-fair $fair cells, representing assume(s_eventually ...)"
|
||||
"\n-cover $cover cells, representing cover() statements", ""},
|
||||
{"Additionally chformal will operate on $check cells corresponding to the selected constraint "
|
||||
"types.", ""},
|
||||
}
|
||||
},
|
||||
{
|
||||
.description = "Exactly one of the following modes must be specified:",
|
||||
.options = {
|
||||
{"-remove",
|
||||
"remove the cells and thus constraints from the design"},
|
||||
{"-early",
|
||||
"bypass FFs that only delay the activation of a constraint. When inputs "
|
||||
"of the bypassed FFs do not remain stable between clock edges, this may "
|
||||
"result in unexpected behavior."
|
||||
},
|
||||
{"-delay <N>",
|
||||
"delay activation of the constraint by <N> clock cycles"
|
||||
},
|
||||
{"-skip <N>",
|
||||
"ignore activation of the constraint in the first <N> clock cycles"
|
||||
},
|
||||
{"-coverenable",
|
||||
"add cover statements for the enable signals of the constraints"
|
||||
#ifdef YOSYS_ENABLE_VERIFIC
|
||||
"\n\nNote: For the Verific frontend it is currently not guaranteed that a "
|
||||
"reachable SVA statement corresponds to an active enable signal."
|
||||
#endif
|
||||
},
|
||||
{"-assert2assume"
|
||||
"\n-assume2assert"
|
||||
"\n-live2fair"
|
||||
"\n-fair2live",
|
||||
"change the roles of cells as indicated. these options can be combined"
|
||||
},
|
||||
{"-lower",
|
||||
"convert each $check cell into an $assert, $assume, $live, $fair or "
|
||||
"$cover cell. If the $check cell contains a message, also produce a "
|
||||
"$print cell."
|
||||
},
|
||||
}
|
||||
},
|
||||
}) { }
|
||||
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override {}
|
||||
|
||||
} ChformalPassStruct;
|
||||
|
||||
struct ChformalPassDocs : public Pass {
|
||||
ChformalPassDocs() : Pass("chformal_docstring", "change formal constraints of the design", {
|
||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||
".. cmd:usage:: chformal [types] [mode] [options] [selection]",
|
||||
"",
|
||||
"Make changes to the formal constraints of the design. The [types] options "
|
||||
"the type of constraint to operate on. If none of the following options are "
|
||||
"given, the command will operate on all constraint types:",
|
||||
"",
|
||||
".. cmd:optiongroup:: [types]",
|
||||
"",
|
||||
" :option -assert: `$assert` cells, representing ``assert(...)`` constraints",
|
||||
" :option -assume: `$assume` cells, representing ``assume(...)`` constraints",
|
||||
" :option -live: `$live` cells, representing ``assert(s_eventually ...)``",
|
||||
" :option -fair: `$fair` cells, representing ``assume(s_eventually ...)``",
|
||||
" :option -cover: `$cover` cells, representing ``cover()`` statements",
|
||||
"",
|
||||
" Additionally chformal will operate on `$check` cells corresponding to the "
|
||||
" selected constraint types.",
|
||||
"",
|
||||
"Exactly one of the following modes must be specified:",
|
||||
"",
|
||||
".. cmd:optiongroup:: [mode]",
|
||||
"",
|
||||
" :option -remove:",
|
||||
" remove the cells and thus constraints from the design",
|
||||
"",
|
||||
" :option -early:",
|
||||
" bypass FFs that only delay the activation of a constraint. When inputs "
|
||||
" of the bypassed FFs do not remain stable between clock edges, this may "
|
||||
" result in unexpected behavior.",
|
||||
"",
|
||||
" :option -delay <N>:",
|
||||
" delay activation of the constraint by <N> clock cycles",
|
||||
"",
|
||||
" :option -skip <N>:",
|
||||
" ignore activation of the constraint in the first <N> clock cycles",
|
||||
"",
|
||||
" :option -coverenable:",
|
||||
" add cover statements for the enable signals of the constraints",
|
||||
#ifdef YOSYS_ENABLE_VERIFIC
|
||||
"",
|
||||
" Note: For the Verific frontend it is currently not guaranteed that a "
|
||||
" reachable SVA statement corresponds to an active enable signal.",
|
||||
#endif
|
||||
"",
|
||||
" :option -assert2assume:",
|
||||
" :option -assume2assert:",
|
||||
" :option -live2fair:",
|
||||
" :option -fair2live:",
|
||||
" change the roles of cells as indicated. these options can be combined",
|
||||
"",
|
||||
" :option -lower:",
|
||||
" convert each $check cell into an $assert, $assume, $live, $fair or "
|
||||
" $cover cell. If the $check cell contains a message, also produce a "
|
||||
" $print cell.",
|
||||
}) { }
|
||||
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override {}
|
||||
|
||||
} ChformalPassDocs;
|
||||
|
||||
struct ChformalPass : public Pass {
|
||||
ChformalPass() : Pass("chformal", "change formal constraints of the design") {};
|
||||
void help() override
|
||||
{
|
||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||
log("\n");
|
||||
log(" chformal [types] [mode] [options] [selection]\n");
|
||||
log("\n");
|
||||
log("Make changes to the formal constraints of the design. The [types] options\n");
|
||||
log("the type of constraint to operate on. If none of the following options are\n");
|
||||
log("given, the command will operate on all constraint types:\n");
|
||||
log("\n");
|
||||
log(" -assert $assert cells, representing assert(...) constraints\n");
|
||||
log(" -assume $assume cells, representing assume(...) constraints\n");
|
||||
log(" -live $live cells, representing assert(s_eventually ...)\n");
|
||||
log(" -fair $fair cells, representing assume(s_eventually ...)\n");
|
||||
log(" -cover $cover cells, representing cover() statements\n");
|
||||
log("\n");
|
||||
log(" Additionally chformal will operate on $check cells corresponding to the\n");
|
||||
log(" selected constraint types.\n");
|
||||
log("\n");
|
||||
log("Exactly one of the following modes must be specified:\n");
|
||||
log("\n");
|
||||
log(" -remove\n");
|
||||
log(" remove the cells and thus constraints from the design\n");
|
||||
log("\n");
|
||||
log(" -early\n");
|
||||
log(" bypass FFs that only delay the activation of a constraint. When inputs\n");
|
||||
log(" of the bypassed FFs do not remain stable between clock edges, this may\n");
|
||||
log(" result in unexpected behavior.\n");
|
||||
log("\n");
|
||||
log(" -delay <N>\n");
|
||||
log(" delay activation of the constraint by <N> clock cycles\n");
|
||||
log("\n");
|
||||
log(" -skip <N>\n");
|
||||
log(" ignore activation of the constraint in the first <N> clock cycles\n");
|
||||
log("\n");
|
||||
log(" -coverenable\n");
|
||||
log(" add cover statements for the enable signals of the constraints\n");
|
||||
log("\n");
|
||||
ChformalPass() : Pass("chformal", "change formal constraints of the design") {}
|
||||
|
||||
bool help_v2() override {
|
||||
auto *help = PrettyHelp::get_current();
|
||||
help->usage("chformal [types] [mode] [options] [selection]");
|
||||
help->paragraph(
|
||||
"Make changes to the formal constraints of the design. The [types] options "
|
||||
"the type of constraint to operate on. If none of the following options are "
|
||||
"given, the command will operate on all constraint types:"
|
||||
);
|
||||
|
||||
help->optiongroup("[types]");
|
||||
help->option("-assert", "`$assert` cells, representing ``assert(...)`` constraints");
|
||||
help->option("-assume", "`$assume` cells, representing ``assume(...)`` constraints");
|
||||
help->option("-live", "`$live` cells, representing ``assert(s_eventually ...)``");
|
||||
help->option("-fair", "`$fair` cells, representing ``assume(s_eventually ...)``");
|
||||
help->option("-cover", "`$cover` cells, representing ``cover()`` statements");
|
||||
help->paragraph(
|
||||
"Additionally chformal will operate on `$check` cells corresponding to the "
|
||||
"selected constraint types."
|
||||
);
|
||||
help->endgroup();
|
||||
|
||||
help->paragraph("Exactly one of the following modes must be specified:");
|
||||
|
||||
help->optiongroup("[mode]");
|
||||
help->option("-remove", "remove the cells and thus constraints from the design");
|
||||
help->option("-early",
|
||||
"bypass FFs that only delay the activation of a constraint. When inputs "
|
||||
"of the bypassed FFs do not remain stable between clock edges, this may "
|
||||
"result in unexpected behavior."
|
||||
);
|
||||
help->option("-delay <N>", "delay activation of the constraint by <N> clock cycles");
|
||||
help->option("-skip <N>", "ignore activation of the constraint in the first <N> clock cycles");
|
||||
help->option("-coverenable",
|
||||
"add cover statements for the enable signals of the constraints"
|
||||
#ifdef YOSYS_ENABLE_VERIFIC
|
||||
log(" Note: For the Verific frontend it is currently not guaranteed that a\n");
|
||||
log(" reachable SVA statement corresponds to an active enable signal.\n");
|
||||
log("\n");
|
||||
"\n\n"
|
||||
"Note: For the Verific frontend it is currently not guaranteed that a "
|
||||
"reachable SVA statement corresponds to an active enable signal."
|
||||
#endif
|
||||
log(" -assert2assume\n");
|
||||
log(" -assume2assert\n");
|
||||
log(" -live2fair\n");
|
||||
log(" -fair2live\n");
|
||||
log(" change the roles of cells as indicated. these options can be combined\n");
|
||||
log("\n");
|
||||
log(" -lower\n");
|
||||
log(" convert each $check cell into an $assert, $assume, $live, $fair or\n");
|
||||
log(" $cover cell. If the $check cell contains a message, also produce a\n");
|
||||
log(" $print cell.\n");
|
||||
log("\n");
|
||||
);
|
||||
help->option("-assert2assume");
|
||||
help->option("-assume2assert");
|
||||
help->option("-live2fair");
|
||||
help->option("-fair2live", "change the roles of cells as indicated. these options can be combined");
|
||||
help->option("-lower",
|
||||
"convert each $check cell into an $assert, $assume, $live, $fair or "
|
||||
"$cover cell. If the $check cell contains a message, also produce a "
|
||||
"$print cell."
|
||||
);
|
||||
return true;
|
||||
}
|
||||
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
|
|
|
|||
Loading…
Reference in New Issue