Skip to content

netlist_carpentry.scripts.equivalence_checking

Module for handling equivalence checks with Yosys EQY.

Classes:

  • EquivalenceChecking –

    Wrapper class for executing equivalence checks via Yosys EQY to prove the logical equivalence of two Verilog designs.

Functions:

  • run_eqy –

    Runs the Yosys EQY tool to prove the logical equivalence of the Verilog designs for the given Verilog designs.

  • run_equiv –

    Runs a predefined script using the equiv_* passes from Yosys to prove the logical equivalence of the Verilog designs for the given Verilog designs.

  • run_equiv_miter –

    Runs a predefined script to prove the logical equivalence for the given Verilog designs using a miter/SAT approach in Yosys.

EquivalenceChecking 

EquivalenceChecking(
    gold_vfile_paths: List[str],
    gold_top_module: Optional[str],
    gate_vfile_paths: List[str],
    gate_top_module: Optional[str],
    script_path: str,
)

Wrapper class for executing equivalence checks via Yosys EQY to prove the logical equivalence of two Verilog designs. It handles all setup and execution of the equivalence checks and provides methods for running them.

Parameters:

  • script_path

    (str) –

    The path (including the desired file name) to the directory where the .eqy script will be saved.

  • gold_vfile_paths

    (List[str]) –

    A list of paths to the gold Verilog files.

  • gold_top_module

    (Optional[str]) –

    The top module name for the gold design. If None, module is auto-selected.

  • gate_vfile_paths

    (List[str]) –

    A list of paths to the gate Verilog files.

  • gate_top_module

    (Optional[str]) –

    The top module name for the gate design. If None, module is auto-selected.

Methods:

  • run_eqy –

    Runs the Yosys EQY tool to prove the logical equivalence of the Verilog designs for the given Verilog designs.

Attributes:

  • gold_vfile_paths –

    A list of paths to the gold Verilog files.

  • gold_top_module –

    The top module name for the gold design. If None, module is auto-selected.

  • gate_vfile_paths –

    A list of paths to the gate Verilog files.

  • gate_top_module –

    The top module name for the gate design. If None, module is auto-selected.

  • script_path –

    The path to the directory where the .eqy script will be saved.

  • formatted_template (str) –

    Formats the EQY template string with the provided input parameters.

gold_vfile_paths instance-attribute 

gold_vfile_paths = gold_vfile_paths

A list of paths to the gold Verilog files.

gold_top_module instance-attribute 

gold_top_module = gold_top_module

The top module name for the gold design. If None, module is auto-selected.

gate_vfile_paths instance-attribute 

gate_vfile_paths = gate_vfile_paths

A list of paths to the gate Verilog files.

gate_top_module instance-attribute 

gate_top_module = gate_top_module

The top module name for the gate design. If None, module is auto-selected.

script_path instance-attribute 

script_path = Path(script_path)

The path to the directory where the .eqy script will be saved.

formatted_template property 

formatted_template: str

Formats the EQY template string with the provided input parameters.

The gold Verilog files are the golden reference design files, while the gate Verilog files are the synthesized (gate-level) designs. In the scope of this framework, the gate designs refer to the modified or optimized versions of the original designs.

Parameters:

  • gold_vfile_paths

    (List[str]) –

    A list of paths to the gold Verilog files.

  • gold_top_module

    (Optional[str]) –

    The top module name for the gold design. If None, module is auto-selected.

  • gate_vfile_paths

    (List[str]) –

    A list of paths to the gate Verilog files.

  • gate_top_module

    (Optional[str]) –

    The top module name for the gate design. If None, module is auto-selected.

Returns:

  • str ( str ) –

    The formatted EQY template string.

run_eqy 

run_eqy(
    output_path: Optional[str] = None,
    overwrite: bool = False,
    quiet: bool = False,
) -> Popen[str]

Runs the Yosys EQY tool to prove the logical equivalence of the Verilog designs for the given Verilog designs.

The gold Verilog files are the golden reference design files, while the gate Verilog files are the synthesized (gate-level) designs. In the scope of this framework, the gate designs refer to the modified or optimized versions of the original designs.

