
开发工具Lint静态分析硬件开发【免费下载链接】veribleVerible is a suite of SystemVerilog developer tools, including a parser, style-linter, formatter and language server项目地址https://gitcode.com/gh_mirrors/ve/verible点击查看免费下载本文以 doc/formatter.md 这份开发者指南为骨架逐层拆解 Verible 中 SystemVerilog 格式化器verible-verilog-format的内部架构从相邻 Token 间的间距标注InterTokenInfo到把语法树“解包”成TokenPartitionTree的TreeUnwrapper再到基于最短路搜索的换行优化与表格对齐tabular alignment。读完后你不仅能理解verible-verilog-format各阶段在做什么、哪些源码文件负责哪个环节还能掌握官方给出的故障排查命令与环境变量组合独立定位格式化行为异常。格式化器整体数据流doc/formatter.md把格式化器描述为若干子系统Inter-Token AnnotationToken 间标注、Token Partition TreeToken 分区树、Custom Policies自定义策略、Wrapping换行优化与 Alignment对齐。从源码结构看这些子系统在 Formatter::Format() 中按如下顺序串联构建UnwrapperData把词法 Token 流过滤成PreFormatToken序列保留注释、去除纯空白见 tree-unwrapper.h 中的UnwrapperData定义。Token 间标注调用 AnnotateFormattingInformation() 为每对相邻 Token 填充InterTokenInfo。注释明确要求此步骤必须先于任何“是否展开分区”的决策因为决策依赖最小间距与必须换行等信息formatter.cc。计算禁用区间DisableFormattingRanges()解析// verilog_format: off/on注释指令PreserveSpacesOnDisabledTokenRanges()将这些区间标记为“保留原始空白”。解包语法树tree_unwrapper.Unwrap()把 CST 转换为TokenPartitionTree。策略重塑按分区策略执行kAppendFittingSubPartitions的重塑ReshapeFittingSubpartitions、布局优化器策略OptimizeTokenPartitionTree以及kTabularAlignment的表格对齐TabularAlignTokenPartitions见 formatter.cc。换行搜索对每个可独立工作的UnwrappedLine调用SearchLineWraps()最小化换行/间距决策的总代价。校验与收敛格式化结果会重新解析并做词法等价检查全文件格式化时还会验证format(format(text)) format(text)收敛性FormatVerilog()。此外ExecutionControl 结构体承载了大量诊断开关show_token_partition_tree、show_inter_token_info、show_largest_token_partitions、max_search_states、verify_convergence等它们既是开发调试工具也是命令行上的正式参数。Inter-Token Annotation相邻 Token 之间的格式属性doc/formatter.md指出在被格式化文本的每一对相邻 Token 之间都有一组影响间距与换行决策的属性即InterTokenInfo例如两 Token 之间的最小间距。Token annotator 的职责就是依据相邻 Token 的属性、类型和语法上下文来填充这些属性——围绕括号、方括号等标点 Token 的格式化规则往往高度依赖语法上下文。在源码中InterTokenInfo是一个结构体format-token.h核心字段为字段含义spaces_required该 Token 前应插入的空格数最小间距。若删除空格会改变词法流错误该值必须非零也可用于格式化行首 Token 的缩进break_penalty在该 Token 前换行所引入的惩罚值供优化阶段使用break_decisionSpacingOptions枚举编码换行探索选项preserved_space_start指向原始空白文本起点的迭代器配合当前 Token 可还原SpacingOptions::kPreserve情形下的既有空白SpacingOptions与最终决策SpacingDecision的取值format-token.henum class SpacingOptions { kUndecided, // 未决定待优化默认 kMustAppend, // 此处不能换行 kMustWrap, // 此处必须换行 kAppendAligned, // 追加时允许左侧填充空格 kPreserve, // 不优化使用原始间距 }; enum class SpacingDecision { // 优化后的最终决策刻意没有“未决定” kPreserve, // 保留原始间距 kAppend, // 追加到当前行带适当间距 kWrap, // 换到下一行带适当缩进 kAlign, // 类似 Append但强制左侧填充空格即使在行首 };规则与理由Rules and Reasons原文档特别强调了标注函数的编写风格确定InterTokenInfo各属性的主函数都以优先级排序的规则形式书写即一系列if (condition) return ...;。相邻 Token 对的组合可能有 O(N²) 种但目标是用少量规则覆盖尽可能大的组合空间而 token-annotator_test.cc 这类测试则应尽可能显式覆盖防止无意回归。另一个值得注意的调试设计开启日志运行时这些函数返回的每个值或属性都会附带一个reason字符串例如Always insert a space after X。它不仅告诉你返回值还告诉你是哪一行/哪条规则触发的这对调试至关重要。文档给出的维护建议也很具体修复问题时不要立刻想“该加什么代码”先考虑调整规则顺序是否可行——把相似的 case 条件归组、或把某条规则泛化到更宽的范围有时反而能简化代码。Token Partition Tree格式化子问题的层次化表示TokenPartitionTree 是格式化Token 区段的语言无关的层次化表示。每个节点承载的数据是一个 UnwrappedLine其中包含一段格式化 Token 区间用轻量级const_iterator范围表示可无拷贝开销地增长以及缩进信息。TokenPartitionTree满足两条不变式原文档原文树中某节点跨越的区间等于其所有子节点跨越的区间之和若有子节点相邻兄弟节点的 Token 区间端点相等即相邻兄弟节点之间没有区间空隙。doc/formatter.md对每个节点的语义给出了一个很有用的心智模型把它看作一个格式化子问题——给定框宽约束这段文本的最佳格式化方式是什么TokenPartitionTree的叶分区则是当前由换行优化阶段处理的“工作单位”。UnwrappedLine的另一个关键字段是分区策略 PartitionPolicyEnum原文档提到的两个策略kTabularAlignment、kAppendFittingSubPartitions都在其中enum class PartitionPolicyEnum { kUninitialized, // 未设置策略 kAlwaysExpand, // 仅用于分组始终展开子分区 kFitOnLineElseExpand, // 不超过列限时压成一行否则展开 kTabularAlignment, // 子分区之间用空格填充实现垂直对齐 kAlreadyFormatted, // 已完成格式化跳过 SearchLineWraps kInline, // kAlreadyFormatted 行的切片布局优化器用 kAppendFittingSubPartitions, // 子分区作为整体能放同一行就放 kJuxtaposition, kStack, kWrap, kJuxtapositionOrIndentedStack, // LayoutOptimizer 策略 };Tree Unwrapping把 CST 变成分区树TreeUnwrapper 负责把 SystemVerilog 具体语法树CST转换成TokenPartitionTree即VectorTreeUnwrappedLine。一旦进入TokenPartitionTree形式原始语法结构就被抽象掉了对后续所有格式化阶段不再相关。文档由此引出一个重要的架构推论如果要实现一个不依赖合法语法树的格式化器只需能产出TokenPartitionTree即可复用后续全部机制——例如可以直接从词法 Token 流生成分区树。这种策略能更好地容纳预处理繁重的代码否则会在语法树产生之前就被解析器拒绝代价是需要做一点“伪解析”。语言无关库函数与 Verilog 特定代码的分离原文档明确指出TreeUnwrapper的实现拆分为语言无关的库函数与Verilog 特定代码两部分并给出简化类继承图见文首插图图源 doc/formatter_simplified_class_diagram.png。TreeUnwrapper类利用 Visitor 模式递归处理输入 CST 树// SymbolVisitor is an abstract visitor class from which visitors can be derived // SymbolVisitor only visits a single Symbol, and does not recurse on nodes // // Usage: // SymbolPtr tree ... // SymbolVisitorSubclass visitor; // tree-Accept(visitor); // class SymbolVisitor { public: virtual ~SymbolVisitor() {} virtual void Visit(const SyntaxTreeLeaf leaf) 0; virtual void Visit(const SyntaxTreeNode node) 0; };在 verible/common/text/visitors.h 中可以看到SymbolVisitor只访问单个Symbol且不自动递归递归控制完全交给子类——这正是解包器需要精细控制遍历与分区创建的原因。Verilog 侧的 verilog::formatter::TreeUnwrapperfinal派生类通过一组辅助方法简化构建过程原文档列出的三个关键方法在源码中均有对应实现TraverseChildren()—— 只遍历 CSTVisitIndentedSection()—— 创建缩进节区并遍历 CSTVisitNewUnwrappedLine()—— 开启一个新的 Token 分区并遍历 CST另有VisitNewUnindentedUnwrappedLine()用于 flush-left 构造新建的UnwrappedLine不追加缩进。自定义策略的应用Custom Policies格式化流程的下一阶段是按所选策略对分区树做重塑。Formatter::Format()中有一遍前序遍历ApplyPreOrder按PartitionPolicyEnum分派kAppendFittingSubPartitions调用ReshapeFittingSubpartitions()重塑子分区结构——这是原文档提到的第二个示例策略unwrapped-line.h 注释说明其语义把子分区当作单位能放进同一行就追加否则换行并对齐到第一个元素的位置kJuxtaposition/kStack/kWrap/kJuxtapositionOrIndentedStack交给 LayoutOptimizerOptimizeTokenPartitionTree()注释特别警告一旦这些策略被赋给某个分区其整棵子树都由 LayoutOptimizer 处理kTabularAlignment调用TabularAlignTokenPartitions()后文详述。一个体现“策略决定展开与否”的实现细节在 DeterminePartitionExpansion()以kAppendFittingSubPartitions为例先用FitsOnLine()判断能否压进单行——能则Unexpand()否则Expand()而kTabularAlignment对函数调用kArgumentList有个特殊优化整个调用能放进一行时直接Unexpand()否则才展开做表格对齐。Wrapping换行优化最短路搜索原文档“Wrapping”一节说明换行优化当前通过在“append/wrap 决策空间”上执行Dijkstra 最短路搜索完成搜索跨越一段格式化 Token 区间每当某处采用换行line break优化状态就会计入一个在 Token 标注阶段确定的惩罚值。文档同时坦诚该算法“可扩展性不算很好有计划替换成类似动态规划的实现”。对应源码即 SearchLineWraps()输入一个已标注的UnwrappedLine与样式结构返回一组同等最优的FormattedExcerpt格式化决策已固化。max_search_states限制搜索规模超限时返回一个贪心格式化结果并标记!CompletedFormatting()Formatter::Format()发现这类“未完成”行时会返回ResourceExhaustedErrorformatter.cc。惩罚项由样式参数控制line_break_penalty每引入一个换行的惩罚默认 2与over_column_limit_penalty超过column_limit的基准惩罚默认 100每超 1 字符再加 1定义见 basic-format-style-init.cc。CLI 侧的--max_search_states默认值为 100000见 tools/formatter/README.md。Disable Control 与 Preservation格式禁用区原文档的 “Disable Control and Preservation” 一节标题下的内容较简其完整行为需要结合源码与工具 README 来看用户通过注释指令排除某些文本// verilog_format: off ... untouched code ... // verilog_format: on或块注释形式/* verilog_format: off */ ... /* verilog_format: on */。良好实践是在指令后附上原因例如// verilog_format: off // my alignment is prettier than the tools完整说明见 tools/formatter/README.md。这些指令优先于--lines指定生效。实现上DisableFormattingRanges()comment-controls.h把指令翻译成字节区间集合Formatter::Format()将其并入disabled_ranges_随后 PreserveSpacesOnDisabledTokenRanges() 把禁用区间内的 Token 标记为保留原始空白。SelectLines()--lines参数也是同一机制把“启用格式化的行集合”转成“禁用字节区间”formatter.cc。若某个分区被部分禁用DeterminePartitionExpansion() 会强制展开该分区使子分区之间的空白在Emit()阶段按禁用区逐段处理。故障排查Troubleshootingdoc/formatter.md的排查章节给出了三层递进的诊断手段以下完整保留并补充源码对应关系。1. 查看语法树verible-verilog-syntax --printtree显示源代码的具体语法树表示。许多格式化决策基于语法树节点类型这些类型以kPackageDeclaration这类常量形式出现。2. 查看分区树verible-verilog-format --show_token_partition_tree显示TokenPartitionTree对格式化 Token 区段的划分及相对缩进追加--show_inter_token_info会在每个 Token 前打印更多InterTokenInfo信息间距、换行惩罚等。这两个开关对应ExecutionControl的同名字段在Formatter::Format()中通过TokenPartitionTreePrinter打印后直接停止、不产出格式化结果formatter.cc。3. 详细日志用环境变量VERIBLE_LOGTHRESHOLD0 VERIBLE_VLOG_DETAIL8原理解释VERIBLE_LOGTHRESHOLD0表示要看 INFO 及以上日志四个级别INFO0、WARNING1、ERROR2、FATAL3它们打印到 stderr——不开启的话看不到任何 vlog 输出因为 vlog 走 INFO 级VERIBLE_VLOG_DETAIL8表示记录不超过 8 级详细度的所有VLOG()命令数字越大细节越多。原文档中关于VERIBLE_VLOG_MODULE的引入仍是 TODO 状态。文档给出的一个真实TreeUnwrapper调试示例echo module m; initial a b c; endmodule | \ VERIBLE_LOGTHRESHOLD0 \ VERIBLE_VLOG_DETAIL8 \ bazel run //verible/verilog/tools/formatter:verible-verilog-format -- -show_token_partition_tree -补充两个实战建议均来自仓库文档与代码换行决策存疑时加--show_equally_optimal_wrappings当某分区存在多个同等最优解时会在 stderr 打印对照DisplayEquallyOptimalWrappings()便于调换行惩罚想定位“哪个分区 Token 太多”时用--show_largest_token_partitionsN打印最大的 N 个叶分区及其行号然后退出PrintLargestPartitions()。表格对齐Alignmentdoc/formatter.md把表格对齐功能概括为给定一段语法结构相似的代码块插入所需空格使相同子结构的元素实现垂直对齐。其实现同样拆分为语言无关的库函数与Verilog 特定调用。触发kTabularAlignment 标记要对某段代码触发对齐TreeUnwrapper会在TokenPartitionTree节点上打上 kTabularAlignment 标记这表示该节点的某些子分区“可以”被对齐。第一阶段语言特定Language-specificTokenPartitionTree进入顶层对齐处理器后对齐分两阶段进行。第一阶段取决于每个分区对应的语法树节点类型从一张函数表中选择处理函数由其负责找出 AlignablePartitionGroup——一组可参与对齐格式化的子分区可理解为构成一张“表”的行rows。原文档列出的行为要点在源码中均有体现单个父节点返回的AlignablePartitionGroup可以覆盖不同的语法构造。例如一个表示语句元素的节点下可能既有声明组也有赋值语句组若组跨越了对齐无关的文本如注释AlignablePartitionGroup可能是稀疏填充的每个AlignablePartitionGroup都被赋予一个函数负责把行上的 Token 切成列column单元格AlignmentCellScannerFunction候选对齐组的起止点判定可基于多种因素语法树节点类型、注释、空行等所有未被选入对齐的子分区默认走非对齐格式化。第二阶段语言无关Language-agnostic每个对齐组分析并转换自己的行与列本质上计算每列最大宽度并相应调整InterTokenInfo间距同时考虑左/右对齐flush属性AlignmentColumnProperties的flush_left、left_border_override等见 align.h。要点每行被扫描并切分为将归入各列的单元格这要求各行具有相同或相似的语法结构列可以为空——可选语法构造在表中就是空白单元格为正确分列每个 Token 单元格都被赋予一个键其在父语法树节点内的路径path形如[N,M,P]SyntaxTreePath对应ColumnPositionEntry的键见 align.h。路径的层次性与键的字典序便于容纳每行的空单元格也支持动态列数——例如数据声明的列数取决于维度个数单元格分列形成column schema据此计算列宽列宽最终转化为InterTokenInfo的间距调整。若最终列宽超过列限column_limit样式参数则放弃对齐回退到非对齐格式化——AlignablePartitionGroup::Align(int column_limit)的接口签名align.h即携带该约束。用户侧控制对齐策略与分组边界对齐行为通过一系列--*_alignment标志控制默认全部为inferAlignmentPolicy::kInferUserIntentformat-style-init.cc覆盖端口声明、struct/union 成员、命名参数/端口、模块内 net/variable 声明、形式参数、parameter/localparam 声明、类成员变量、case 项、分布项、赋值语句等上下文。四种取值align.halign—— 强制表格对齐flush-left—— 不做对齐按间距约束左对齐preserve—— 原样保留infer—— 依据原始代码的间距推断作者意图。infer的判定逻辑在 tools/formatter/README.md 中有完整示例对齐与 flush-left 的间距差“足够小”时倾向于对齐若原始代码中的 excess spaces超出最小间距的多余空格低于阈值则推断作者想要 flush-left作者若要对齐需在组内任一行的任意两 Token 之间注入 4 个多余空格来“表态”否则原始代码保持不动。另外--alignment_group_boundary默认none取值{none,blank-lines,separator-comments,blank-lines-and-separator-comments}format-style-init.cc控制空行或分隔注释是否打断对齐组让各子节按各自宽度独立对齐。样式参数速查格式化器风格由两层标志组成BasicFormatStyle语言无关basic-format-style-init.cc与 Verilog 特定的 FormatStyle。常用参数与默认值参数默认值说明--column_limit100格式化时尽量不超过的目标行宽--indentation_spaces2每级缩进增加的空格数--wrap_spaces4每级 wrap 增加的空格数适用于开组后首元素换行的场景--line_break_penalty2每个引入的换行加入解的惩罚--over_column_limit_penalty100超过列宽的基准惩罚每超 1 字符加 1--line_terminatorauto行结束符auto按输入推断也可固定 CR / CRLF--try_wrap_long_linesfalse是否需要换行时让格式化器优化换行决策否则保留原样降低风险的短期措施--alignment_group_boundarynone对齐组边界控制见上文--*_alignment系列infer各上下文对齐策略{align,flush-left,preserve,infer}--*_indentation系列wrap端口/形式参数/命名参数/命名端口的缩进风格{indent,wrap}完整参数列表可直接用verible-verilog-format --helpfull查看或参考 tools/formatter/README.md。收尾failsafe 设计约束了以上所有机制上述各阶段的任何一环失败都会触发 tools/formatter/README.md 所述的安全行为——格式化器绝不能损坏数据词法/解析失败没有语法树可用时放弃输出前做词法等价性检查只允许空白变化与收敛性检查再次格式化无进一步变化换行搜索超出--max_search_states等内部资源限制时放弃且只有在全部内部验证通过后才打开文件写入——任何崩溃都会保持原文件完整。理解这一点也解释了本文各阶段为何被设计成“可诊断、可提前停止”ExecutionControl::AnyStop()。小结doc/formatter.md描绘的 Verible 格式化器架构可以概括为一条清晰的流水线词法 Token → InterTokenInfo 标注规则 reason→ TokenPartitionTreeVisitor 解包→ 分区策略重塑对齐/布局/子分区折叠→ 最短路换行搜索 → 等价性与收敛性校验。语言无关的通用库verible/common/formatting/承担表示与优化Verilog 特定层verible/verilog/formatting/承担标注规则、分区策略选择与对齐扫描。排查问题时从--printtree、--show_token_partition_tree --show_inter_token_info到VERIBLE_LOGTHRESHOLD0 VERIBLE_VLOG_DETAIL8的组合可以逐层逼近决策发生的具体规则与代码位置。赞分享开发工具Lint静态分析硬件开发【免费下载链接】veribleVerible is a suite of SystemVerilog developer tools, including a parser, style-linter, formatter and language server项目地址https://gitcode.com/gh_mirrors/ve/verible点击查看免费下载相关推荐Canopy 区块链跨链 Token 兑换Token Swap状态机实现深度解析Canopy 区块链跨链 Token 兑换Token Swap状态机实现深度解析 本文以 fsm/swap.md https://link.gitcode.区块链后端Verible项目中的SystemVerilog解析器设计解析Verible项目中的SystemVerilog解析器设计解析 前言 在数字电路设计和验证领域SystemVerilog作为一门复杂的硬件描述和验证语言其解开发工具Lint静态分析硬件开发Docker Swarm Join Token 管理实战深入解析 docker swarm join-token 命令Docker Swarm Join Token 管理实战深入解析 docker swarm join token 命令 导读 本文围绕 Docker CE 中容器运行时云原生创作声明:本文部分内容由AI辅助生成(AIGC),仅供参考