How to convert Verilog to btor2 or aiger format

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.

Verilog to AIGER

read_verilog -formal <verilog-file>
prep -top <top-module>
flatten
memory -nordff
setundef -undriven -init -expose
sim -clock <clock-name> -reset <reset-name> -rstlen <reset-cycle> -n <simulation-cycle> -w <top-module>
delete -output
techmap
abc -fast -g AND
write_aiger -zinit <aiger-file>

The option -zinit is usually not necessary (it creates an equivalent circuit where all flip-flops are initialized to 0), unless you need to interprete the inductive invariant generated by the pdr command from abc. delete -output is necessary as it removes the original output which could mess up with the output of bad states and constraints used in AIGER.