test/orfs: retire eqy equivalence checking

bazel-orfs upstream dropped eqy_test/sby_test formal verification
support (eqy isn't actively maintained). Remove all consumers:
eqy-flow.bzl, the ram_8x7 test (whose only purpose was catching
eqy bugs), eqy_flow_test/eqy_test calls in mock-array and gcd,
and related README documentation.

Signed-off-by: Øyvind Harboe <oyvind.harboe@zylin.com>

Author: oharboe

test/orfs/README.md

@@ -109,127 +109,6 @@ To hunt down missing `tags = ["manual"]` run a query like:
 
 Note that OpenROAD *does* want `bazelisk test ...` to run all tests, so test targets should be marked `tags = ["orfs"]` instead, so that `.bazelrc` can skip builds of those targets with the `build --build_tag_filters=-orfs` line.
 
-## eqy tests
-
-`eqy_test` is used to run equivalence checks before and after an ORFS stage, such as before and after floorplan for mock-array. To run the test and keep all the files from the test and see interactive output, run:
-
-    bazelisk test //test/orfs/mock-array:MockArray_4x4_eqy_test --test_output=streamed --sandbox_debug
-
-If this fails, then it will output the line below. `eqy` uses a very, very large number of files and copying out these files to the bazel-testlogs folder for inspection takes some time:
-
-    Copying 114462 files to bazel-testlogs/test/orfs/mock-array/MockArray_4x4_eqy_test/test.outputs for inspection.
-
-If you just want the files needed to run a locally installed `eqy`, build all the files used in the run above by:
-
-    bazelisk build //test/orfs/mock-array:MockArray_4x4_eqy_test
-
-The files used to run the test are then in `bazel-bin/test/orfs/mock-array/`.
-
-### TL;DR creating archive for standalone eqy test
-
-Create `/tmp/issue.tar.gz`
-
-    bazelisk build //test/orfs/gcd:gcd_eqy_synth_test
-    tar --exclude='*oss_cad_suite*' -czvf /tmp/issue.tar.gz -C "$(bazelisk info bazel-bin)/test/orfs/gcd/gcd_eqy_synth_test.run.sh.runfiles" .
-
-Reproduction instructions:
-
-1. untar archive
-2. cd _main
-3. ~/oss-cad-suite/bin/eqy test/orfs/gcd/gcd_eqy_synth_test.eqy
-
-Comments:
-
-- `~/oss-cad-suite/` should be familiar with anyone versed in eqy as it refers to the [official binary release binaries](https://github.com/YosysHQ/oss-cad-suite-build)
-- Reproduction cases should be minimal in terms of size and context. The above recipe contains some unnecessary files, unnecessary directory structure, etc. Prune the test case further manually to get to the core of the matter.
-
-## Running eqy tests standalone outside bazel
-
-Build the test files:
-
-    bazelisk build //test/orfs/gcd:gcd_eqy_synth_test
-
-This outputs:
-
-    Target //test/orfs/gcd:gcd_eqy_synth_test up-to-date:
-      bazel-bin/test/orfs/gcd/gcd_eqy_synth_test.run.sh
-
-Copy all files needed to run the tests into a working folder `foo`:
-
-    rsync -aL "$(bazelisk info bazel-bin)/test/orfs/gcd/gcd_eqy_synth_test.run.sh.runfiles/" foo/
-
-Change cwd for running the tests:
-
-    cd foo/_main
-
-Bazel sets up both binaries and data files to run the tests, to create a reportable standalone test. A report should include only the data files and not the actual binaries used locally to run the test:
-
-    $ find .
-    .
-    ./test
-    ./test/orfs
-    ./test/orfs/asap7
-    ./test/orfs/asap7/asap7sc7p5t_SIMPLE_RVT_TT_201020.v
-    ./test/orfs/asap7/asap7sc7p5t_INVBUF_RVT_TT_201020.v
-    ./test/orfs/asap7/asap7sc7p5t_AO_RVT_TT_201020.v
-    ./test/orfs/asap7/asap7sc7p5t_OA_RVT_TT_201020.v
-    ./test/orfs/gcd
-    ./test/orfs/gcd/gcd.v
-    ./test/orfs/gcd/gcd_eqy_synth_test.run.sh
-    ./test/orfs/gcd/gcd_eqy_synth.v
-    ./test/orfs/gcd/gcd_eqy_synth_test.eqy
-
-Bazel generated `bazel-bin/test/orfs/gcd/gcd_eqy_synth_test.run.sh` to runs the tests. Examine this script to look at that for clues as to how to run the tests standalone:
-
-    $ head -n 5 test/orfs/gcd/gcd_eqy_synth_test.run.sh 
-    # !/bin/sh
-    set -euo pipefail
-    test_status=0
-    (exec ../bazel-orfs++_repo_rules+oss_cad_suite/bin/eqy "$@" test/orfs/gcd/gcd_eqy_synth_test.eqy) || test_status=$?
-
-What we want is:
-
-    ../bazel-orfs++_repo_rules+oss_cad_suite/bin/eqy test/orfs/gcd/gcd_eqy_synth_test.eqy
-
-Running this, we get:
-
-<pre>$ ../bazel-orfs++_repo_rules+oss_cad_suite/bin/eqy test/orfs/gcd/gcd_eqy_synth_test.eqy
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:24</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#A347BA">read_gold</font>: starting process &quot;yosys -ql gcd_eqy_synth_test/gold.log gcd_eqy_synth_test/gold.ys&quot;
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:24</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#A347BA">read_gold</font>: finished (returncode=0)
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:24</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#A347BA">read_gate</font>: starting process &quot;yosys -ql gcd_eqy_synth_test/gate.log gcd_eqy_synth_test/gate.ys&quot;
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:25</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#A347BA">read_gate</font>: finished (returncode=0)
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:25</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#A347BA">combine</font>: starting process &quot;yosys -ql gcd_eqy_synth_test/combine.log gcd_eqy_synth_test/combine.ys&quot;
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:25</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#A347BA">combine</font>: finished (returncode=0)
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:25</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#A2734C"><b>Warning: Cannot find entity _*_.*.</b></font>
-[deleted]
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:32</font> [<font color="#12488B">gcd_eqy_synth_test</font>] <font color="#C01C28"><b>Failed to prove equivalence of partition gcd.resp_msg.1</b></font>
-[deleted]
-<font color="#12488B">EQY</font> <font color="#26A269"> 8:05:32</font> [<font color="#12488B">gcd_eqy_synth_test</font>] DONE (FAIL, rc=2)
-</pre>
-
-
-## using sv-bugpoint to whittle down test-cases
-
-[sv-bugpoint](https://github.com/antmicro/sv-bugpoint) can be used to whittle down test-cases to a minimum example.
-
-Let's say that `bazelisk test test/orfs/gcd:eqy_synth_test` fails, first create a script that looks for the error string in the output, in this case a false positive `Failed to prove equivalence of partition gcd.req_rdy`.
-
-After compiling sv-bugpoint, we create a check.sh script:
-
-```bash
-#!/usr/bin/env bash
-set -euo pipefail
-cp $1 test/orfs/gcd/
-(bazelisk test test/orfs/gcd:eqy_synth_test --test_timeout=30 --test_output=streamed || error=$?) | tee /dev/tty | grep "Failed to prove equivalence of partition gcd.req_rdy"
-```
-
-- `--test_timeout=30` is a suitable timeout for this test and machine, adjust. Note that the timeout must be handled by Bazel and not a generic `timeout` utility as it would not work correctly with the bazel server.
-
-
-Next, run sv-bugpoint to whittle `test/orfs/gcd/gcd.v` down to a minimal test case:
-
-    ~/sv-bugpoint/build/sv-bugpoint fail check.sh test/orfs/gcd/gcd.v
-
 ## Using whittle.py to minimize .odb files
 
 While sv-bugpoint minimizes Verilog source files, `whittle.py` minimizes

test/orfs/eqy-flow.bzl

@@ -1,7 +1,6 @@
 load("@bazel-orfs//:sweep.bzl", "orfs_sweep")
 load("@rules_shell//shell:sh_test.bzl", "sh_test")
 load("//test/orfs:check_same.bzl", "check_same")
-load("//test/orfs:eqy-flow.bzl", "eqy_flow_test")
 
 package(features = ["layering_check"])
 
@@ -36,14 +35,6 @@ orfs_sweep(
     verilog_files = ["gcd.v"],
 )
 
-eqy_flow_test(
-    name = "gcd_eqy",
-    flow = "gcd",
-    module_top = "gcd",
-    tags = ["manual"],
-    verilog_files = ["gcd.v"],
-)
-
 filegroup(
     name = "gcd_floorplan_odb",
     srcs = [":gcd_floorplan"],

test/orfs/gcd/BUILD

@@ -11,31 +11,6 @@ This design has about 250 cells.
 
 Re-used code derived from http://opencelerity.org/ project.
 
-## LEC tests
-
-LEC tests exist for each of the ORFS stages as well as a self-test for the original source.
-
-In terms of expectations for LEC tests, this is experimental and contributions are highly appreciated. As of writing, even for such a small test case as gcd, the running time is considerable and eqy has false positives reported to the eqy project.
-
-```bash
-$ cd test/orfs/gcd
-$ bazelisk query :* | grep eqy | grep _test
-Loading: 0 packages loaded
-//test/orfs/gcd:gcd_eqy_cts_test
-//test/orfs/gcd:gcd_eqy_final_test
-//test/orfs/gcd:gcd_eqy_floorplan_test
-//test/orfs/gcd:gcd_eqy_grt_test
-//test/orfs/gcd:gcd_eqy_place_test
-//test/orfs/gcd:gcd_eqy_route_test
-//test/orfs/gcd:gcd_eqy_source_test
-//test/orfs/gcd:gcd_eqy_synth_test
-//test/orfs/gcd:gcd_eqy_tests
-```
-
-To run all the tests:
-
-    bazelisk test //test/orfs/gcd:gcd_eqy_tests --keep_going
-
 ## Whittle test
 
 The `gcd_whittle_test` is an integration test for `etc/whittle.py`, the

test/orfs/gcd/README.md

@@ -83,23 +83,6 @@ CONFIGS = {name: config(name, rows, cols) for name, rows, cols in [
     config = config,
 ) for name, config in CONFIGS.items()]
 
-test_suite(
-    name = "eqy_tests",
-    tags = ["manual"],
-    tests = ["Element_eqy_{variant}".format(variant = name) for name in CONFIGS] +
-            [
-                "MockArray_eqy_{name}_{variant}".format(
-                    name = name,
-                    variant = variant,
-                )
-                for name in CONFIGS
-                for variant in [
-                    "flat",
-                    "base",
-                ]
-            ],
-)
-
 orfs_run(
     name = "write_macro_placement",
     src = ":MockArray_4x4_base_floorplan",

test/orfs/mock-array/BUILD

@@ -63,9 +63,6 @@ power reporting. It has exposed:
   names (`475eb39584`).
 - Verilator reported 17k UNDRIVEN warnings on hierarchical output
   (issue #8108).
-- Equivalence checking (eqy) failures from `write_verilog` output and
-  FILLER/TAPCELL cell interactions (issues #8869, #8905, #9035; fix
-  PR #8966).
 
 ## What mock-array does NOT test
 
@@ -151,7 +148,4 @@ bazelisk build //test/orfs/mock-array:Element_4x4_slang_synth
 # Full: place-and-route (takes minutes)
 bazelisk test //test/orfs/mock-array:MockArray_4x4_base_test
 bazelisk test //test/orfs/mock-array:MockArray_4x4_flat_test
-
-# Power and equivalence (slowest)
-bazelisk test //test/orfs/mock-array:eqy_tests
 ```

test/orfs/mock-array/README.md

@@ -9,7 +9,6 @@ load("@rules_cc//cc:defs.bzl", "cc_binary")
 load("@rules_shell//shell:sh_test.bzl", "sh_test")
 load("@rules_verilator//verilator:defs.bzl", "verilator_cc_library")
 load("@rules_verilator//verilog:defs.bzl", "verilog_library")
-load("//test/orfs:eqy-flow.bzl", "eqy_flow_test")
 
 FIRTOOL_OPTIONS = [
     "-disable-all-randomization",
@@ -107,13 +106,6 @@ def element(name, config):
         verilog_files = [":{name}_verilog".format(name = name)],
         variant = "{name}_base".format(name = name),
     )
-    eqy_flow_test(
-        name = "Element_eqy_{variant}".format(variant = name),
-        flow = "Element_{variant}_base".format(variant = name),
-        verilog_files = [":{name}_verilog".format(name = name)],
-        tags = ["manual"],
-        module_top = "Element",
-    )
 
 POWER_STAGES = {
     "cts": {
@@ -302,14 +294,6 @@ def mock_array(name, config):
             variant = variant,
             verilog_files = [":{name}_verilog".format(name = name)],
         )
-        eqy_flow_test(
-            name = "MockArray_eqy_{variant}".format(variant = variant),
-            flow = "MockArray_{variant}".format(variant = variant),
-            verilog_files = [":{name}_verilog".format(name = name)],
-            other_verilog_files = [":Element_eqy_{name}_final_verilog".format(name = name)],
-            tags = ["manual"],
-            module_top = "MockArray",
-        )
 
         for stage in POWER_STAGES:
             for macro in MACROS: