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.

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,
) -> CompletedProcess[bytes]

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:

• CompletedProcess[bytes] –

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

run_eqy

run_eqy(
    gold_vfile_paths: List[str],
    gate_vfile_paths: List[str],
    gold_top_module: Optional[str] = None,
    gate_top_module: Optional[str] = None,
    script_path: Optional[str] = None,
    output_path: Optional[str] = None,
    overwrite: bool = False,
    quiet: bool = False,
) -> CompletedProcess[bytes]

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_vfile_paths

  (List[str]) –

  A list of paths to the gold Verilog files.

• gate_vfile_paths

  (List[str]) –

  A list of paths to the gate Verilog files.

• gold_top_module

  (Optional[str], default: None ) –

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

• gate_top_module

  (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:

• CompletedProcess[bytes] –

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

run_equiv

run_equiv(
    gold_vfile_path: str,
    gate_vfile_path: str,
    gold_top_module: str,
    gate_top_module: str,
    quiet: bool = False,
) -> CompletedProcess[bytes]

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 Verilog file is the golden reference design, while the gate Verilog file 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_vfile_path

  (str) –

  The file path to the gold Verilog file.

• gate_vfile_path

  (str) –

  The file path to the gate Verilog file.

• gold_top_module

  (str) –

  The top module name for the gold design.

• gate_top_module

  (str) –

  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.

Returns:

• CompletedProcess[bytes] –

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