如何依据IEEE-1800.2017标准判断Verilog代码是否存在竞态条件

这段SystemVerilog代码存在竞态条件，依据IEEE-1800.2017标准的调度语义与并发块规则可如下判断：

核心逻辑拆解 #

代码中fork-join_any启动了两个无延迟、无事件控制的并发分支：

• 分支1：if (a) $display("FOO")，因a=0，分支体内语句不会执行，分支直接完成
• 分支2：if (b) $display("ZIG")，因b=1，分支会执行$display后完成

join_any会在任意一个分支完成时触发后续代码（disable fork和$display("BAR")），而disable fork会终止fork块中所有尚未完成的分支。

标准条款的关键依据 #

1. 并发块执行顺序（IEEE-1800.2017第9.3节）：
   fork块内的并发语句属于同一时间步的执行单元，标准明确规定：同一时间步内并发语句的执行顺序由模拟器实现定义，不存在强制固定顺序。

2. 调度语义（IEEE-1800.2017第4章）：
   无延迟的立即执行语句会被放入Active队列执行，同一队列内的语句执行顺序不确定。这意味着两种合法执行路径：

   • 模拟器先执行分支1：分支1直接完成，触发join_any，随后disable fork终止未执行的分支2，最终仅输出BAR
   • 模拟器先执行分支2：分支2执行$display("ZIG")后完成，触发join_any时分支1已完成，disable fork无作用，最终输出ZIG和BAR

关于VCS的表现 #

你观察到VCS总是输出BAR，这是VCS实现时选择了先执行分支1的顺序，但该实现行为不代表代码无竞态——换用其他符合标准的模拟器，或调整VCS编译/运行选项，完全可能出现输出ZIG+BAR的情况。

内容的提问来源于stack exchange，提问作者RayaneCTX