A symbolic approach for detecting conflicts in Verilog´s non blocking assignments

In Verilog programs, multiple non blocking assignments (NBA) to the same signal in an identical always structure may introduce conflicts and nondeterministic behaviors. It is a severe design flaw. In this paper, we propose a control flow graph based symbolic approach for detecting conflicts caused by non blocking assignments. This approach applies the static analysis method on the parallel nature of Verilog programs, and adopts the Multi-valued Decision Diagram (MDD) to symbolically encode the reachability conditions with flexibility and efficiency. Our static analysis approach shows valid results from our tests.