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, which compares the circuits structurally and logically. Alternatively, Yosys provides two internal ways to check equivalence:

• Yosys can create a miter module (throwing the original and new circuits together and compare outputs), for which it tries to find differing behavior, in which case the inequality is proven
• Yosys provides a collection of equiv_ passes that try to prove equivalence via temporal induction This notebook demonstrates how to use these different approaches 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 = <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}')

Comparing two Circuit objects¶

• The Circuit class comes with a prove_equivalence() method that takes another circuit
• The main circuit is treated as the gold circuit (golden reference), and the parameter of the prove_equivalence() method is the gate circuit (gate-level circuit)
• The function returns a subprocess.Popen object, containing data about the run
• If the quiet parameter is True, the output is delegated to stdout of the subprocess.Popen object and can be accesssed afterwards

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', quiet=False)

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', quiet=False)

• Alternatively, two RTL files can also be given by using the netlist_carpentry.run_eqy() function
• 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.
• run_eqy() returns a subprocess.Popen object, containing data about the run

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 [ ]:

from netlist_carpentry import run_eqy

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'

proc = run_eqy(gold_design=original_file_path, gate_design=modified_file_path, gold_top=base_name, gate_top=base_name, script_path=eqy_script_path, output_path='files/eqy/out', overwrite=True, quiet=True)

from netlist_carpentry import run_eqy 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' proc = run_eqy(gold_design=original_file_path, gate_design=modified_file_path, gold_top=base_name, gate_top=base_name, script_path=eqy_script_path, output_path='files/eqy/out', overwrite=True, quiet=True)

Handling the returned object¶

• stdout contains the standard output from the run, and is empty (i.e. None) if quiet=False, since the output is directly printed to the console
• stderr contains errors if any occur
• returncode indicates whether the equivalence could be proven or not

In [ ]:

print(proc.stdout)  # Prints the output of the equivalence checking process to the console, which was stored in the stdout attribute because quiet=True
if proc.returncode == 0:
    print("\n\tThe designs are logically equivalent.")
else:
    print(f"\n\tThe equivalence check failed with return code {proc.returncode}")
    print("These are the errors:")
    print(proc.stderr)

print(proc.stdout) # Prints the output of the equivalence checking process to the console, which was stored in the stdout attribute because quiet=True if proc.returncode == 0: print("\n\tThe designs are logically equivalent.") else: print(f"\n\tThe equivalence check failed with return code {proc.returncode}") print("These are the errors:") print(proc.stderr)

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 [ ]:

from netlist_carpentry.scripts.equivalence_checking import EquivalenceChecking

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)

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

from netlist_carpentry.scripts.equivalence_checking import EquivalenceChecking 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) result = eqy_tool_wrapper.run_eqy('files/eqy/out', overwrite=True) if result.returncode == 0: print("The designs are logically equivalent.") else: print(f"The equivalence check failed with return code {result.returncode}")

Proving equivalence using Yosys's internal equiv passes¶

• The equiv_ passes form an internal equivalence checking solution
• The primary purpose is for proving corresponding internal signals
• This is best for very similar designs, where there are probably only very few discrepancies, for debugging
• In the cell below, this is shown again for the already introduced files from above

In [ ]:

from netlist_carpentry import run_equiv

proc = run_equiv(gold_design=original_file_path, gate_design=modified_file_path, gold_top=base_name, gate_top=base_name, quiet=True)

if proc.returncode == 0:
    print("Using the 'equiv_' passes, the designs are proven to be logically equivalent.")
else:
    print(f"The equivalence check failed with return code {proc.returncode}")
    print("These are the errors:")
    print(proc.stderr)

print("This was the standard output of the equivalence checking process:")
print(proc.stdout)

from netlist_carpentry import run_equiv proc = run_equiv(gold_design=original_file_path, gate_design=modified_file_path, gold_top=base_name, gate_top=base_name, quiet=True) if proc.returncode == 0: print("Using the 'equiv_' passes, the designs are proven to be logically equivalent.") else: print(f"The equivalence check failed with return code {proc.returncode}") print("These are the errors:") print(proc.stderr) print("This was the standard output of the equivalence checking process:") print(proc.stdout)

Proving equivalence using a miter module¶

• Yosys also provides the option to create a miter module, which transforms the equivalence proof into a single verification property
  • This means, Yosys XORs all outputs of the gold design and the gate design, and checks if at least one of these outputs can ever be 1
  • For example if DATA_O_gold XOR DATA_O_gate == 0 for every valid input combination, this means there is no trigger that would result in different behavior between both designs
  • If for example there is an input ENABLE_I, and Yosys sets ENABLE_I_gold = ENABLE_I_gate = 1, and this would result in DATA_O_gold = 0 and DATA_O_gate = 1, then the XOR comparison would bring a 1, indicating that there are discrepancies in the design, but it cannot show, where the source of this issue is
• This is ideal for a generic equivalence check, or to retrieve a concrete counterexamples, if the designs actually differ
• So, the miter approach is ideal for checking if two designs are equivalent (along with a concrete fail-case example), but it WILL NOT HELP if the question is WHERE the equivalence gets lost and the circuits start to differ

In [ ]:

from netlist_carpentry import run_equiv_miter

proc = run_equiv_miter(gold_design=original_file_path, gate_design=modified_file_path, gold_top=base_name, gate_top=base_name, quiet=True)


if proc.returncode == 0:
    print("Using the miter module approach, the designs are proven to be logically equivalent.")
else:
    print(f"The equivalence check failed with return code {proc.returncode}")
    print("These are the errors:")
    print(proc.stderr)

print("This was the standard output of the equivalence checking process:")
print(proc.stdout)

from netlist_carpentry import run_equiv_miter proc = run_equiv_miter(gold_design=original_file_path, gate_design=modified_file_path, gold_top=base_name, gate_top=base_name, quiet=True) if proc.returncode == 0: print("Using the miter module approach, the designs are proven to be logically equivalent.") else: print(f"The equivalence check failed with return code {proc.returncode}") print("These are the errors:") print(proc.stderr) print("This was the standard output of the equivalence checking process:") print(proc.stdout)