hw/formal/lec_sv2v

#!/bin/bash

# Copyright lowRISC contributors.
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
# SPDX-License-Identifier: Apache-2.0

# This script runs LEC (logical equivalence checking) between 2 RTL
# files using Cadence Conformal LEC. Specifically, it checks if the
# Verilog file gnereated by the sv2v tool is logically equivalent to
# the original SystemVerilog.
#
# Usage: lec_sv2v <path-to-files> <module-name>
# Example: To run lec between prim_subreg.sv and generated prim_subreg.v,
# which are in directory ../../util/syn_out, type:
#   lec_sv2v ../../util/syn_out prim_subreg

export LEC_DIR=${1}
export LEC_TOP=${2}

# run Conformal LEC
lec -xl -nogui -nobanner \
  -dofile  lec_sv2v.do \
  -logfile lec_${LEC_TOP}.log \
  <<< "exit -force"