Posts

For your reference, below are the scripts I used for yosys. Verilog to Btor2: read_verilog -formal <verilog-file> prep -top <top-module> flatten memory -nomap hierarchy -check setundef -undriven -init -expose sim -clock <clock-name> -reset <reset-name> -rstlen <reset-cycle> -n <simulation-cycle> -w <top-module> write_btor -s <btor-name> For memory command, use memory -nomap if you want to keep array sort in Btor2, otherwise, use memory or memory -nordff to “word-blast” Verilog array.

(Credit to Justin Patel) It is possible that vvp simulations get stuck and never finish. This post is about why the problem is happening and what you can do to fix it.

(Credit to Justin Patel) Use the always @(*) block for combinational logic only. The reg types that you assign to in an always @(*) block are simply wires driven by the output of combinational logic blocks (i.