<commit_before>#!/usr/bin/env python3
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
r"""Command-line tool to perform LEC on all AES S-Box implementations using Yosys

"""
import glob
import os
import subprocess
import sys


def replace_module_name(file_name, string_search, string_replace):
    fin = open(file_name, 'rt')
    data = fin.read()
    data = data.replace(string_search, string_replace)
    fin.close()
    fin = open(file_name, 'wt')
    fin.write(data)
    fin.close()


rtl_path = '../../rtl/'

# List all S-Box reference implementation + AES package
impl_gold = 'aes_sbox_lut'
file_pkg = 'aes_pkg.sv'
file_pkg_canright = 'aes_sbox_canright_pkg'

# Detect all S-Box implementations to check
impl_list = glob.glob(rtl_path + 'aes_sbox_*.sv')
impl_list = [
    impl_dut.replace(rtl_path, '').replace('.sv', '') for impl_dut in impl_list
]
# Remove multicycle implementations, we can't perform LEC for those.
impl_list.remove('aes_sbox_dom')
# Remove reference implementation and package files.
impl_list.remove(impl_gold)
impl_list.remove(file_pkg_canright)
file_pkg_canright = file_pkg_canright + '.sv'

# Create workdir
os.makedirs('scratch', exist_ok=True)

# Convert the reference implementation to Verilog
sv2v_cmd = ['sv2v', rtl_path + impl_gold + '.sv', rtl_path + file_pkg]
with open('scratch/aes_sbox_ref.v', 'w') as outfile:
    subprocess.run(sv2v_cmd, stdout=outfile)

# Change module name
replace_module_name('scratch/aes_sbox_ref.v', impl_gold, 'aes_sbox_ref')

print('Running LEC on ' + str(len(impl_list)) + ' S-Box implementation(s)...')

# Check every implementation separately
num_impl_success = 0
num_impl_failed = 0
for impl_dut in impl_list:

    # Prepare Verilog conversion of DUT
    sv2v_cmd = [
        'sv2v', rtl_path + impl_dut + '.sv', rtl_path + file_pkg,
        rtl_path + file_pkg_canright
    ]

    # Masked implementations require a wrapper
    if 'masked' in impl_dut:
        file_wrap = 'aes_sbox_masked_wrapper.sv'

        # Copy the wrapper
        os.system('cp ' + file_wrap + ' scratch/' + file_wrap)

        # Change module name
        replace_module_name('scratch/' + file_wrap, 'aes_sbox_masked',
                            impl_dut)

        # Include in conversion
        sv2v_cmd.insert(2, 'scratch/' + file_wrap)

    # Convert DUT to Verilog
    with open('scratch/aes_sbox_dut.v', 'w') as outfile:
        subprocess.run(sv2v_cmd, stdout=outfile)

    # Change module name
    if 'masked' in impl_dut:
        replace_module_name('scratch/aes_sbox_dut.v', impl_dut + '_wrapper',
                            'aes_sbox_dut')
    else:
        replace_module_name('scratch/aes_sbox_dut.v', impl_dut, 'aes_sbox_dut')

    # Perform LEC in Yosys
    yosys_cmd = ['yosys', '../aes_sbox_lec.ys']
    lec_log = 'scratch/' + impl_dut + '_lec.log'
    with open(lec_log, 'w') as outfile:
        subprocess.run(yosys_cmd, cwd="scratch", stdout=outfile)

    # Get actual LEC output
    lec_string = 'Trying to prove $equiv'<commit_msg>[aes] Fix and realign LEC script for the different combinational S-Boxes<commit_after>#!/usr/bin/env python3
# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0
r"""Command-line tool to perform LEC on all AES S-Box implementations using Yosys

"""
import glob
import os
import subprocess
import sys
from pathlib import Path


def replace_module_name(file_name, string_search, string_replace):
    fin = open(file_name, 'rt')
    data = fin.read()
    data = data.replace(string_search, string_replace)
    fin.close()
    fin = open(file_name, 'wt')
    fin.write(data)
    fin.close()