The script for the equivalence check is the one specified in the path attribute of this class.

If the parameter overwrite is set to True and the output directory exists already, 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.

Parameters:

  • output_path

    (Optional[str], default: None ) –

    The path to the directory where the EQY tool will be executed. If None, executes the equivalence check in a temporary directory. Defaults to None.

  • overwrite

    (bool, default: False ) –

    Whether to overwrite the output directory if it already exists. Only has an effect, if an output_path is provided. Defaults to False.

  • quiet

    (bool, default: False ) –

    If True, pipes all Yosys output into the subprocess.CompletedProcess object. If False, prints all Yosys output to the console. Defaults to False.

Returns:

  • Popen[str] –

    subprocess.CompletedProcess: The result of the execution plus some metadata.

run_eqy 

run_eqy(
    gold_design: Circuit,
    gate_design: Circuit,
    *,
    script_path: Optional[str] = None,
    output_path: Optional[str] = None,
    overwrite: bool = False,
    quiet: bool = False
) -> Popen[str]

run_eqy(
    gold_design: Union[str, Path, List[str]],
    gate_design: Union[str, Path, List[str]],
    gold_top: Optional[str] = None,
    gate_top: Optional[str] = None,
    *,
    script_path: Optional[str] = None,
    output_path: Optional[str] = None,
    overwrite: bool = False,
    quiet: bool = False
) -> Popen[str]

run_eqy(
    gold_design: Union[Circuit, str, Path, List[str]],
    gate_design: Union[Circuit, str, Path, List[str]],
    gold_top: Optional[str] = None,
    gate_top: Optional[str] = None,
    *,
    script_path: Optional[str] = None,
    output_path: Optional[str] = None,
    overwrite: bool = False,
    quiet: bool = False
) -> Popen[str]

Runs the Yosys EQY tool to prove the logical equivalence of the Verilog designs for the given Verilog designs.

The gold Verilog files are the golden reference design files, while the gate Verilog files are the synthesized (gate-level) designs. In the scope of this framework, the gate designs refer to the modified or optimized versions of the original designs.

The script for the equivalence check is the one specified in the path attribute of this class.

If the parameter overwrite is set to True and the output directory exists already, 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.

Parameters:

  • gold_design

    (Union[Circuit, str, Path, List[str]]) –

    The circuit object, or the file path(s) to the gold Verilog file(s).

  • gate_design

    (Union[Circuit, str, Path, List[str]]) –

    The circuit object, or the file path(s) to the gate Verilog file(s).

  • gold_top

    (Optional[str], default: None ) –

    The top module name for the gold design. If None, module is auto-selected.

  • gate_top

    (Optional[str], default: None ) –

    The top module name for the gate design. If None, module is auto-selected.

  • script_path

    (Optional[str], default: None ) –

    The path (including the desired file name) to the directory where the .eqy script will be saved.

  • output_path

    (Optional[str], default: None ) –

    The path to the directory where the EQY tool will be executed. If None, executes the equivalence check in a temporary directory. Defaults to None.

  • overwrite

    (bool, default: False ) –

    Whether to overwrite the output directory if it already exists. Only has an effect, if an output_path is provided. Defaults to False.

  • quiet

    (bool, default: False ) –

    If True, pipes all Yosys output into the subprocess.CompletedProcess object. If False, prints all Yosys output to the console. Defaults to False.

Returns:

  • Popen[str] –

    subprocess.CompletedProcess: The result of the execution plus some metadata.

run_equiv 

run_equiv(
    gold_design: Circuit,
    gate_design: Circuit,
    *,
    quiet: bool = False,
    out_dir: Optional[str] = None,
    no_name_matching: bool = False
) -> Popen[str]

run_equiv(
    gold_design: Union[str, Path, List[str]],
    gate_design: Union[str, Path, List[str]],
    gold_top: str,
    gate_top: str,
    *,
    quiet: bool = False,
    out_dir: Optional[str] = None,
    no_name_matching: bool = False
) -> Popen[str]

