
[tasks]
rv32_prove prove rv32   sboxes_1
rv32_cover cover rv32   sboxes_1
rv64_4_prove prove rv64 sboxes_4
rv64_4_cover cover rv64 sboxes_4
rv64_8_prove prove rv64 sboxes_8
rv64_8_cover cover rv64 sboxes_8

[options]
sboxes_1: depth 5
sboxes_4: depth 6
sboxes_8: depth 5

prove: mode bmc
cover: mode cover
timeout 7200

[engines]
smtbmc boolector

[script]
rv32: verilog_defaults -add -DXLEN=32 
rv64: verilog_defaults -add -DXLEN=64 

sboxes_1: verilog_defaults -add -DSBOXES=1
sboxes_4: verilog_defaults -add -DSBOXES=4
sboxes_8: verilog_defaults -add -DSBOXES=8


read_verilog -formal riscv_crypto_fu.v
read_verilog -formal riscv_crypto_fu_aes_mix_columns.v
read_verilog -formal riscv_crypto_fu_lut4.v
read_verilog -formal riscv_crypto_fu_saes32.v
read_verilog -formal riscv_crypto_fu_saes64.v
read_verilog -formal riscv_crypto_fu_sboxes.v
read_verilog -formal riscv_crypto_fu_ssm3.v
read_verilog -formal riscv_crypto_fu_ssha256.v
read_verilog -formal riscv_crypto_fu_ssha512.v
read_verilog -formal riscv_crypto_fu_ssm4.v
read_verilog -formal riscv_crypto_fu_saes32_ssm4.v
read_verilog -formal tb_checker_saes32.v
read_verilog -formal tb_checker_saes64.v
read_verilog -formal tb_checker_ssm4.v
read_verilog -formal tb_checker_lut4_rv32.v
read_verilog -formal tb_checker_lut4_rv64.v
read_verilog -formal tb_riscv_crypto_fu.v

prep -top tb_riscv_crypto_fu

[files]
crypto-fu/riscv_crypto_fu.v
crypto-fu/riscv_crypto_fu_aes_mix_columns.v
crypto-fu/riscv_crypto_fu_lut4.v
crypto-fu/riscv_crypto_fu_saes32.v
crypto-fu/riscv_crypto_fu_saes64.v
crypto-fu/riscv_crypto_fu_sboxes.v
crypto-fu/riscv_crypto_fu_ssm3.v
crypto-fu/riscv_crypto_fu_ssha256.v
crypto-fu/riscv_crypto_fu_ssha512.v
crypto-fu/riscv_crypto_fu_ssm4.v
crypto-fu/riscv_crypto_fu_saes32_ssm4.v
crypto-fu/tb_checker_saes32.v
crypto-fu/tb_checker_saes64.v
crypto-fu/tb_checker_ssm4.v
crypto-fu/tb_checker_saes.vh
crypto-fu/tb_checker_lut4_rv32.v
crypto-fu/tb_checker_lut4_rv64.v
crypto-fu/tb_riscv_crypto_fu.v