path_root = str(Path(__file__).resolve().parents[5])
rtl_path = path_root + '/hw/ip/aes/rtl/'
prim_path = path_root + '/hw/ip/prim/rtl/'
prim_xilinx_path = path_root + '/hw/ip/prim_xilinx/rtl/'

# Specify S-Box reference implementation
impl_gold = 'aes_sbox_lut'
file_pkg = 'aes_pkg.sv'

# Specify dependencies
dep_list = [
    rtl_path + 'aes_pkg.sv',
    rtl_path + 'aes_reg_pkg.sv',
    rtl_path + 'aes_sbox_canright_pkg.sv',
    prim_xilinx_path + 'prim_xilinx_buf.sv',
    prim_xilinx_path + 'prim_xilinx_xor2.sv',
]

# Detect all S-Box implementations to check
impl_list = glob.glob(rtl_path + 'aes_sbox_*.sv')
impl_list = [
    impl_dut.replace(rtl_path, '').replace('.sv', '') for impl_dut in impl_list
]
# Remove multicycle implementations, we can't perform LEC for those.
impl_list.remove('aes_sbox_dom')
# Remove reference implementation and package files.
impl_list.remove(impl_gold)
impl_list.remove('aes_sbox_canright_pkg')

# Create workdir
os.makedirs('scratch', exist_ok=True)

# Convert the reference implementation to Verilog
sv2v_cmd = ['sv2v', '-I', prim_path
            ] + dep_list + [rtl_path + impl_gold + '.sv']
with open('scratch/aes_sbox_ref.v', 'w') as outfile:
    subprocess.run(sv2v_cmd, stdout=outfile)

# Change module name
replace_module_name('scratch/aes_sbox_ref.v', impl_gold, 'aes_sbox_ref')

print('Running LEC on ' + str(len(impl_list)) + ' S-Box implementation(s)...')

# Check every implementation separately
num_impl_success = 0
num_impl_failed = 0
for impl_dut in impl_list:

    # Prepare Verilog conversion of DUT
    sv2v_cmd = ['sv2v', '-I', prim_path
                ] + dep_list + [rtl_path + impl_dut + '.sv']

    # Masked implementations require a wrapper
    if 'masked' in impl_dut:
        file_wrap = 'aes_sbox_masked_wrapper.sv'

        # Copy the wrapper
        os.system('cp ' + file_wrap + ' scratch/' + file_wrap)

        # Change module name
        replace_module_name('scratch/' + file_wrap, 'aes_sbox_masked',
                            impl_dut)

        # Include in conversion
        sv2v_cmd.insert(3, 'scratch/' + file_wrap)

    # Convert DUT to Verilog
    with open('scratch/aes_sbox_dut.v', 'w') as outfile:
        subprocess.run(sv2v_cmd, stdout=outfile)

    # Change module name
    if 'masked' in impl_dut:
        replace_module_name('scratch/aes_sbox_dut.v', impl_dut + '_wrapper',
                            'aes_sbox_dut')
    else:
        replace_module_name('scratch/aes_sbox_dut.v', impl_dut, 'aes_sbox_dut')

    # Use Xilinx implementation for primitives
    replace_module_name('scratch/aes_sbox_dut.v', 'prim_xilinx_', 'prim_')

    # Perform LEC in Yosys
    yosys_cmd = ['yosys', '../aes_sbox_lec.ys']
    lec_log = 'scratch/' + impl_dut + '_lec.log'
    with open(lec_log, 'w') as outfile:
        subprocess.run(yosys_cmd, cwd="scratch", stdout=outfile)

    # Get actual LEC output
    lec_string = 'Trying to prove $equiv'
{'fraction_non_alphanumeric': 0.11563105349426316, 'fraction_numerical': 0.0047682908657428105, 'mean_word_length': 3.6130584192439863, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3511516', 'n_tokens_mistral': 2484, 'n_tokens_neox': 2374, 'n_words': 545}