run_equiv(
    gold_design: Union[Circuit, str, Path, List[str]],
    gate_design: Union[Circuit, str, Path, List[str]],
    gold_top: str = "",
    gate_top: str = "",
    *,
    quiet: bool = False,
    out_dir: Optional[str] = None,
    no_name_matching: bool = False
) -> Popen[str]

Runs a predefined script using the equiv_* passes from Yosys to prove the logical equivalence of the Verilog designs for the given Verilog designs.

The gold design is the golden reference design, while the gate design is the synthesized (gate-level) design. In the scope of this framework, the gate design refers to the modified or optimized version of the original design.

Parameters:

  • gold_design

    (Union[Circuit, str, Path, List[str]]) –

    The circuit object, or the file path(s) to the gold design.

  • gate_design

    (Union[Circuit, str, Path, List[str]]) –

    The circuit object, or the file path(s) to the gate design.

  • gold_top

    (str, default: '' ) –

    The top module name for the gold design.

  • gate_top

    (str, default: '' ) –

    The top module name for the gate design.

  • quiet

    (bool, default: False ) –

    If True, pipes all Yosys output into the subprocess.CompletedProcess object. If False, prints all Yosys output to the console. Defaults to False.

  • out_dir

    (Optional[str], default: None ) –

    The directory path, where the script (and other temporary files) will be stored. Defaults to None, in which case a temporary directory is created.

  • no_name_matching

    (bool, default: False ) –

    Whether to suppress the assumption that wires with the same name are identical. For example, gold.w1 may be structurally different from gate.w1, but logically equivalent. If no_name_matching is set to True, the equivalence check will still see the equivalence, but if it is False it will fail, since gold.w1 and gate.w1 do not follow the same structure. Defaults to False.

Returns:

  • Popen[str] –

    subprocess.CompletedProcess: The result of the execution plus some metadata.

run_equiv_miter 

run_equiv_miter(
    gold_design: Union[Circuit, str, Path, List[str]],
    gate_design: Union[Circuit, str, Path, List[str]],
    gold_top: str = "",
    gate_top: str = "",
    *,
    quiet: bool = False,
    out_dir: Optional[str] = None,
    cycles: Optional[PositiveInt] = None
) -> Popen[str]

Runs a predefined script to prove the logical equivalence for the given Verilog designs using a miter/SAT approach in Yosys.

The equivalence check is either executed for a given number of cycles for which the design must be equivalent (Bounded Model Check) or via temporal induction to prove that if the designs are equal after K cycles, they will be equal in cycle K+1.

The gold design is the golden reference design, while the gate design is the synthesized (gate-level) design. In the scope of this framework, the gate design refers to the modified or optimized version of the original design.

Parameters:

  • gold_design

    (Union[Circuit, str, Path, List[str]]) –

    The circuit object, or the file path(s) to the gold design.

  • gate_design

    (Union[Circuit, str, Path, List[str]]) –

    The circuit object, or the file path(s) to the gate design.

  • gold_top

    (str, default: '' ) –

    The top module name for the gold design.

  • gate_top

    (str, default: '' ) –

    The top module name for the gate design.

  • quiet

    (bool, default: False ) –

    If True, pipes all Yosys output into the subprocess.CompletedProcess object. If False, prints all Yosys output to the console. Defaults to False.

  • out_dir

    (Optional[str], default: None ) –

    The directory path, where the script (and other temporary files) will be stored. Defaults to None, in which case a temporary directory is created.

  • cycles

    (Optional[PositiveInt], default: None ) –

    The number of clock cycles for which the Bounded Model Checking should be executed. This approach checks if the designs behave equally for the given number of clock cycles. This however means, that if Yosys proves the equivalence for 5 cycles, it may diverge on the 6th cycle. However, larger numbers (e.g. more than 10 cycles) may lead to the algorithm running infinitely. If cycles is None (default case), an induction prove is executed that checks if they match at an arbitrary cycle K, they must match at cycle K+1 as well. This however may be hard for large circuits and run seemingly infinitely. Defaults to None, in which case a temporal induction is executed.

Returns:

  • Popen[str] –

    subprocess.CompletedProcess: The result of the execution plus some metadata.