Issue with Generating bad Statements in BTOR2 Files Using Yosys

[EPTansuo]

Hello,

I am using Yosys to convert Verilog files into BTOR2 format. Below is the Tcl script I'm currently using:

set VSRC [lindex $argv 0]
set TOP   [lindex $argv 1]
set OUT   [lindex $argv 2]

yosys -import

read_verilog -sv -formal ${VSRC};
prep -top ${TOP};
hierarchy -check;
chformal -assume -early;
memory -nomap;
flatten;
setundef -undriven -expose;

write_btor $OUT

show

In my Verilog/SystemVerilog code, I have assertions like this:

  always @* begin
      assert(var < 6);
   end

But I can not find any bad statement in btor2 file.

However, I am unable to find any bad statements in the generated BTOR2 file, which should appear as:

xxx bad xxx

Could you please help me understand why the bad statements are not being generated and how I can resolve this issue?

Thank you for your assistance.

[KrystalDelusion]

Does the btor output from SBY do what you're after?

[EPTansuo]

Thanks. I've solved this problem. I was able to solve this problem using the following shell script instead of the yosys script:

#!/usr/bin/bash

help(){
        echo "v2btor2-0.43 <verlog file> <top name> <output file>"
}

if [ $# -ne 3 ];
then
        help
        exit 1
fi

VSRC=$1
TOP=$2
OUT=$3

echo "read -formal ${VSRC};" \
        "prep -top ${TOP};" \
        "hierarchy -check;" \
        "chformal -assume -early;" \
        "memory -nomap;" \
        "flatten;" \
        "setundef -undriven -expose;" \
        "write_btor ${OUT};" | yosys