Checking the Logical Equivalence of Two Verilog Designs¶

When optimizing circuit designs, it is important to ensure that the changes do not introduce unintended behavior or alter the behavior of the circuit. One way to verify this is by checking if two circuits are logically equivalent. This can be done by the Yosys plugin EQY. This notebook demonstrates how to use EQY to check for logical equivalence between two Verilog designs.

Checking EQY Installation¶

• The Yosys Plugin EQY is required for the execution of a logical equivalence check.
• You can find more information regarding EQY as well as an installation guide on this site.
• Execute the cell below to check whether Jupyter is able to find the installation.

In [ ]:

import shutil

yosys_path = shutil.which('eqy')
if yosys_path is None:
    raise OSError(
        'EQY was not found!\n\tIf EQY is not installed, please install it first.\n\tAlternatively, if EQY is installed and Jupyter was just unable to find EQY, please add EQY to your PATH variable.\n\tYou could do this at the beginning of each notebook:\n\n\t\timport os\n\n\t\tcustom_eqy_prog_path = <path_to_your_eqy_installation>\n\t\tos.environ["PATH"] += os.pathsep + custom_eqy_prog_path\n\n\tTo find the path to your EQY installation run "which eqy" in a terminal!'
    )
else:
    print(f'Successfully found EQY! This is the path to EQY: {yosys_path}')

import shutil yosys_path = shutil.which('eqy') if yosys_path is None: raise OSError( 'EQY was not found!\n\tIf EQY is not installed, please install it first.\n\tAlternatively, if EQY is installed and Jupyter was just unable to find EQY, please add EQY to your PATH variable.\n\tYou could do this at the beginning of each notebook:\n\n\t\timport os\n\n\t\tcustom_eqy_prog_path = \n\t\tos.environ["PATH"] += os.pathsep + custom_eqy_prog_path\n\n\tTo find the path to your EQY installation run "which eqy" in a terminal!' ) else: print(f'Successfully found EQY! This is the path to EQY: {yosys_path}')

Generating EQY script¶

• The first step is to generate an EQY script based on a specific location where the script will be saved, as well as the paths to the original Verilog files and the modified files (along with the names of their top modules).
• The gold and gate are the two files that will be compared.
• The gold is the original file (golden reference), and gate (gate-level netlist) is the modified file.
• Execute the cell below to create the EQY configuration file at the specified path for the two versions of the design.

In [ ]:

import netlist_carpentry

base_name = 'simpleAdder'
original_circuit = netlist_carpentry.read(f'files/{base_name}.v', circuit_name="gold")
modified_circuit = netlist_carpentry.read('output/adder_output.v', circuit_name="gate")

original_circuit.prove_equivalence(modified_circuit, 'files/eqy/out')  # Somehow, eqy currently does not accept it this way. The other ways work fine, though

import netlist_carpentry base_name = 'simpleAdder' original_circuit = netlist_carpentry.read(f'files/{base_name}.v', circuit_name="gold") modified_circuit = netlist_carpentry.read('output/adder_output.v', circuit_name="gate") original_circuit.prove_equivalence(modified_circuit, 'files/eqy/out') # Somehow, eqy currently does not accept it this way. The other ways work fine, though

In [ ]:

from netlist_carpentry.scripts.equivalence_checking import EquivalenceChecking

base_name = 'simpleAdder'
original_file_path = f'files/{base_name}.v'
modified_file_path = 'output/adder_output.v'

eqy_script_path = 'files/eqy/generated_eqy_script.eqy'
eqy_tool_wrapper = EquivalenceChecking([original_file_path], base_name, [modified_file_path], base_name, eqy_script_path)

eqy_tool_wrapper.run_eqy()

from netlist_carpentry.scripts.equivalence_checking import EquivalenceChecking base_name = 'simpleAdder' original_file_path = f'files/{base_name}.v' modified_file_path = 'output/adder_output.v' eqy_script_path = 'files/eqy/generated_eqy_script.eqy' eqy_tool_wrapper = EquivalenceChecking([original_file_path], base_name, [modified_file_path], base_name, eqy_script_path) eqy_tool_wrapper.run_eqy()

Running the Equivalence Check¶

• The generated file can either be executed in the terminal via eqy <eqy_script_path> -d <output_path> or via EqyWrapper.run_eqy(<output_path>).
• The specified target output directory must not exist beforehand.
• Any contents in this folder will be overwritten.
• The directory parameter is optional and defaults to the current working directory if not specified.
• Execute the cell below to run the generated script to check the logical equivalence of both Verilog circuits.

Info: The equivalence checking process may take multiple minutes for larger designs. In this notebook, however, the equivalence check is performed on a small design only containing a decentral mux. Thus, the process should be finished within seconds.

In [ ]:

return_code = eqy_tool_wrapper.run_eqy('files/eqy/out', overwrite=True)
if return_code == 0:
    print("The designs are logically equivalent.")
else:
    print(f"The equivalence check failed with return code {return_code}")

return_code = eqy_tool_wrapper.run_eqy('files/eqy/out', overwrite=True) if return_code == 0: print("The designs are logically equivalent.") else: print(f"The equivalence check failed with return code {return_code}")

Using a Custom Script for Equivalence Check Execution¶

• If the generated script is not suitable for a given use case, a custom .eqy script can be provided and used as well.
• In the cell below, a custom script eqy/example_script.eqy is used, which was created manually (as can be seen by the comments in the file).
• The script matches the original simpleAdder.v file against the read (and unmodified) output design output/adder_output.v and proves logical equality.
• Execute the cell below to run the equivalence check on these two designs.

Info: The parameter overwrite is set to True, which means that if the output directory already exists, it will be overwritten. If the directory exists, and the parameter is False or omitted, the equivalence checking script will fail with a corresponding error message.

In [ ]:

eqy_script_path2 = 'files/eqy/example_script.eqy'
eqy_tool_wrapper = EquivalenceChecking([original_file_path], base_name, [modified_file_path], base_name, eqy_script_path2)

return_code = eqy_tool_wrapper.run_eqy('files/eqy/out', overwrite=True)
if return_code == 0:
    print("The designs are logically equivalent.")
else:
    print(f"The equivalence check failed with return code {return_code}")

eqy_script_path2 = 'files/eqy/example_script.eqy' eqy_tool_wrapper = EquivalenceChecking([original_file_path], base_name, [modified_file_path], base_name, eqy_script_path2) return_code = eqy_tool_wrapper.run_eqy('files/eqy/out', overwrite=True) if return_code == 0: print("The designs are logically equivalent.") else: print(f"The equivalence check failed with return code {return_code}")