From 9f82ca23b273a5a500cc6a1ca60b30d3c33c5721 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 23 Sep 2024 15:45:05 -0700 Subject: [PATCH] End-to-end multiply smoketest (#84) Closes #81 Also includes an even wider multiply. --- .github/workflows/built-test-check-format.yml | 3 + .gitmodules | 3 + Cargo.lock | 118 +- Cargo.toml | 7 +- Dockerfile | 127 +- egglog_src/churchroad.egg | 25 + lakeroad | 1 + requirements.txt | 1 + run-tests.sh | 2 + src/global_greedy_dag.rs | 244 +++ src/lib.rs | 1262 ++++++++++++-- src/main.rs | 467 +++++ tests/egglog_tests.rs | 276 ++- tests/integration_tests/lit.cfg | 40 + tests/integration_tests/simple_mul.v | 28 + tests/integration_tests/wide_mul.v | 29 + tests/interpreter_tests.rs | 163 +- tests/type_inference_tests.rs | 4 +- yosys-plugin/churchroad.cc | 1549 ++--------------- yosys-plugin/tests/2bit-rca.sv | 33 +- yosys-plugin/tests/adder.sv | 17 +- yosys-plugin/tests/concat.sv | 17 +- yosys-plugin/tests/dsp48e2.sv | 262 +++ yosys-plugin/tests/example.ys | 17 +- yosys-plugin/tests/extract-bug.sv | 11 +- yosys-plugin/tests/module-instance.sv | 20 +- yosys-plugin/tests/permuter.sv | 39 +- yosys-plugin/tests/shiftx.sv | 2 +- yosys-plugin/tests/simple.sv | 15 +- 29 files changed, 2978 insertions(+), 1804 deletions(-) create mode 100644 .gitmodules create mode 160000 lakeroad create mode 100644 src/global_greedy_dag.rs create mode 100644 src/main.rs create mode 100644 tests/integration_tests/lit.cfg create mode 100644 tests/integration_tests/simple_mul.v create mode 100644 tests/integration_tests/wide_mul.v create mode 100644 yosys-plugin/tests/dsp48e2.sv diff --git a/.github/workflows/built-test-check-format.yml b/.github/workflows/built-test-check-format.yml index 1814df8..9783e90 100644 --- a/.github/workflows/built-test-check-format.yml +++ b/.github/workflows/built-test-check-format.yml @@ -49,6 +49,9 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v4 + with: + submodules: recursive + token: ${{ secrets.LAKEROAD_PRIVATE_PAT }} - name: Log in to the Container registry uses: docker/login-action@v3 diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..bc7d050 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "lakeroad"] + path = lakeroad + url = git@github.com:uwsampl/lakeroad diff --git a/Cargo.lock b/Cargo.lock index 61ef303..18e7f52 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -89,6 +89,15 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "archery" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eae2ed21cd55021f05707a807a5fc85695dafb98832921f6cfa06db67ca5b869" +dependencies = [ + "triomphe", +] + [[package]] name = "ascii-canvas" version = "3.0.0" @@ -125,6 +134,15 @@ version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" +[[package]] +name = "bitmaps" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2" +dependencies = [ + "typenum", +] + [[package]] name = "block-buffer" version = "0.10.4" @@ -144,18 +162,23 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" name = "churchroad" version = "0.1.0" dependencies = [ + "clap", "egglog", "egraph-serialize", + "env_logger 0.11.5", "indexmap", "log", + "ordered-float", "rand", + "rpds", + "tempfile", ] [[package]] name = "clap" -version = "4.5.7" +version = "4.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5db83dced34638ad474f39f250d7fea9598bdd239eaced1bdf45d597da0f433f" +checksum = "84b3edb18336f4df585bc9aa31dd99c036dfa5dc5e9a2939a722a188f3a8970d" dependencies = [ "clap_builder", "clap_derive", @@ -163,9 +186,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.7" +version = "4.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f7e204572485eb3fbf28f871612191521df159bc3e15a9f5064c66dba3a8c05f" +checksum = "c1c09dd5ada6c6c78075d6fd0da3f90d8080651e2d6cc8eb2f1aaa4034ced708" dependencies = [ "anstream", "anstyle", @@ -175,9 +198,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.5" +version = "4.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c780290ccf4fb26629baa7a1081e68ced113f1d3ec302fa5948f1c381ebf06c6" +checksum = "2bac35c6dafb060fd4d275d9a4ffae97917c13a6327903a8be2153cd964f7085" dependencies = [ "heck", "proc-macro2", @@ -270,14 +293,15 @@ checksum = "675e35c02a51bb4d4618cb4885b3839ce6d1787c97b664474d9208d074742e20" [[package]] name = "egglog" -version = "0.1.0" -source = "git+https://github.com/egraphs-good/egglog?rev=325814fd90767b5e43c72bc2eb65e14ff0b8746c#325814fd90767b5e43c72bc2eb65e14ff0b8746c" +version = "0.2.0" +source = "git+https://github.com/egraphs-good/egglog?rev=757c52f6dcf8fe5b7b5eefb4bdc872ef70a5433a#757c52f6dcf8fe5b7b5eefb4bdc872ef70a5433a" dependencies = [ "clap", "egraph-serialize", - "env_logger", + "env_logger 0.10.2", "generic_symbolic_expressions", "hashbrown 0.14.5", + "im-rc", "indexmap", "instant", "lalrpop", @@ -325,6 +349,16 @@ dependencies = [ "log", ] +[[package]] +name = "env_filter" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4f2c92ceda6ceec50f43169f9ee8424fe2db276791afde7b2cd8bc084cb376ab" +dependencies = [ + "log", + "regex", +] + [[package]] name = "env_logger" version = "0.10.2" @@ -338,6 +372,19 @@ dependencies = [ "termcolor", ] +[[package]] +name = "env_logger" +version = "0.11.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e13fa619b91fb2381732789fc5de83b45675e882f66623b7d8cb4f643017018d" +dependencies = [ + "anstream", + "anstyle", + "env_filter", + "humantime", + "log", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -378,8 +425,9 @@ dependencies = [ [[package]] name = "generic_symbolic_expressions" -version = "5.0.3" -source = "git+https://github.com/oflatt/symbolic-expressions?rev=655b6a4c06b4b3d3b2300e17779860b4abe440f0#655b6a4c06b4b3d3b2300e17779860b4abe440f0" +version = "5.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "597eb584fb7cfd1935294fc3608a453fc35a58dfa9da4299c8fd3bc75a4c0b4b" [[package]] name = "getrandom" @@ -445,6 +493,20 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" +[[package]] +name = "im-rc" +version = "15.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "af1955a75fa080c677d3972822ec4bad316169ab1cfc6c257a942c2265dbe5fe" +dependencies = [ + "bitmaps", + "rand_core", + "rand_xoshiro", + "sized-chunks", + "typenum", + "version_check", +] + [[package]] name = "indexmap" version = "2.2.6" @@ -817,6 +879,15 @@ dependencies = [ "serde", ] +[[package]] +name = "rand_xoshiro" +version = "0.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa" +dependencies = [ + "rand_core", +] + [[package]] name = "redox_syscall" version = "0.5.2" @@ -866,6 +937,15 @@ version = "0.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b" +[[package]] +name = "rpds" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0e15515d3ce3313324d842629ea4905c25a13f81953eadb88f85516f59290a4" +dependencies = [ + "archery", +] + [[package]] name = "rustc-hash" version = "1.1.0" @@ -961,6 +1041,16 @@ version = "0.3.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "38b58827f4464d87d377d175e90bf58eb00fd8716ff0a62f80356b5e61555d0d" +[[package]] +name = "sized-chunks" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e" +dependencies = [ + "bitmaps", + "typenum", +] + [[package]] name = "smallvec" version = "1.13.2" @@ -1079,6 +1169,12 @@ dependencies = [ "crunchy", ] +[[package]] +name = "triomphe" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6631e42e10b40c0690bf92f404ebcfe6e1fdb480391d15f17cc8e96eeed5369" + [[package]] name = "typenum" version = "1.17.0" diff --git a/Cargo.toml b/Cargo.toml index c523d14..7b67e01 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,8 +6,13 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -egglog = { git = "https://github.com/egraphs-good/egglog", rev = "325814fd90767b5e43c72bc2eb65e14ff0b8746c" } +egglog = { git = "https://github.com/egraphs-good/egglog", rev = "757c52f6dcf8fe5b7b5eefb4bdc872ef70a5433a" } log = "0.4.20" egraph-serialize = "0.1" rand = "0.8.4" indexmap = "2.0.0" +clap = "4.5.8" +tempfile = "3.10.1" +env_logger = "0.11.5" +rpds = "1.1.0" +ordered-float = "3" diff --git a/Dockerfile b/Dockerfile index bc45691..7808531 100644 --- a/Dockerfile +++ b/Dockerfile @@ -5,9 +5,11 @@ FROM ubuntu:22.04 ARG MAKE_JOBS=2 SHELL ["/bin/bash", "-c"] -# Update, get add-apt-repository. +# Update, get add-apt-repository, add PPA for Racket, update again. RUN apt update \ - && apt install -y software-properties-common + && apt install -y software-properties-common \ + && add-apt-repository ppa:plt/racket \ + && apt update # Install apt dependencies # `noninteractive` prevents the tzdata package from asking for a timezone on the @@ -51,17 +53,6 @@ RUN apt install -y \ RUN curl https://sh.rustup.rs -sSf | sh -s -- -y ENV PATH="/root/.cargo/bin:$PATH" -# Build Rust package. -WORKDIR /root/churchroad -# ADD has weird behavior when it comes to directories. That's why we need so -# many ADDs. -ADD egglog_src egglog_src -ADD src src -ADD tests tests -ADD Cargo.toml Cargo.toml -ADD Cargo.lock Cargo.lock -RUN cargo build - # Build Yosys. WORKDIR /root ARG MAKE_JOBS=2 @@ -76,11 +67,6 @@ RUN source /root/dependencies.sh \ # Add /root/.local/bin to PATH. ENV PATH="/root/.local/bin:$PATH" -# Build Yosys plugin. -WORKDIR /root/churchroad/yosys-plugin -ADD yosys-plugin . -RUN make -j ${MAKE_JOBS} - # Make a binary for `lit`. If you're on Mac, you can install lit via Brew. # Ubuntu doesn't have a binary for it, but it is available on pip and is # installed later in this Dockerfile. @@ -114,7 +100,109 @@ RUN apt install -y help2man && source /root/dependencies.sh \ && make install \ && cd .. \ && rm -rf verilator - + +# Build Yosys plugin. +WORKDIR /root/churchroad/yosys-plugin +ADD yosys-plugin . +RUN make -j ${MAKE_JOBS} + +# Add Lakeroad's dependencies.sh (later we add all of Lakeroad). +WORKDIR /root +ADD lakeroad/dependencies.sh lakeroad/dependencies.sh +ENV LAKEROAD_DIR=/root/lakeroad + +# Build Bitwuzla. +WORKDIR /root +RUN source $LAKEROAD_DIR/dependencies.sh \ + && mkdir bitwuzla \ + && wget -qO- https://github.com/bitwuzla/bitwuzla/archive/$BITWUZLA_COMMIT_HASH.tar.gz | tar xz -C bitwuzla --strip-components=1 \ + && cd bitwuzla \ + && ./configure.py --prefix=/root/.local \ + && cd build \ + && ninja -j${MAKE_JOBS} \ + && ninja install \ + && rm -rf /root/bitwuzla + +# Install raco (Racket) dependencies. +WORKDIR /root +RUN \ + # First, fix https://github.com/racket/racket/issues/2691 by building the + # docs. + raco setup --doc-index --force-user-docs \ + # Install packages. + && raco pkg install --deps search-auto --batch \ + rosette \ + yaml \ + # Install fmt directly from GitHub. This prevents the version from changing on + # us unexpectedly. + && cd /root \ + && git clone https://github.com/sorawee/fmt \ + && cd fmt \ + && source $LAKEROAD_DIR/dependencies.sh \ + && git checkout $RACKET_FMT_COMMIT_HASH \ + && raco pkg install --deps search-auto --batch + +# Build STP. +# TODO(@gussmith23): We shouldn't need this once https://github.com/stp/stp/issues/481 is fixed or https://github.com/stp/stp/pull/482 works correctly. +ENV LD_LIBRARY_PATH="/root/stp/deps/cadical/build:/root/stp/deps/cadiback/:$LD_LIBRARY_PATH" +WORKDIR /root +RUN apt-get install -y git cmake bison flex libboost-all-dev python2 perl && \ + source $LAKEROAD_DIR/dependencies.sh && \ + mkdir stp && cd stp && \ + wget -qO- https://github.com/$STP_USER_AND_REPO/archive/$STP_COMMIT_HASH.tar.gz | tar xz --strip-components=1 && \ + ./scripts/deps/setup-gtest.sh && \ + ./scripts/deps/setup-outputcheck.sh && \ + ./scripts/deps/setup-cms.sh && \ + ./scripts/deps/setup-minisat.sh && \ + mkdir build && \ + cd build && \ + cmake .. -DCMAKE_INSTALL_PREFIX=/root/.local && \ + make -j ${MAKE_JOBS} +# TODO(@gussmith23): Install and delete folder once +# https://github.com/stp/stp/issues/479 is fixed. +# make install && \ +# rm -rf /root/stp +# And after that we also don't need to add STP to the path. +ENV PATH="/root/stp/build:${PATH}" + +# Build CVC5. +RUN source $LAKEROAD_DIR/dependencies.sh \ + && mkdir cvc5 && cd cvc5 \ + && wget -qO- https://github.com/cvc5/cvc5/archive/$CVC5_COMMIT_HASH.tar.gz | tar xz --strip-components=1 \ + && ./configure.sh --prefix="/root/.local" --auto-download \ + && cd ./build \ + && make -j ${MAKE_JOBS} \ + && make -j ${MAKE_JOBS} install \ + && rm -rf /root/cvc5 + +# Build Yices2. +RUN source $LAKEROAD_DIR/dependencies.sh \ + && apt-get install -y gperf \ + && mkdir yices2 && cd yices2 \ + && wget -qO- https://github.com/SRI-CSL/yices2/archive/$YICES2_COMMIT_HASH.tar.gz | tar xz --strip-components=1 \ + && autoconf \ + && ./configure --prefix="/root/.local" \ + && make -j ${MAKE_JOBS} \ + && make -j ${MAKE_JOBS} install \ + && rm -rf /root/yices2 + +# Add Lakeroad and build Racket bytecode; makes Lakeroad much faster. +WORKDIR /root +ADD lakeroad lakeroad +ENV LAKEROAD_DIR=/root/lakeroad +RUN raco make $LAKEROAD_DIR/bin/main.rkt + +# Build Rust package. This should be as far down as it can be, as it'll change +# frequently. +WORKDIR /root/churchroad +# ADD has weird behavior when it comes to directories. That's why we need so +# many ADDs. +ADD egglog_src egglog_src +ADD src src +ADD tests tests +ADD Cargo.toml Cargo.toml +ADD Cargo.lock Cargo.lock +RUN cargo build # Add other Churchroad files. It's useful to put this as far down as possible. # In general, only ADD files just before they're needed. This maximizes the @@ -127,6 +215,7 @@ RUN apt install -y help2man && source /root/dependencies.sh \ WORKDIR /root/churchroad ADD --keep-git-dir=false . . + WORKDIR /root/churchroad ADD fmt.sh run-tests.sh ./ CMD [ "/bin/bash", "run-tests.sh" ] diff --git a/egglog_src/churchroad.egg b/egglog_src/churchroad.egg index 9ffc911..183fb07 100644 --- a/egglog_src/churchroad.egg +++ b/egglog_src/churchroad.egg @@ -17,6 +17,7 @@ (Or) (Xor) (Shr) + (Shl) ; Returns a bitvector of width 1. (Eq) (Ne) @@ -46,8 +47,12 @@ ; (Op0 (BV value bitwidth)) (BV i64 i64) + ; (Op0 (CRString val)) + (CRString String) + ; (Op1 (ZeroExtend bitwidth) expr) (ZeroExtend i64) + ; (Op1 (SignExtend bitwidth) expr) (SignExtend i64) ) @@ -154,6 +159,8 @@ (AllBitwidthsMatch (Or)) (AllBitwidthsMatch (Xor)) (AllBitwidthsMatch (Shr)) +(AllBitwidthsMatch (Shl)) +(AllBitwidthsMatch (Mul)) ;;; TODO(@ninehusky): don't we need this here? (AllBitwidthsMatch (Not)) ; Have to write this one as a rule, unfortunately. @@ -174,6 +181,19 @@ (Bitwise (Xor)) ;;; (Bitwise (Not)) TODO(@ninehusky): don't we need this here? +;;; Misc +(ruleset misc) +;;; Rule to union concatted wires with +(rule + ((= expr (Op2 (Concat) (Wire name bw) e)) + (HasType e (Bitvector n))) + ((union (Wire name bw) (Op1 (Extract (- (+ bw n) 1) n) expr))) + :ruleset misc) +(rule + ((= expr (Op2 (Concat) e (Wire name bw)))) + ((union (Wire name bw) (Op1 (Extract (- bw 1) 0) expr))) + :ruleset misc) + ;;; Typing judgements. (ruleset typing) @@ -300,3 +320,8 @@ (Op1 (Extract (- n 1) 1) e1) (Op1 (Extract (- n 1) 1) e2)) (Op2 op (Op1 (Extract 0 0) e1) (Op1 (Extract 0 0) e2)))))) + +; TODO(@gussmith23): Figure out a better interface for these, currently just +; adding them as needed. +(function PrimitiveInterfaceDSP (Expr Expr) Expr) +(function PrimitiveInterfaceDSP3 (Expr Expr Expr) Expr) \ No newline at end of file diff --git a/lakeroad b/lakeroad new file mode 160000 index 0000000..7a69047 --- /dev/null +++ b/lakeroad @@ -0,0 +1 @@ +Subproject commit 7a69047ad20cad54e5c78d68d397b716b42ff462 diff --git a/requirements.txt b/requirements.txt index acc40b6..03b4684 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,3 @@ black==24.2.0 lit==15.0.0 +meson==1.2.0 diff --git a/run-tests.sh b/run-tests.sh index d47c3e4..62873b8 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -5,3 +5,5 @@ set -e cargo test ./yosys-plugin/run_tests.sh + +lit -v tests/integration_tests diff --git a/src/global_greedy_dag.rs b/src/global_greedy_dag.rs new file mode 100644 index 0000000..5d8e02d --- /dev/null +++ b/src/global_greedy_dag.rs @@ -0,0 +1,244 @@ +/// from https://github.com/egraphs-good/extraction-gym/blob/main/src/extract/global_greedy_dag.rs +use std::iter; + +use egraph_serialize::Cost; +use ordered_float::NotNan; +use rpds::HashTrieSet; + +use super::*; + +type TermId = usize; + +pub const INFINITY: Cost = unsafe { NotNan::new_unchecked(f64::INFINITY) }; + +#[derive(Clone, PartialEq, Eq, Hash)] +struct Term { + op: String, + children: Vec, +} + +type Reachable = HashTrieSet; + +struct TermInfo { + node: NodeId, + eclass: ClassId, + node_cost: Cost, + total_cost: Cost, + // store the set of reachable terms from this term + reachable: Reachable, + size: usize, +} + +/// A TermDag needs to store terms that share common +/// subterms using a hashmap. +/// However, it also critically needs to be able to answer +/// reachability queries in this dag `reachable`. +/// This prevents double-counting costs when +/// computing the cost of a term. +#[derive(Default)] +pub struct TermDag { + nodes: Vec, + info: Vec, + hash_cons: HashMap, +} + +impl TermDag { + /// Makes a new term using a node and children terms + /// Correctly computes total_cost with sharing + /// If this term contains itself, returns None + /// If this term costs more than target, returns None + pub fn make( + &mut self, + node_id: NodeId, + node: &Node, + children: Vec, + target: Cost, + ) -> Option { + let term = Term { + op: node.op.clone(), + children: children.clone(), + }; + + if let Some(id) = self.hash_cons.get(&term) { + return Some(*id); + } + + let node_cost = node.cost; + + if children.is_empty() { + let next_id = self.nodes.len(); + self.nodes.push(term.clone()); + self.info.push(TermInfo { + node: node_id, + eclass: node.eclass.clone(), + node_cost, + total_cost: node_cost, + reachable: iter::once(node.eclass.clone()).collect(), + size: 1, + }); + self.hash_cons.insert(term, next_id); + Some(next_id) + } else { + // check if children contains this node, preventing cycles + // This is sound because `reachable` is the set of reachable eclasses + // from this term. + for child in &children { + if self.info[*child].reachable.contains(&node.eclass) { + return None; + } + } + + let biggest_child = (0..children.len()) + .max_by_key(|i| self.info[children[*i]].size) + .unwrap(); + + let mut cost = node_cost + self.total_cost(children[biggest_child]); + let mut reachable = self.info[children[biggest_child]].reachable.clone(); + let next_id = self.nodes.len(); + + for child in children.iter() { + if cost > target { + return None; + } + let child_cost = self.get_cost(&mut reachable, *child); + cost += child_cost; + } + + if cost > target { + return None; + } + + reachable = reachable.insert(node.eclass.clone()); + + self.info.push(TermInfo { + node: node_id, + node_cost, + eclass: node.eclass.clone(), + total_cost: cost, + reachable, + size: 1 + children.iter().map(|c| self.info[*c].size).sum::(), + }); + self.nodes.push(term.clone()); + self.hash_cons.insert(term, next_id); + Some(next_id) + } + } + + /// Return a new term, like this one but making use of shared terms. + /// Also return the cost of the new nodes. + fn get_cost(&self, shared: &mut Reachable, id: TermId) -> Cost { + let eclass = self.info[id].eclass.clone(); + + // This is the key to why this algorithm is faster than greedy_dag. + // While doing the set union between reachable sets, we can stop early + // if we find a shared term. + // Since the term with `id` is shared, the reachable set of `id` will already + // be in `shared`. + if shared.contains(&eclass) { + NotNan::::new(0.0).unwrap() + } else { + let mut cost = self.node_cost(id); + for child in &self.nodes[id].children { + let child_cost = self.get_cost(shared, *child); + cost += child_cost; + } + *shared = shared.insert(eclass); + cost + } + } + + pub fn node_cost(&self, id: TermId) -> Cost { + self.info[id].node_cost + } + + pub fn total_cost(&self, id: TermId) -> Cost { + self.info[id].total_cost + } +} + +pub struct GlobalGreedyDagExtractor { + pub structural_only: bool, +} +impl GlobalGreedyDagExtractor { + pub fn extract( + &self, + egraph: &egraph_serialize::EGraph, + _roots: &[ClassId], + ) -> IndexMap { + let mut keep_going = true; + + let nodes = egraph.nodes.clone(); + let mut termdag = TermDag::default(); + let mut best_in_class: HashMap = HashMap::default(); + + while keep_going { + keep_going = false; + + 'node_loop: for (node_id, node) in &nodes { + // NOTE: This is the only modification we made to make this work + // with churchroad. Could find a different way to do this. + // + // Always exclude certain nodes that are always unwanted. + if node.op == "Wire" + || node.op == "PrimitiveInterfaceDSP" + || node.op == "PrimitiveInterfaceDSP3" + { + continue 'node_loop; + } + // Sometimes exclude nodes that are only structural, if the user wants. + if self.structural_only + && match node.op.as_str() { + "Op0" | "Op1" | "Op2" | "Op3" => { + let op_name = &egraph[node_id].children[0]; + !matches!( + egraph[op_name].op.as_str(), + "Extract" + | "Concat" + | "BV" + | "CRString" + | "ZeroExtend" + | "SignExtend" + | "Shr" + | "Shl" + ) + } + _ => false, + } + { + continue 'node_loop; + } + + let mut children: Vec = vec![]; + // compute the cost set from the children + for child in &node.children { + let child_cid = egraph.nid_to_cid(child); + if let Some(best) = best_in_class.get(child_cid) { + children.push(*best); + } else { + continue 'node_loop; + } + } + + let old_cost = best_in_class + .get(&node.eclass) + .map(|id| termdag.total_cost(*id)) + .unwrap_or(INFINITY); + + if let Some(candidate) = termdag.make(node_id.clone(), node, children, old_cost) { + let cadidate_cost = termdag.total_cost(candidate); + + if cadidate_cost < old_cost { + best_in_class.insert(node.eclass.clone(), candidate); + keep_going = true; + } + } + } + } + + let mut result = IndexMap::default(); + for (class, term) in best_in_class { + result.insert(class, termdag.info[term].node.clone()); + } + result + } +} diff --git a/src/lib.rs b/src/lib.rs index 5d8daf7..1277118 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,17 +1,863 @@ +pub mod global_greedy_dag; + use egraph_serialize::{ClassId, Node, NodeId}; use indexmap::IndexMap; +use log::{info, warn}; use std::{ collections::{HashMap, HashSet}, + env, + fmt::Debug, + fs::read_to_string, + io::Write, + path::Path, + process::{Command, Stdio}, sync::Arc, + time::SystemTime, }; +use tempfile::NamedTempFile; use egglog::{ - ast::{Literal, Symbol}, + ast::{Literal, Span, SrcFile, Symbol}, constraint::{SimpleTypeConstraint, TypeConstraint}, sort::{FromSort, I64Sort, IntoSort, Sort, VecSort}, ArcSort, EGraph, PrimitiveLike, Term, TermDag, Value, }; +pub fn call_lakeroad_on_primitive_interface_and_spec( + serialized_egraph: &egraph_serialize::EGraph, + spec_choices: &indexmap::IndexMap, + _spec_node_id: &NodeId, + sketch_template_node_id: &NodeId, + architecture: &str, +) -> String { + let eclass = &serialized_egraph[sketch_template_node_id].eclass; + // Assert the two nodes are the same class. + assert_eq!(eclass, &serialized_egraph[_spec_node_id].eclass); + + // Not supporting anything other than a simple DSP sketch at the moment. + assert!( + serialized_egraph[sketch_template_node_id].op == "PrimitiveInterfaceDSP" + || serialized_egraph[sketch_template_node_id].op == "PrimitiveInterfaceDSP3" + ); + + let out_bw = get_bitwidth_for_node(serialized_egraph, sketch_template_node_id).unwrap(); + + log::debug!( + "a expr: {}", + node_to_string( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[0], + spec_choices + ) + ); + log::debug!( + "b expr: {}", + node_to_string( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[1], + spec_choices + ) + ); + + if serialized_egraph[sketch_template_node_id].op == "PrimitiveInterfaceDSP3" { + log::debug!( + "c expr: {}", + node_to_string( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[2], + spec_choices + ) + ); + } + + let a_bw = get_bitwidth_for_node( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[0], + ) + .unwrap(); + let b_bw = get_bitwidth_for_node( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[1], + ) + .unwrap(); + + let mut bottom_out_at = HashMap::new(); + bottom_out_at.insert( + serialized_egraph[&serialized_egraph[sketch_template_node_id].children[0]] + .eclass + .clone(), + "a".to_string(), + ); + bottom_out_at.insert( + serialized_egraph[&serialized_egraph[sketch_template_node_id].children[1]] + .eclass + .clone(), + "b".to_string(), + ); + if serialized_egraph[sketch_template_node_id].op == "PrimitiveInterfaceDSP3" { + bottom_out_at.insert( + serialized_egraph[&serialized_egraph[sketch_template_node_id].children[2]] + .eclass + .clone(), + "c".to_string(), + ); + } + + // Put the spec in a tempfile. + let mut spec_file = NamedTempFile::new().unwrap(); + let spec_filepath = spec_file.path().to_owned(); + spec_file + .write_all( + to_verilog_egraph_serialize( + serialized_egraph, + spec_choices, + "clk", + bottom_out_at, + Some([(eclass.clone(), "out".to_string())].into()), + ) + .as_bytes(), + ) + .unwrap(); + spec_file.flush().unwrap(); + // spec_file.persist("tmp.v").unwrap(); + + let binding = + env::var("LAKEROAD_DIR").expect("LAKEROAD_DIR environment variable should be set."); + let lakeroad_dir = Path::new(&binding); + let mut command = Command::new("racket"); + command + .arg(lakeroad_dir.join("bin").join("main.rkt")) + .arg("--architecture") + .arg(architecture) + .arg("--verilog-module-filepath") + .arg(spec_filepath) + // TODO(@gussmith23): This should probably not be implicit in the generate-verilog function. + .arg("--top-module-name") + .arg("top") + // TODO(@gussmith23): Determine this automatically somehow. + .arg("--verilog-module-out-signal") + .arg(format!("out:{out_bw}")) + .arg("--input-signal") + .arg(format!("a:(port a {a_bw}):{a_bw}")) + .arg("--input-signal") + .arg(format!("b:(port b {b_bw}):{b_bw}")) + .arg("--template") + .arg("dsp") + .arg("--pipeline-depth") + .arg("0") + .arg("--out-format") + .arg("verilog") + .arg("--timeout") + .arg("120"); + if serialized_egraph[sketch_template_node_id].op == "PrimitiveInterfaceDSP3" { + let c_bw = get_bitwidth_for_node( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[2], + ) + .unwrap(); + command + .arg("--input-signal") + .arg(format!("c:(port c {c_bw}):{c_bw}")); + } + log::debug!( + "Lakeroad command: {}", + &command + .get_args() + .map(|s| s.to_str().unwrap().to_owned()) + .collect::>() + .join(" ") + ); + let output = command.output().unwrap(); + + if !output.status.success() { + panic!( + "Lakeroad failed with code {}. stdout:\n{}\n\nstderr:\n{}", + output.status.code().unwrap(), + String::from_utf8_lossy(&output.stderr), + String::from_utf8_lossy(&output.stdout) + ); + } + + let mut verilog = String::from_utf8_lossy(&output.stdout).into_owned(); + + info!( + "First few lines of generated Verilog:\n{}", + verilog.lines().take(10).collect::>().join("\n") + ); + + // TODO(@gussmith23): hardcoding the definition of DSP48E2 here. Should + // instead take it as input to the flow at some point. + verilog.push_str( + r#" +// DSP48E2 definition from Xilinx. Note that we keep the module empty for now -- +// we only need the input/output port definitions. + +/////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 1995/2018 Xilinx, Inc. +// All Right Reserved. +/////////////////////////////////////////////////////////////////////////////// +// ____ ____ +// / /\/ / +// /___/ \ / Vendor : Xilinx +// \ \ \/ Version : 2018.3 +// \ \ Description : Xilinx Unified Simulation Library Component +// / / 48-bit Multi-Functional Arithmetic Block +// /___/ /\ Filename : DSP48E2.v +// \ \ / \ +// \___\/\___\ +// +/////////////////////////////////////////////////////////////////////////////// +// Revision: +// 07/15/12 - Migrate from E1. +// 12/10/12 - Add dynamic registers +// 01/10/13 - 694456 - DIN_in/D_in connectivity issue +// 01/11/13 - DIN, D_DATA data width change (26/24) sync4 yml +// 02/13/13 - PCIN_47A change from internal feedback to PCIN(47) pin +// 03/06/13 - 701316 - A_B_reg no clk when REG=0 +// 04/03/13 - yaml update +// 04/08/13 - 710304 - AREG, BREG, ACASCREG and BCASCREG dynamic registers mis sized. +// 04/22/13 - 714213 - ACOUT, BCOUT wrong logic +// 04/22/13 - 713695 - Zero mult result on USE_SIMD +// 04/22/13 - 713617 - CARRYCASCOUT behaviour +// 04/23/13 - 714772 - remove sensitivity to negedge GSR +// 04/23/13 - 713706 - change P_PDBK connection +// 05/07/13 - 716896 - AREG, BREG, ACASCREG and BCASCREG localparams mis sized. +// 05/07/13 - 716896 - ALUMODE/OPMODE_INV_REG mis sized +// 05/07/13 - 716896 - INMODE_INV_REG mis sized +// 05/07/13 - x_mac_cascd missing for sensitivity list. +// 10/22/14 - 808642 - Added #1 to $finish +// End Revision: +/////////////////////////////////////////////////////////////////////////////// + +module DSP48E2 #( + parameter integer ACASCREG = 1, + parameter integer ADREG = 1, + parameter integer ALUMODEREG = 1, + parameter AMULTSEL = "A", + parameter integer AREG = 1, + parameter AUTORESET_PATDET = "NO_RESET", + parameter AUTORESET_PRIORITY = "RESET", + parameter A_INPUT = "DIRECT", + parameter integer BCASCREG = 1, + parameter BMULTSEL = "B", + parameter integer BREG = 1, + parameter B_INPUT = "DIRECT", + parameter integer CARRYINREG = 1, + parameter integer CARRYINSELREG = 1, + parameter integer CREG = 1, + parameter integer DREG = 1, + parameter integer INMODEREG = 1, + parameter [3:0] IS_ALUMODE_INVERTED = 4'b0000, + parameter [0:0] IS_CARRYIN_INVERTED = 1'b0, + parameter [0:0] IS_CLK_INVERTED = 1'b0, + parameter [4:0] IS_INMODE_INVERTED = 5'b00000, + parameter [8:0] IS_OPMODE_INVERTED = 9'b000000000, + parameter [0:0] IS_RSTALLCARRYIN_INVERTED = 1'b0, + parameter [0:0] IS_RSTALUMODE_INVERTED = 1'b0, + parameter [0:0] IS_RSTA_INVERTED = 1'b0, + parameter [0:0] IS_RSTB_INVERTED = 1'b0, + parameter [0:0] IS_RSTCTRL_INVERTED = 1'b0, + parameter [0:0] IS_RSTC_INVERTED = 1'b0, + parameter [0:0] IS_RSTD_INVERTED = 1'b0, + parameter [0:0] IS_RSTINMODE_INVERTED = 1'b0, + parameter [0:0] IS_RSTM_INVERTED = 1'b0, + parameter [0:0] IS_RSTP_INVERTED = 1'b0, + parameter [47:0] MASK = 48'h3FFFFFFFFFFF, + parameter integer MREG = 1, + parameter integer OPMODEREG = 1, + parameter [47:0] PATTERN = 48'h000000000000, + parameter PREADDINSEL = "A", + parameter integer PREG = 1, + parameter [47:0] RND = 48'h000000000000, + parameter SEL_MASK = "MASK", + parameter SEL_PATTERN = "PATTERN", + parameter USE_MULT = "MULTIPLY", + parameter USE_PATTERN_DETECT = "NO_PATDET", + parameter USE_SIMD = "ONE48", + parameter USE_WIDEXOR = "FALSE", + parameter XORSIMD = "XOR24_48_96" +) ( + output [29:0] ACOUT, + output [17:0] BCOUT, + output CARRYCASCOUT, + output [3:0] CARRYOUT, + output MULTSIGNOUT, + output OVERFLOW, + output [47:0] P, + output PATTERNBDETECT, + output PATTERNDETECT, + output [47:0] PCOUT, + output UNDERFLOW, + output [7:0] XOROUT, + + input [29:0] A, + input [29:0] ACIN, + input [3:0] ALUMODE, + input [17:0] B, + input [17:0] BCIN, + input [47:0] C, + input CARRYCASCIN, + input CARRYIN, + input [2:0] CARRYINSEL, + input CEA1, + input CEA2, + input CEAD, + input CEALUMODE, + input CEB1, + input CEB2, + input CEC, + input CECARRYIN, + input CECTRL, + input CED, + input CEINMODE, + input CEM, + input CEP, + input CLK, + input [26:0] D, + input [4:0] INMODE, + input MULTSIGNIN, + input [8:0] OPMODE, + input [47:0] PCIN, + input RSTA, + input RSTALLCARRYIN, + input RSTALUMODE, + input RSTB, + input RSTC, + input RSTCTRL, + input RSTD, + input RSTINMODE, + input RSTM, + input RSTP +); + +endmodule +"#, + ); + + let choices = AnythingExtractor.extract(serialized_egraph, &[]); + + // Generate port bindings. + let mut port_to_expr_map = HashMap::new(); + port_to_expr_map.insert( + "a".to_string(), + node_to_string( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[0], + &choices, + ), + ); + port_to_expr_map.insert( + "b".to_string(), + node_to_string( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[1], + &choices, + ), + ); + if serialized_egraph[sketch_template_node_id].op == "PrimitiveInterfaceDSP3" { + port_to_expr_map.insert( + "c".to_string(), + node_to_string( + serialized_egraph, + &serialized_egraph[sketch_template_node_id].children[2], + &choices, + ), + ); + } + port_to_expr_map.insert( + "out".to_string(), + node_to_string(serialized_egraph, sketch_template_node_id, &choices), + ); + + // TODO(@gussmith23): hardcoded module name + // Don't simcheck, because there'll be undefined modules. That's expected. + // Don't generate let bindings. + + commands_from_verilog(&verilog, "top", false, false, port_to_expr_map) +} + +/// Converts serialized egraph with map of choices and root node to an S-expr. +/// TODO(@gussmith23): this will probably run infinitely when there are cycles. +pub fn node_to_string( + egraph: &egraph_serialize::EGraph, + node_id: &NodeId, + choices: &indexmap::IndexMap, +) -> String { + let node = &egraph.nodes[node_id]; + let mut out = String::new(); + // Don't wrap in parens when op begins with a quote or a number. + // TODO(@gussmith23): this is very rough. + let wrap_in_parens = node.op.chars().next().unwrap().is_ascii_alphabetic(); + + if wrap_in_parens { + out += "("; + } + out += node.op.as_str(); + for child_id in &node.children { + out += " "; + out += &node_to_string(egraph, &choices[&egraph[child_id].eclass], choices); + } + + if wrap_in_parens { + out += ")"; + } + + out +} + +// TODO(@gussmith23): It would be nice to not have to use a mutable reference +// here. +pub fn find_primitive_interface_values(egraph: &mut EGraph) -> Vec<(ArcSort, Value)> { + const NUM_TO_GET: usize = 100; + let (results, termdag) = egraph + .function_to_dag("PrimitiveInterfaceDSP".into(), NUM_TO_GET) + .unwrap(); + assert!(results.len() < NUM_TO_GET); + + for (term, output) in &results { + // I don't know if this is actually always the case, but I don't know + // what it means when it's not the case. + assert_eq!(term, output); + } + + let sorts_and_exprs: Vec<_> = results + .iter() + .map(|(term, output)| { + // I don't know if this is actually always the case, but I don't know + // what it means when it's not the case. + assert_eq!(term, output); + + egraph.eval_expr(&termdag.term_to_expr(term)).unwrap() + }) + .collect(); + + sorts_and_exprs +} + +/// Same as [`find_primitive_interface_values`] but over a serialized egraph. +pub fn find_primitive_interfaces_serialized(egraph: &egraph_serialize::EGraph) -> Vec { + egraph + .nodes + .iter() + .filter_map(|(node_id, node)| { + if node.op == "PrimitiveInterfaceDSP" || node.op == "PrimitiveInterfaceDSP3" { + Some(node_id.to_owned()) + } else { + None + } + }) + .collect() +} + +/// Extracts only expressions legal in structural Verilog. +#[derive(Default)] +pub struct StructuralVerilogExtractor; +impl StructuralVerilogExtractor { + pub fn extract( + &self, + egraph: &egraph_serialize::EGraph, + _roots: &[egraph_serialize::ClassId], + ) -> IndexMap { + egraph + .classes() + .iter() + .map(|(id, class)| { + let mut potential_nodes = class + .nodes + .iter() + .filter(|node_id| { + let op = &egraph[*node_id].op; + // Filter certain op types. + !(["PrimitiveInterfaceDSP"].contains(&op.as_str())) + }) + .filter(|node_id| { + let op = egraph[*node_id].op.as_str(); + match op { + "Op0" | "Op1" | "Op2" | "Op3" => { + let op_name = &egraph[*node_id].children[0]; + matches!( + egraph[op_name].op.as_str(), + "Extract" + | "Concat" + | "BV" + | "CRString" + | "ZeroExtend" + | "SignExtend" + ) + } + _ => true, + } + }) + .collect::>(); + potential_nodes.sort_by(|a, b| { + // If either is a wire, it should come last. + let are_wires = (egraph[*a].op == "Wire", egraph[*b].op == "Wire"); + match are_wires { + (true, true) => std::cmp::Ordering::Equal, + (true, false) => std::cmp::Ordering::Greater, + (false, true) => std::cmp::Ordering::Less, + (false, false) => { + // Otherwise, sort by the node ID. + a.cmp(b) + } + } + }); + assert!(!potential_nodes.is_empty(), "Found unextractable class."); + let node_id = potential_nodes[0].clone(); + // Warn if we're still extracting a Wire. + if egraph[&node_id].op == "Wire" { + log::warn!( + "Extracting wire {}. All nodes in this eclass:\n{}", + egraph[&egraph[&node_id].children[0]].op, + class + .nodes + .iter() + .map(|node_id| egraph[node_id].op.clone()) + .collect::>() + .join("\n") + ); + } + (id.clone(), node_id) + }) + .collect() + } +} + +/// Extract specs, ensuring specific nodes are chosen. +#[derive(Default)] +pub struct EnsureExtractSpecExtractor { + pub ensure_extract: HashSet, +} +impl EnsureExtractSpecExtractor { + pub fn extract( + &self, + egraph: &egraph_serialize::EGraph, + _roots: &[egraph_serialize::ClassId], + ) -> IndexMap { + let _work_to_be_done = true; + + // Maps node ID to the number of desired-to-be-extracted nodes that can + // be extracted via this node. + let mut ensure_extract_tracker: HashMap<_, _> = egraph + .nodes + .iter() + .map(|(node_id, _)| { + if self.ensure_extract.contains(node_id) { + (node_id.clone(), 1) + } else { + (node_id.clone(), 0) + } + }) + .collect(); + + let mut choices: IndexMap<_, _> = egraph + .classes() + .iter() + .map(|(id, class)| { + let node_id = class + .nodes + .iter() + .find(|node_id| { + let op = &egraph[*node_id].op; + + // Filter certain op types. + !(["PrimitiveInterfaceDSP", "PrimitiveInterfaceDSP3", "Wire"] + .contains(&op.as_str())) + }) + .unwrap() + .clone(); + (id.clone(), node_id) + }) + .collect(); + + // For every eclass, choose the node with the highest number of + // desired-to-be-extracted nodes under it. + fn update_choices( + egraph: &egraph_serialize::EGraph, + ensure_extract_tracker: &HashMap, + choices: &mut IndexMap, + ) { + for (id, class) in egraph.classes() { + let mut sorted_nodes: Vec<_> = class + .nodes + .iter() + .filter(|&node_id| { + let op = &egraph[node_id].op; + // Filter out banned nodes. + !(["PrimitiveInterfaceDSP", "PrimitiveInterfaceDSP3", "Wire"] + .contains(&op.as_str())) + }) + .cloned() + .collect(); + sorted_nodes.sort_by_key(|node_id| ensure_extract_tracker[node_id]); + sorted_nodes.reverse(); + let new_choice = sorted_nodes[0].clone(); + let old_choice = choices + .insert(id.clone(), new_choice.clone()) + .expect("Class should have already been in choices."); + if new_choice != old_choice { + log::debug!( + "Changed choice for class {} from {} to {}", + id, + egraph[&old_choice].op, + egraph[&new_choice].op + ); + } + } + } + + // Returns whether any updates were made. + fn update_node_tracker( + egraph: &egraph_serialize::EGraph, + ensure_extract_tracker: &mut HashMap, + choices: &IndexMap, + ) -> bool { + let mut update_occurred = false; + for (node_id, node) in egraph.nodes.iter() { + // Leaves already have their final value and don't need to be + // updated. + if node.children.is_empty() { + continue; + } + + let new_value = node + .children + .iter() + .map(|child_id| { + // We have to make sure to use choices to get the + // *actual* node ID. Indexing an egraph at a nodeid + // gives you another node, but we need to consider + // that that node might not actually be the current + // choice for the eclass. + let node_choice = &choices[&egraph[child_id].eclass]; + ensure_extract_tracker[node_choice] + }) + .sum(); + let old_value = ensure_extract_tracker.insert(node_id.clone(), new_value); + assert!( + old_value.is_some(), + "Node should have already been in ensure_extract_tracker." + ); + + if old_value.unwrap() != new_value { + update_occurred = true; + } + } + + update_occurred + } + + // Set to true so we do at least one iteration. + let mut updates_occurred = true; + // Keep updating until no more updates are made. + while updates_occurred { + update_choices(egraph, &ensure_extract_tracker, &mut choices); + updates_occurred = update_node_tracker(egraph, &mut ensure_extract_tracker, &choices); + } + + choices + } +} +/// I don't know if we should be making Extractors in such an ad-hoc way, but +/// this actually seems to be the most convenient way to do this. +/// +/// An extractor for extracting things we can use as specifications. This mostly +/// means that it extract things that we can turn into legal Verilog. +#[derive(Default)] +pub struct SpecExtractor; +impl SpecExtractor { + pub fn extract( + &self, + egraph: &egraph_serialize::EGraph, + _roots: &[egraph_serialize::ClassId], + ) -> IndexMap { + egraph + .classes() + .iter() + .map(|(id, class)| { + let node_id = class + .nodes + .iter() + .find(|node_id| { + let op = &egraph[*node_id].op; + + // Filter certain op types. + !(["PrimitiveInterfaceDSP", "Wire"].contains(&op.as_str())) + }) + .unwrap() + .clone(); + (id.clone(), node_id) + }) + .collect() + } +} + +/// For a given primitive interface term `term`, find an equivalent "concrete" +/// expression that we can use as our spec for synthesis via Lakeroad. +/// +/// Returns the node choides for each node in the egraph, plus the specific node +/// ID representing the spec. +pub fn find_spec_for_primitive_interface( + eclass: &egraph_serialize::ClassId, + serialized_egraph: &egraph_serialize::EGraph, +) -> (IndexMap, NodeId) { + let choices = SpecExtractor.extract(serialized_egraph, vec![].as_slice()); + let node_id = choices.get(eclass).unwrap().to_owned(); + (choices, node_id) +} + +/// For a given primitive interface term `term`, find an equivalent "concrete" +/// expression that we can use as our spec for synthesis via Lakeroad. This +/// version allows the caller to specify a set of nodes that must be extracted. +pub fn find_spec_for_primitive_interface_including_nodes( + eclass: &egraph_serialize::ClassId, + serialized_egraph: &egraph_serialize::EGraph, + ensure_extract: HashSet, +) -> (IndexMap, NodeId) { + let extractor = EnsureExtractSpecExtractor { ensure_extract }; + let choices = extractor.extract(serialized_egraph, vec![].as_slice()); + let node_id = choices.get(eclass).unwrap().to_owned(); + (choices, node_id) +} + +pub fn call_lakeroad_on_primitive_interface(term: &Term, term_dag: &TermDag) { + dbg!(term_dag.term_to_expr(term).to_string()); + + dbg!(to_verilog(term_dag, term_dag.lookup(term))); +} + +pub fn call_lakeroad() {} + +/// ``` +/// let mut egraph = churchroad::from_verilog( +/// "module identity(input i, output o); assign o = i; endmodule", +/// "identity", +/// true, +/// true, +/// [].into()); +/// egraph.parse_and_run_program(None, r#"(check (IsPort "" "i" (Input) i) (IsPort "" "o" (Output) o) (= i o))"#); +/// ``` +pub fn from_verilog( + verilog: &str, + top_module_name: &str, + simcheck: bool, + let_bindings: bool, + port_to_expr_map: HashMap, +) -> EGraph { + let mut f = NamedTempFile::new().unwrap(); + f.write_all(verilog.as_bytes()).unwrap(); + from_verilog_file( + f.path(), + top_module_name, + simcheck, + let_bindings, + port_to_expr_map, + ) +} + +/// Version of [`from_verilog`] that takes a filepath argument. +pub fn from_verilog_file( + verilog_filepath: &Path, + top_module_name: &str, + simcheck: bool, + let_bindings: bool, + port_to_expr_map: HashMap, +) -> EGraph { + let mut egraph = EGraph::default(); + import_churchroad(&mut egraph); + egraph + .parse_and_run_program( + None, + &commands_from_verilog_file( + verilog_filepath, + top_module_name, + simcheck, + let_bindings, + port_to_expr_map, + ), + ) + .unwrap(); + + egraph +} + +pub fn commands_from_verilog( + verilog: &str, + top_module_name: &str, + simcheck: bool, + let_bindings: bool, + port_to_expr_map: HashMap, +) -> String { + let mut f = NamedTempFile::new().unwrap(); + f.write_all(verilog.as_bytes()).unwrap(); + commands_from_verilog_file( + f.path(), + top_module_name, + simcheck, + let_bindings, + port_to_expr_map, + ) +} + +/// simcheck: whether to run `hierarchy` with `-simcheck`. +pub fn commands_from_verilog_file( + verilog_filepath: &Path, + top_module_name: &str, + simcheck: bool, + let_bindings: bool, + port_to_expr_map: HashMap, +) -> String { + fn spaces_to_underscores(s: &str) -> String { + assert!(!s.contains('_')); + s.replace(' ', "_") + } + // Convert the port_to_expr_map into "-portunion key value". + let port_union_flags: String = port_to_expr_map + .iter() + // TODO(@gussmith23): qouting here is a problem... + .map(|(port_name, expr)| { + format!("-portunion {} {}", port_name, spaces_to_underscores(expr)) + }) + .collect::>() + .join(" "); + + let logfile = NamedTempFile::new().unwrap(); + // TODO(@gussmith23): hardcoded .so will break on other systems. + let command_output = Command::new("yosys") + .arg("-m") + .arg( + Path::new(env!("CARGO_MANIFEST_DIR")) + .join("yosys-plugin") + .join("churchroad.so"), + ) + // Quiet, so the only output is Churchroad egglog code. + .arg("-q") + // Log useful information to a file. + .arg("-l") + .arg(logfile.path()) + .arg("-p") + .arg(format!( + "read_verilog -sv {path}; hierarchy {simcheck} -top {top_module_name}; prep; write_churchroad -salt {salt} {let_bindings_flag} {port_union_flags}", + path = verilog_filepath.to_str().unwrap(), + simcheck = if simcheck { "-simcheck" } else { "" }, + salt = SystemTime::now().duration_since(SystemTime::UNIX_EPOCH).unwrap().as_nanos(), + let_bindings_flag = if let_bindings { "-letbindings" } else { "" }, + port_union_flags = port_union_flags, + )) + .stdout(Stdio::piped()) + .output() + .expect("Couldn't run Yosys."); + + if !command_output.status.success() { + panic!( + "Yosys failed. Log:\n{}", + read_to_string(logfile.path()).unwrap() + ); + } + + String::from_utf8_lossy(&command_output.stdout).into_owned() +} + // The result of interpreting a Churchroad program. #[derive(Debug, PartialEq, Clone)] pub enum InterpreterResult { @@ -27,7 +873,7 @@ pub enum InterpreterResult { /// use egraph_serialize::NodeId; /// let mut egraph = EGraph::default(); /// import_churchroad(&mut egraph); -/// egraph.parse_and_run_program( +/// egraph.parse_and_run_program(None, /// r#" /// (let v0 (Wire "v0" 1)) /// (let v1 (Wire "v1" 1)) @@ -63,7 +909,8 @@ pub enum InterpreterResult { /// .unwrap(); /// /// let result = interpret(&serialized, &output_node.eclass, 0, -/// &[("a", vec![1]), ("b", vec![1])].into() +/// &[("a", vec![1]), ("b", vec![1])].into(), +/// None /// ); /// /// assert_eq!(result, Ok(InterpreterResult::Bitvector(1, 1))); @@ -74,9 +921,10 @@ pub fn interpret( class_id: &ClassId, time: usize, env: &HashMap<&str, Vec>, + choices: Option<&IndexMap>, ) -> Result { let result = match egraph.classes().iter().find(|(id, _)| *id == class_id) { - Some((id, _)) => interpret_helper(egraph, id, time, env, &mut HashMap::default()), + Some((id, _)) => interpret_helper(egraph, id, time, env, &mut HashMap::default(), choices), None => return Err("No class with the given ID.".to_string()), }; @@ -87,11 +935,9 @@ pub fn get_bitwidth_for_node( egraph: &egraph_serialize::EGraph, id: &NodeId, ) -> Result { - match egraph - .nodes - .iter() - .find(|(_, node)| node.op.as_str() == "HasType" && node.children[0] == *id) - { + match egraph.nodes.iter().find(|(_, node)| { + node.op.as_str() == "HasType" && egraph[&node.children[0]].eclass == egraph[id].eclass + }) { Some((_, has_type_node)) => { let type_node = egraph.nodes.get(&has_type_node.children[1]).unwrap(); assert!(type_node.op == "Bitvector"); @@ -105,7 +951,7 @@ pub fn get_bitwidth_for_node( .unwrap(); Ok(bw) } - None => return Err("No HasType node found for the given ID.".to_string()), + None => Err("No HasType node found for the given ID.".to_string()), } } @@ -125,20 +971,40 @@ fn interpret_helper( time: usize, env: &HashMap<&str, Vec>, cache: &mut HashMap<(ClassId, usize), InterpreterResult>, + choices: Option<&IndexMap>, ) -> Result { if cache.contains_key(&(id.clone(), time)) { return Ok(cache[&(id.clone(), time)].clone()); } - let node_ids = &egraph.classes().get(id).unwrap().nodes; - if node_ids.len() != 1 { - return Err(format!( - "There should be exactly one node in the class, but there are {}.", - node_ids.len() - )); - } - let node_id = node_ids.first().unwrap(); - let node = egraph.nodes.get(node_id).unwrap(); + // Get node. + let node_id = if let Some(choices) = choices { + choices.get(id).unwrap().to_owned() + } else { + let node_ids = egraph + .classes() + .get(id) + .unwrap() + .nodes + .iter() + .filter(|&node_id| egraph.nodes.get(node_id).unwrap().op != "Wire") + .cloned() + .collect::>(); + if node_ids.len() != 1 { + warn!( + "There is more than one node in the eclass. Will choose the first. Nodes:\n{}", + node_ids + .iter() + .map(|node_id| egraph.nodes.get(node_id).unwrap().op.clone()) + .collect::>() + .join("\n") + ); + } + + node_ids.first().unwrap().to_owned() + }; + + let node = egraph.nodes.get(&node_id).unwrap(); let result = match node.op.as_str() { "Var" => { @@ -169,7 +1035,7 @@ fn interpret_helper( if time == 0 { let clk = egraph.nodes.get(&node.children[1]).unwrap(); let InterpreterResult::Bitvector(curr_clk_val, _) = - interpret_helper(egraph, &clk.eclass, time, env, cache).unwrap(); + interpret_helper(egraph, &clk.eclass, time, env, cache, choices).unwrap(); assert_eq!( curr_clk_val, 0, "We don't currently know what to do when clk=1 at time 0! See #88" @@ -182,15 +1048,16 @@ fn interpret_helper( } else { let clk = egraph.nodes.get(&node.children[1]).unwrap(); let InterpreterResult::Bitvector(prev_clk_val, _) = - interpret_helper(egraph, &clk.eclass, time - 1, env, cache).unwrap(); + interpret_helper(egraph, &clk.eclass, time - 1, env, cache, choices) + .unwrap(); let InterpreterResult::Bitvector(curr_clk_val, _) = - interpret_helper(egraph, &clk.eclass, time, env, cache).unwrap(); + interpret_helper(egraph, &clk.eclass, time, env, cache, choices).unwrap(); if prev_clk_val == 0 && curr_clk_val == 1 { let d = egraph.nodes.get(&node.children[2]).unwrap(); - return interpret_helper(egraph, &d.eclass, time - 1, env, cache); + return interpret_helper(egraph, &d.eclass, time - 1, env, cache, choices); } else { - return interpret_helper(egraph, id, time - 1, env, cache); + return interpret_helper(egraph, id, time - 1, env, cache, choices); } } } @@ -200,7 +1067,7 @@ fn interpret_helper( .skip(1) .map(|id| { let child = egraph.nodes.get(id).unwrap(); - interpret_helper(egraph, &child.eclass, time, env, cache) + interpret_helper(egraph, &child.eclass, time, env, cache, choices) }) .collect(); @@ -463,15 +1330,22 @@ impl AnythingExtractor { } } +/// - bottom_out_at: maps ClassIds to variable names. Any time we reach a node +/// with a class ID in this map, we simply output a variable with the given +/// name. +/// - outputs: maps ClassIds to variable names. These classes will be taken as +/// the outputs of the module. If not specified, we output all output ports. pub fn to_verilog_egraph_serialize( egraph: &egraph_serialize::EGraph, choices: &IndexMap, clk_name: &str, + bottom_out_at: HashMap, + outputs: Option>, ) -> String { // let mut wires = HashMap::default(); fn id_to_wire_name(id: &ClassId) -> String { - format!("wire_{}", id) + format!("wire_{}", id.to_string().replace('-', "_")) } struct ModuleInstance { @@ -484,68 +1358,94 @@ pub fn to_verilog_egraph_serialize( // Maps EClass ID to the module instance at that class. let mut module_instantiations: HashMap = HashMap::new(); - let mut inputs = String::new(); - let mut outputs = String::new(); + let mut inputs_str = String::new(); + let mut outputs_str = String::new(); let mut logic_declarations = String::new(); let mut registers = String::new(); // Collect all the outputs. - let mut queue: Vec = egraph - .nodes - .iter() - .filter_map(|(_id, node)| { + let mut queue: Vec = if let Some(outputs) = &outputs { + outputs.keys().cloned().collect() + } else { + egraph + .nodes + .iter() + .filter_map(|(_id, node)| { + // op should be IsPort + let op = &node.op; + if op != "IsPort" { + return None; + } + + assert_eq!(node.children.len(), 4); + + if egraph[&node.children[2]].op != "Output" { + return None; + } + + Some(egraph[&node.children[3]].eclass.clone()) + }) + .collect() + }; + + // Generate outputs. + if let Some(outputs) = &outputs { + for (class_id, name) in outputs { + log::debug!("Outputting class {} as {}", class_id, name); + let node_id = &choices[class_id]; + let term = &egraph[node_id]; + let bw = get_bitwidth_for_node(egraph, node_id).unwrap(); + + outputs_str.push_str(&format!( + "output [{bw}-1:0] {name},\n", + bw = bw, + name = name + )); + + logic_declarations.push_str(&format!( + "assign {name} = {wire};\n", + name = name, + wire = id_to_wire_name(&term.eclass) + )); + } + } else { + for (_, node) in egraph.nodes.iter() { // op should be IsPort let op = &node.op; if op != "IsPort" { - return None; + continue; } assert_eq!(node.children.len(), 4); if egraph[&node.children[2]].op != "Output" { - return None; + continue; } - Some(egraph[&node.children[3]].eclass.clone()) - }) - .collect(); - - // Generate outputs. - for (_, node) in egraph.nodes.iter() { - // op should be IsPort - let op = &node.op; - if op != "IsPort" { - continue; - } - - assert_eq!(node.children.len(), 4); - - if egraph[&node.children[2]].op != "Output" { - continue; + outputs_str.push_str(&format!( + "output [{bw}-1:0] {name},\n", + bw = get_bitwidth_for_node(egraph, &node.children[3]).unwrap(), + name = egraph[&node.children[1]] + .op + .as_str() + .strip_prefix('\"') + .unwrap() + .strip_suffix('\"') + .unwrap() + )); + + logic_declarations.push_str(&format!( + "assign {name} = {wire};\n", + name = egraph[&node.children[1]] + .op + .as_str() + .strip_prefix('\"') + .unwrap() + .strip_suffix('\"') + .unwrap(), + wire = id_to_wire_name(&egraph[&node.children[3]].eclass) + )) } - - outputs.push_str(&format!( - "output {name},\n", - name = egraph[&node.children[1]] - .op - .as_str() - .strip_prefix('\"') - .unwrap() - .strip_suffix('\"') - .unwrap() - )); - - logic_declarations.push_str(&format!( - "logic {name} = {wire};\n", - name = egraph[&node.children[1]] - .op - .as_str() - .strip_prefix('\"') - .unwrap() - .strip_suffix('\"') - .unwrap(), - wire = id_to_wire_name(&egraph[&node.children[3]].eclass) - )) } let mut done = HashSet::new(); @@ -562,7 +1462,37 @@ pub fn to_verilog_egraph_serialize( while let Some(id) = queue.pop() { done.insert(id.clone()); - let term = &egraph[&choices[&id]]; + let node_id = &choices[&id]; + // This can cause an infinite loop! + // log::debug!( + // "just popped {:?}, expr {}, queue is {:?}", + // id, + // node_to_string(egraph, node_id, choices), + // queue + // ); + let term = &egraph[node_id]; + + // First, handle the case where we're supposed to "bottom out" at this + // node, i.e. output a variable name instead of the rest of the + // expression. + if let Some(name) = bottom_out_at.get(&id) { + log::debug!("Bottoming out at node with name {}", name); + let bw = get_bitwidth_for_node(egraph, node_id).unwrap(); + + inputs_str + .push_str(format!("input [{bw}-1:0] {name},\n", bw = bw, name = name).as_str()); + + logic_declarations.push_str( + format!( + "logic [{bw}-1:0] {this_wire} = {name};\n", + bw = bw, + this_wire = id_to_wire_name(&term.eclass), + name = name + ) + .as_str(), + ); + continue; + } let op = &term.op; match op.as_str() { @@ -575,6 +1505,7 @@ pub fn to_verilog_egraph_serialize( "Input" | "Output" | // Ignore the nodes for the ops themselves. + "CRString" | "ZeroExtend" | "Concat" | "Extract" | @@ -597,14 +1528,31 @@ pub fn to_verilog_egraph_serialize( let bw = egraph[&op_node.children[0]].op.parse::().unwrap(); logic_declarations.push_str( format!( - "logic [{bw}-1:0] {this_wire} = {bw}'d{value};\n", + "logic [{bw}-1:0] {this_wire} = {bw}'({value});\n", this_wire = id_to_wire_name(&id), value = id_to_wire_name(&egraph[&term.children[1]].eclass) ) .as_str(), ); + maybe_push_expr_on_queue(&mut queue, &done, &egraph[&term.children[1]].eclass); + } + "CRString" => { + assert_eq!(op_node.children.len(), 1); + let value = &egraph[&op_node.children[0]].op; + logic_declarations.push_str( + // The string already has quotes in it. This may not + // always be the case. Should be careful here in the + // future. + format!( + // Localparam so that it's a constant. + "localparam [{}*8:0] {this_wire} = {value};\n", + value.len()-2, + this_wire = id_to_wire_name(&id), + ) + .as_str(), + ); } "BV" => { assert_eq!(op_node.children.len(), 2); @@ -613,7 +1561,8 @@ pub fn to_verilog_egraph_serialize( logic_declarations.push_str( format!( - "logic [{bw}-1:0] {this_wire} = {bw}'d{value};\n", + // Localparam so that it's a constant. + "localparam [{bw}-1:0] {this_wire} = {bw}'d{value};\n", this_wire = id_to_wire_name(&id), ) .as_str(), @@ -626,7 +1575,8 @@ pub fn to_verilog_egraph_serialize( logic_declarations.push_str( format!( - "logic {this_wire} = {default};\n", + "logic [{bw}-1:0] {this_wire} = {default};\n", + bw = get_bitwidth_for_node(egraph, node_id).unwrap(), this_wire = id_to_wire_name(&id), default = default_val ) @@ -646,27 +1596,36 @@ pub fn to_verilog_egraph_serialize( queue.push(d_id.clone()); } }, - "Concat" | "Xor" |"And" | "Or" => { - assert_eq!(term.children.len(), 3); + "Concat" | "Xor" |"And" | "Or" | "Mul" | "Add" => { + assert_eq!(term.children.len(), 3, "Found {} op with #children = {}", op_node.op, term.children.len()); let expr0_id = &egraph[&term.children[1]].eclass; let expr1_id = &egraph[&term.children[2]].eclass; logic_declarations.push_str(&format!( - "logic {this_wire} = {op};\n", + "logic [{bw}-1:0] {this_wire} = {op};\n", + bw = get_bitwidth_for_node(egraph, node_id).unwrap(), op = match op_node.op.as_str() { "Concat" => format!("{{ {expr0}, {expr1} }}", expr0 = id_to_wire_name(expr0_id), expr1 = id_to_wire_name(expr1_id), ), - "Xor" => format!("{expr0}^{expr1}", + "Xor" => format!("({expr0}^{expr1})", + expr0 = id_to_wire_name(expr0_id), + expr1 = id_to_wire_name(expr1_id), + ), + "And" => format!("({expr0}&{expr1})", expr0 = id_to_wire_name(expr0_id), expr1 = id_to_wire_name(expr1_id), ), - "And" => format!("{expr0}&{expr1}", + "Or" => format!("({expr0}|{expr1})", expr0 = id_to_wire_name(expr0_id), expr1 = id_to_wire_name(expr1_id), ), - "Or" => format!("{expr0}|{expr1}", + "Mul" => format!("({expr0}*{expr1})", + expr0 = id_to_wire_name(expr0_id), + expr1 = id_to_wire_name(expr1_id), + ), + "Add" => format!("({expr0}+{expr1})", expr0 = id_to_wire_name(expr0_id), expr1 = id_to_wire_name(expr1_id), ), @@ -686,7 +1645,8 @@ pub fn to_verilog_egraph_serialize( let id = &term.eclass; let expr_id = &egraph[&term.children[1]].eclass; logic_declarations.push_str(&format!( - "logic {this_wire} = {expr}[{hi}:{lo}];\n", + "logic [{bw}-1:0] {this_wire} = {expr}[{hi}:{lo}];\n", + bw = get_bitwidth_for_node(egraph, node_id).unwrap(), hi = hi, lo = lo, this_wire = id_to_wire_name(id), @@ -695,6 +1655,31 @@ pub fn to_verilog_egraph_serialize( maybe_push_expr_on_queue(&mut queue, &done, expr_id); } + "Shl" => { + assert_eq!(term.children.len(), 3); + + // These only have to hold for structural verilog. These + // checks should be removed in the future once I figure out + // how to deal with shifts in structural Verilog. (namely, + // do we want to allow shifts, or do we want to convert them + // to something else using rewrites and constant + // propagation?) + assert!(egraph[&term.children[2]].op == "Op0"); + assert!(egraph[&egraph[&term.children[2]].children[0]].op == "BV"); + + let id = &term.eclass; + let e0_id = egraph.nid_to_cid(&term.children[1]); + let e1_id = egraph.nid_to_cid(&term.children[2]); + logic_declarations.push_str(&format!( + "logic [{bw}-1:0] {this_wire} = {e0} << {e1};\n", + bw = get_bitwidth_for_node(egraph, node_id).unwrap(), + this_wire = id_to_wire_name(id), + e0 = id_to_wire_name(e0_id), + e1 = id_to_wire_name(e1_id) + )); + maybe_push_expr_on_queue(&mut queue, &done, e0_id); + maybe_push_expr_on_queue(&mut queue, &done, e1_id); + } v => todo!("{:?}", v), @@ -708,7 +1693,7 @@ pub fn to_verilog_egraph_serialize( let name = egraph[&term.children[0]].op.as_str().strip_prefix('\"').unwrap().strip_suffix('\"').unwrap(); let bw: i64 = egraph[&term.children[1]].op.parse().unwrap(); - inputs.push_str( + inputs_str.push_str( format!("input [{bw}-1:0] {name},\n", bw = bw, name = name).as_str(), ); @@ -781,7 +1766,7 @@ pub fn to_verilog_egraph_serialize( if !module_instantiations.contains_key(module_class) { module_instantiations.insert(module_class.clone(), ModuleInstance { module_class_name: module_class_name.to_owned(), - instance_name: format!("module_{}", module_class), + instance_name: format!("module_{}", module_class.to_string().replace('-', "_")), parameters: parameter_names.into_iter().zip(parameter_exprs.into_iter()).collect(), inputs: input_port_names.into_iter().zip(input_port_exprs.into_iter()).collect(), outputs: [(output_name.to_owned(), term.eclass.clone())].into(), @@ -794,7 +1779,8 @@ pub fn to_verilog_egraph_serialize( logic_declarations.push_str( format!( - "logic {this_wire};\n", + "logic [{bw}-1:0] {this_wire};\n", + bw = get_bitwidth_for_node(egraph, node_id).unwrap(), this_wire = id_to_wire_name(&term.eclass), ) .as_str(), @@ -972,7 +1958,7 @@ pub fn to_verilog_egraph_serialize( // For display purposes, we can clean this up later. // We sort to make the output stable. let inputs = { - let mut out = inputs + let mut out = inputs_str .split('\n') .map(|line| format!(" {}", line)) .collect::>(); @@ -981,7 +1967,7 @@ pub fn to_verilog_egraph_serialize( out.join("\n") }; let outputs = { - let mut out = outputs + let mut out = outputs_str .split('\n') .map(|line| format!(" {}", line)) .collect::>(); @@ -1257,7 +2243,13 @@ pub fn to_verilog(term_dag: &TermDag, id: usize) -> String { pub fn import_churchroad(egraph: &mut EGraph) { // STEP 1: import primary language definitions. egraph - .parse_and_run_program(r#"(include "egglog_src/churchroad.egg")"#) + .parse_and_run_program( + None, + &format!( + r#"(include "{}/egglog_src/churchroad.egg")"#, + std::env::var("CARGO_MANIFEST_DIR").unwrap() + ), + ) .unwrap(); // STEP 2: add the `debruijnify` primitive to the egraph. This depends on @@ -1268,7 +2260,13 @@ pub fn import_churchroad(egraph: &mut EGraph) { // STEP 3: import module enumeration rewrites. These depend on the // `debruijnify` primitive. egraph - .parse_and_run_program(r#"(include "egglog_src/module_enumeration_rewrites.egg")"#) + .parse_and_run_program( + None, + &format!( + r#"(include "{}/egglog_src/module_enumeration_rewrites.egg")"#, + std::env::var("CARGO_MANIFEST_DIR").unwrap() + ), + ) .unwrap(); } @@ -1285,10 +2283,11 @@ fn add_debruijnify(egraph: &mut EGraph) { "debruijnify".into() } - fn get_type_constraints(&self) -> Box { + fn get_type_constraints(&self, span: &Span) -> Box { Box::new(SimpleTypeConstraint::new( self.name(), vec![self.in_sort.clone(), self.out_sort.clone()], + span.clone(), )) } @@ -1507,6 +2506,7 @@ pub fn generate_module_enumeration_rewrite( pub fn list_modules(egraph: &mut EGraph, num_variants: usize) { for s in egraph .parse_and_run_program( + None, format!("(query-extract :variants {num_variants} (MakeModule mod args))").as_str(), ) .unwrap() @@ -1527,7 +2527,7 @@ type Ports = Vec<(String, ArcSort, Value)>; /// /// import_churchroad(&mut egraph); /// egraph -/// .parse_and_run_program( +/// .parse_and_run_program(None, /// r#" /// ; wire declarations /// ; $and$< (Ports, Ports) { let churchroad_term = children[3]; + let term_str = termdag.to_string(&termdag.get(churchroad_term)); let (sort, value) = egraph .eval_expr( &egglog::ast::parse::ExprParser::new() - .parse(&termdag.to_string(&termdag.get(churchroad_term))) + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: Some(term_str.clone()), + }), + &term_str, + ) .unwrap(), ) .unwrap(); @@ -1664,7 +2671,7 @@ type PortsFromSerialized = Vec<(String, ClassId)>; /// let mut egraph = EGraph::default(); /// import_churchroad(&mut egraph); /// egraph -/// .parse_and_run_program( +/// .parse_and_run_program(None, /// r#" /// ; wire declarations /// ; $and$<, + + #[arg(long)] + architecture: Architecture, + + #[arg(long)] + simulate: bool, + + #[arg(long)] + out_filepath: Option, + + #[arg(long, action=ArgAction::Append)] + simulate_with_verilator_arg: Vec, +} + +#[derive(ValueEnum, Clone, Debug)] +enum Architecture { + XilinxUltrascalePlus, +} + +/// Run commands to interact with the egraph. +fn _egraph_interact(egraph: &mut EGraph) { + loop { + print!("> "); + stdout().flush().unwrap(); + let mut buf = String::new(); + stdin().read_line(&mut buf).unwrap(); + let out = egraph.parse_and_run_program(None, &buf); + if let Ok(out) = out { + println!("{}", out.join("\n")); + } else { + println!("Error: {:?}", out); + } + } +} + +// TODO(@gussmith23): Seems redundant to do this; I think clap already does something like this under the hood. +impl Display for Architecture { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + Architecture::XilinxUltrascalePlus => f.write_str("xilinx-ultrascale-plus"), + } + } +} + +fn main() { + env_logger::init(); + let args = Args::parse(); + + // STEP 1: Read in design, put it in an egraph. + // simcheck=true just runs some basic checks. + let mut egraph = from_verilog_file( + &args.filepath, + &args.top_module_name, + true, + true, + HashMap::default(), + ); + + info!("Loaded design into egraph."); + + // Get initial input and output ports. + let outputs: Vec<_> = { + let serialized = egraph.serialize(SerializeConfig::default()); + get_inputs_and_outputs_serialized(&serialized) + .1 + .drain(..) + .map(|(output_name, class_id)| (egraph.class_id_to_value(&class_id), output_name)) + .collect() + }; + + let output_names_and_bws: Vec<_> = { + let serialized = egraph.serialize(SerializeConfig::default()); + get_inputs_and_outputs_serialized(&serialized) + .1 + .drain(..) + .map(|(output_name, class_id)| { + ( + output_name, + get_bitwidth_for_node(&serialized, &serialized[&class_id].nodes[0]).unwrap(), + ) + }) + .collect() + }; + let input_names_and_bws: Vec<_> = { + let serialized = egraph.serialize(SerializeConfig::default()); + get_inputs_and_outputs_serialized(&serialized) + .0 + .drain(..) + .map(|(input_name, class_id)| { + ( + input_name, + get_bitwidth_for_node(&serialized, &serialized[&class_id].nodes[0]).unwrap(), + ) + }) + .collect() + }; + + if let Some(svg_dirpath) = &args.svg_dirpath { + create_dir_all(svg_dirpath).unwrap(); + let serialized = egraph.serialize_for_graphviz(true, usize::MAX, usize::MAX); + serialized + .to_svg_file(svg_dirpath.join("initial_egraph.svg")) + .unwrap(); + info!( + "Initial egraph svg: {}", + svg_dirpath.join("initial_egraph.svg").to_string_lossy() + ); + } + + // STEP 2: Run mapping rewrites, proposing potential mappings which Lakeroad + // will later confirm or prove not possible via program synthesis. + // + // Currently, we only have a single rewrite, which looks for "narrower" + // multiplies which should fit on a single DSP. + // + // In the future, there's much more we can do here, including: + // - Parameterizing rewrites based on architecture (i.e. instead of + // hardcoding "18" below, we can get the appropriate width from the + // architecture description.) + // - Mixing mapping rewrites with "expansion" rewrites. For example, adding + // a rewrite which breaks a large multiply into smaller multiplies. Again, + // these rewrites can also be parameterized by arch. descr. + // - Automated generation of rewrites. This is a more interesting research + // question! Could be a place we use ChatGPT; i.e. give it the PDF of + // the DSP manual, give it a description of the Churchroad IR, and ask it + // to propose patterns. + info!("Running rewrites."); + egraph + .parse_and_run_program( + None, + r#" + (ruleset mapping) + ;; TODO need to write a rewrite that deals with multiplying zero extended bvs + (rule + ((= expr (Op2 (Mul) a b)) + (HasType expr (Bitvector n)) + (< n 18)) + ((union expr (PrimitiveInterfaceDSP a b))) + :ruleset mapping) + ;; TODO bitwidths are hardcoded here + (rule + ((= expr (Op2 (Mul) (Op1 (ZeroExtend ?n) ?a) (Op1 (ZeroExtend ?n) ?b))) + (HasType expr (Bitvector ?n)) + (HasType ?a (Bitvector ?a-bw)) + (HasType ?b (Bitvector ?b-bw)) + (<= ?a-bw 16) + (<= ?b-bw 16) + (< ?n 36) + ) + ((union expr (PrimitiveInterfaceDSP ?a ?b))) + :ruleset mapping) + (rule + ((= expr (Op2 (Add) (Op2 (Mul) (Op1 (ZeroExtend ?n) ?a) (Op1 (ZeroExtend ?n) ?b)) ?c)) + (HasType expr (Bitvector ?n)) + (HasType ?a (Bitvector ?a-bw)) + (HasType ?b (Bitvector ?b-bw)) + (HasType ?c (Bitvector ?c-bw)) + (<= ?a-bw 16) + (<= ?b-bw 16) + (<= ?c-bw 48) + (< ?n 36) + ) + ((union expr (PrimitiveInterfaceDSP3 ?a ?b ?c))) + :ruleset mapping) + + (ruleset transform) + (rule + ((= expr (Op2 (Mul) (Op1 (ZeroExtend b-bw) a) b)) + (HasType expr (Bitvector expr-bw)) + (HasType a (Bitvector a-bw)) + (HasType b (Bitvector b-bw)) + (<= expr-bw 48) + (<= a-bw 16) + (<= b-bw 32) + (= 0 (% expr-bw 2))) + ((union + expr + (Op2 (Add) + (Op2 (Mul) (Op1 (ZeroExtend expr-bw) a) (Op1 (ZeroExtend expr-bw) (Op1 (Extract (- (/ expr-bw 2) 1) 0) b))) + (Op2 (Shl) (Op2 (Mul) (Op1 (ZeroExtend expr-bw) a) (Op1 (ZeroExtend expr-bw) (Op1 (Extract (- expr-bw 1) (/ expr-bw 2)) b))) (Op0 (BV (/ expr-bw 2) expr-bw)))))) + :ruleset transform) + "#, + ) + .unwrap(); + egraph + .parse_and_run_program( + None, + "(run-schedule (saturate (seq typing transform mapping)))", + ) + .unwrap(); + + // egraph_interact(&mut egraph); + + // May need this rebuild. See + // https://github.com/egraphs-good/egglog/pull/391 + // egraph.rebuild(); + + if let Some(svg_dirpath) = &args.svg_dirpath { + create_dir_all(svg_dirpath).unwrap(); + let serialized = egraph.serialize_for_graphviz(true, usize::MAX, usize::MAX); + serialized + .to_svg_file(svg_dirpath.join("after_rewrites.svg")) + .unwrap(); + info!( + "Egraph after rewrites: {}", + svg_dirpath.join("after_rewrites.svg").to_string_lossy() + ); + } + + let serialized_egraph = egraph.serialize(SerializeConfig::default()); + + // STEP 3: Collect all proposed mappings. + // In this step, we simply find all mapping proposals, i.e. all places where + // the above rewrites *think* we might be able to use a DSP. In the next + // step, we'll actually confirm or deny whether these mappings can work. + // + // In the future, this step might also involve ranking potential mapping + // proposals, because in a large design, there will likely be many of them! + // There are many potential ways to rank: heuristics, cost models, etc. + // + // + // TODO(@gussmith23): Make this return Vec<(choices, nodeid)>. + // Basically it can have the same API as the spec finding function. They're + // both doing very similar things: basically, an extraction. They're just + // extracting different things for the same classes. + let node_ids = find_primitive_interfaces_serialized(&serialized_egraph); + + info!( + "Found {} potential mappings; running Lakeroad on each.", + node_ids.len() + ); + + // STEP 5: For each proposed mapping, attempt synthesis with Lakeroad. + for sketch_template_node_id in &node_ids { + // TODO(@gussmith23): This is a hack, see https://github.com/egraphs-good/egglog/issues/392 + // Doing everything over the serialized egraph, so I don't actually need this anymore. + // let canonical: usize = egraph.find(*value).bits.try_into().unwrap(); + // let canonical_id: egraph_serialize::ClassId = canonical.to_string().into(); + // let (choices, spec_node_id) = + // find_spec_for_primitive_interface(&canonical_id, &serialized_egraph); + + // STEP 5.1: For each proposed mapping, extract a "spec". + // In the above step, we extracted all of the proposed mapping nodes. + // These nodes are just markers that say "this eclass could potentially + // be implemented with a DSP." To actually do synthesis with Lakeroad, + // we need to extract *yet another* representative from the eclass: + // one that can serve as a specification which Lakeroad can synthesize + // against. Currently, this mostly just means extracting *any* + // expression from the eclass which can be converted to valid Verilog. + // + // In the future, we could also consider extracting *multiple* + // representatives per eclass, which gives us more specs to attempt + // synthesis against. Given that solvers are strange and often benefit + // from running in a portfolio, having many equivalent specs might + // increase chances at synthesis termination. + let (spec_choices, spec_node_id) = find_spec_for_primitive_interface_including_nodes( + &serialized_egraph[sketch_template_node_id].eclass, + &serialized_egraph, + // Use the children of the sketch template node as the required-to-be-extracted nodes. + serialized_egraph[sketch_template_node_id] + .children + .iter() + .cloned() + .collect(), + ); + + log::info!( + "Calling Lakeroad with spec:\n{}\nand sketch:\n{}", + node_to_string(&serialized_egraph, &spec_node_id, &spec_choices), + serialized_egraph[sketch_template_node_id].op + ); + + // STEP 5.2: Call Lakeroad. + let commands = call_lakeroad_on_primitive_interface_and_spec( + &serialized_egraph, + &spec_choices, + &spec_node_id, + sketch_template_node_id, + &args.architecture.to_string(), + ); + + log::debug!( + "First few lines of commands generated from Lakeroad output:\n{}", + commands.lines().take(10).collect::>().join("\n") + ); + + // STEP 5.3: Insert Lakeroad's results back into the egraph. + // If Lakeroad finds a mapping, insert the mapping into the egraph. + // If Lakeroad proves UNSAT, put some kind of marker into the egraph + // to indicate that this mapping shouldn't be attempted again. + egraph.parse_and_run_program(None, &commands).unwrap(); + + info!("Inserted Lakeroad's results back into egraph."); + + // Write out image if the user requested it. + if let Some(svg_dirpath) = &args.svg_dirpath { + let serialized = egraph.serialize_for_graphviz(true, usize::MAX, usize::MAX); + serialized + .to_svg_file(svg_dirpath.join("during_lakeroad.svg")) + .unwrap(); + info!( + "Egraph after nth call to Lakeroad: {}", + svg_dirpath.join("during_lakeroad.svg").to_string_lossy() + ); + } + } + + // Write out image if the user requested it. + if let Some(svg_dirpath) = args.svg_dirpath { + let serialized = egraph.serialize_for_graphviz(true, usize::MAX, usize::MAX); + serialized + .to_svg_file(svg_dirpath.join("after_lakeroad.svg")) + .unwrap(); + info!( + "Egraph after all calls to Lakeroad: {}", + svg_dirpath.join("after_lakeroad.svg").to_string_lossy() + ); + } + + // STEP 6: Extract a lowered design. + // + // Once we have attempted all mappings, we should ideally be able to extract + // a design in structural Verilog. + // + // Future work at this stage will involve building an extractor which + // which actually attempts to find an *optimal* design, not just *any* + // design. + + let serialized = egraph.serialize(SerializeConfig::default()); + let choices = GlobalGreedyDagExtractor { + structural_only: true, + } + .extract(&serialized, &[]); + let verilog = to_verilog_egraph_serialize( + &serialized, + &choices, + "clk", + [].into(), + // Use the original outputs as the outputs of the final design. + Some( + outputs + .iter() + .cloned() + .map(|(value, output_name)| { + (egraph.value_to_class_id(&egraph.find(value)), output_name) + }) + .collect(), + ), + ); + + debug!("Final extracted Verilog:\n{}", &verilog); + + if let Some(out_filepath) = &args.out_filepath { + std::fs::write(out_filepath, &verilog).unwrap(); + } else { + println!("{}", verilog); + } + + // STEP 7: Simulate. + if args.simulate { + // If we didn't write to file, we need to write to a temp file. + let old_verilog_filepath = if let Some(out_filepath) = &args.out_filepath { + out_filepath.to_owned() + } else { + let (_, path) = NamedTempFile::new().unwrap().keep().unwrap(); + std::fs::write(&path, &verilog).unwrap(); + path + }; + + // First, we have to rename the output module, because our + // simulate_with_verilator.py script can't simulate two modules with the + // same name against each other. + let verilog_file = NamedTempFile::new().unwrap(); + // Use Yosys to rename the module. + let new_module_name = format!("{}_simulate_with_verilator", args.top_module_name); + let yosys_output = std::process::Command::new("yosys") + .arg("-p") + .arg(format!( + "read_verilog -sv {}; rename {} {}; write_verilog {}", + old_verilog_filepath.to_string_lossy(), + //args.top_module_name, + { + warn!("TODO(@gussmith23): hardcoded."); + "top" + }, + new_module_name, + verilog_file.path().to_string_lossy() + )) + .output() + .unwrap(); + if !yosys_output.status.success() { + panic!( + "Yosys failed to rename the module. stdout:\n{}\nstderr:\n{}", + String::from_utf8_lossy(&yosys_output.stdout), + String::from_utf8_lossy(&yosys_output.stderr) + ); + } + + let lakeroad_dir = PathBuf::from( + std::env::var("LAKEROAD_DIR") + .expect("LAKEROAD_DIR environment variable should be set."), + ); + + let mut cmd = std::process::Command::new("python3"); + cmd.arg(lakeroad_dir.join("bin").join("simulate_with_verilator.py")) + .arg("--verilog_filepath") + .arg(verilog_file.path()) + .arg("--test_module_name") + .arg(new_module_name) + .arg("--ground_truth_module_name") + .arg(args.top_module_name) + .arg("--verilator_extra_arg") + .arg(args.filepath) + .args(args.simulate_with_verilator_arg); + + for input in &input_names_and_bws { + cmd.arg("--input_signal") + .arg(format!("{}:{}", input.0, input.1)); + } + for output in &output_names_and_bws { + cmd.arg("--output_signal") + .arg(format!("{}:{}", output.0, output.1)); + } + + let output = cmd.output().unwrap(); + + if !output.status.success() { + panic!( + "Simulation with Verilator failed. stdout:\n{}\nstderr:\n{}", + String::from_utf8_lossy(&output.stdout), + String::from_utf8_lossy(&output.stderr) + ); + } + + info!("Simulation with Verilator succeeded."); + } +} diff --git a/tests/egglog_tests.rs b/tests/egglog_tests.rs index 1934f82..1a745c5 100644 --- a/tests/egglog_tests.rs +++ b/tests/egglog_tests.rs @@ -1,9 +1,9 @@ use egglog::{ - ast::{parse::ExprParser, Expr}, + ast::{parse::ExprParser, Expr, Span, SrcFile}, ArcSort, EGraph, TermDag, Value, }; use log::warn; -use std::{collections::HashMap, path::Path}; +use std::{collections::HashMap, path::Path, sync::Arc}; macro_rules! egglog_test { ($name:ident, $path:literal) => { @@ -16,6 +16,7 @@ macro_rules! egglog_test { churchroad::import_churchroad(&mut egraph); egraph .parse_and_run_program( + None, &std::fs::read_to_string(Path::new(env!("CARGO_MANIFEST_DIR")).join($path)) .unwrap(), ) @@ -65,7 +66,7 @@ fn create_rewrites( let mut exprs: Vec<_> = (0..num_rewrites) .map(|seed| extract_random(egraph, value, sort, seed)) .collect(); - exprs.sort(); + exprs.sort_by_key(|expr| expr.to_string()); exprs.dedup(); if exprs.len() < num_rewrites.try_into().unwrap() { @@ -115,7 +116,17 @@ egglog_test!( "tests/egglog_tests/agilex_alm.egg", |egraph: &mut EGraph| { let (sort, value) = egraph - .eval_expr(&egglog::ast::Expr::Var((), "lut6out".into())) + .eval_expr(&egglog::ast::Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "lut6out".into(), + )) .unwrap(); create_rewrites( egraph, @@ -124,59 +135,259 @@ egglog_test!( 1, &vec![ ( - ExprParser::new().parse("(Var \"a\" 1)").unwrap(), - Expr::Var((), "a".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"a\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "a".into(), + ), ), ( - ExprParser::new().parse("(Var \"b\" 1)").unwrap(), - Expr::Var((), "b".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"b\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "b".into(), + ), ), ( - ExprParser::new().parse("(Var \"c0\" 1)").unwrap(), - Expr::Var((), "c0".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"c0\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "c0".into(), + ), ), ( - ExprParser::new().parse("(Var \"c1\" 1)").unwrap(), - Expr::Var((), "c1".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"c1\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "c1".into(), + ), ), ( - ExprParser::new().parse("(Var \"d0\" 1)").unwrap(), - Expr::Var((), "d0".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"d0\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "d0".into(), + ), ), ( - ExprParser::new().parse("(Var \"d1\" 1)").unwrap(), - Expr::Var((), "d1".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"d1\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "d1".into(), + ), ), ( - ExprParser::new().parse("(Var \"e\" 1)").unwrap(), - Expr::Var((), "e".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"e\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "e".into(), + ), ), ( - ExprParser::new().parse("(Var \"f\" 1)").unwrap(), - Expr::Var((), "f".into()), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"f\" 1)", + ) + .unwrap(), + Expr::Var( + Span( + Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + 0, + 0, + ), + "f".into(), + ), ), ( - ExprParser::new().parse("(Var \"lut4_g0_mem\" 16)").unwrap(), ExprParser::new() - .parse("(Symbolic \"lut4_g0_mem\" 16)") + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"lut4_g0_mem\" 16)", + ) + .unwrap(), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Symbolic \"lut4_g0_mem\" 16)", + ) .unwrap(), ), ( - ExprParser::new().parse("(Var \"lut4_p0_mem\" 16)").unwrap(), ExprParser::new() - .parse("(Symbolic \"lut4_p0_mem\" 16)") + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"lut4_p0_mem\" 16)", + ) + .unwrap(), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Symbolic \"lut4_p0_mem\" 16)", + ) .unwrap(), ), ( - ExprParser::new().parse("(Var \"lut4_g1_mem\" 16)").unwrap(), ExprParser::new() - .parse("(Symbolic \"lut4_g1_mem\" 16)") + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"lut4_g1_mem\" 16)", + ) + .unwrap(), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Symbolic \"lut4_g1_mem\" 16)", + ) .unwrap(), ), ( - ExprParser::new().parse("(Var \"lut4_p1_mem\" 16)").unwrap(), ExprParser::new() - .parse("(Symbolic \"lut4_p1_mem\" 16)") + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Var \"lut4_p1_mem\" 16)", + ) + .unwrap(), + ExprParser::new() + .parse( + &Arc::new(SrcFile { + name: "unused".to_owned(), + contents: None, + }), + "(Symbolic \"lut4_p1_mem\" 16)", + ) .unwrap(), ), ] @@ -195,6 +406,7 @@ fn antiunify() { egraph .parse_and_run_program( + None, r#" (let out (debruijnify (vec-of (Var "x" 8) (Var "y" 16)))) (check (= out (vec-of 0 1))) @@ -261,6 +473,7 @@ fn antiunify_permuter() { egraph .parse_and_run_program( + None, r#" (include "tests/egglog_tests/permuter.egg") "#, @@ -269,15 +482,15 @@ fn antiunify_permuter() { // Run enumeration rewrites egraph - .parse_and_run_program("(run-schedule (saturate enumerate-modules))") + .parse_and_run_program(None, "(run-schedule (saturate enumerate-modules))") .unwrap(); egraph - .parse_and_run_program("(run-schedule (saturate typing))") + .parse_and_run_program(None, "(run-schedule (saturate typing))") .unwrap(); egraph - .parse_and_run_program("(run-schedule (repeat 100 (seq (run expansion) (saturate typing) (saturate enumerate-modules))))") + .parse_and_run_program(None,"(run-schedule (repeat 100 (seq (run expansion) (saturate typing) (saturate enumerate-modules))))") .unwrap(); // let serialized = egraph.serialize_for_graphviz(true); @@ -292,6 +505,7 @@ fn find_loop() { egraph .parse_and_run_program( + None, r#" ; This file comes from an example permuter design given to us by Intel. diff --git a/tests/integration_tests/lit.cfg b/tests/integration_tests/lit.cfg new file mode 100644 index 0000000..b56427e --- /dev/null +++ b/tests/integration_tests/lit.cfg @@ -0,0 +1,40 @@ +import lit.formats +import os +import shutil +import subprocess + +# Set up path to LLVM -- specifically so that we can use FileCheck. +# 1. If LLVM_CONFIG is set, uses that to find the bin directory of LLVM. +# 2. Else, uses FileCheck on the PATH, if there is one. +# 3. Else, uses llvm-config on the PATH to set the PATH to LLVM binaries. +# 4. Else, fail. +llvm_bindir = "" +if "LLVM_CONFIG" in os.environ: + llvm_bindir = ( + subprocess.check_output( + [os.environ["LLVM_CONFIG"], "--bindir"], + ) + .decode("utf-8") + .strip() + ) +elif shutil.which("FileCheck"): + pass +elif shutil.which("llvm-config"): + llvm_bindir = ( + subprocess.check_output( + ["llvm-config", "--bindir"], + ) + .decode("utf-8") + .strip() + ) +else: + raise Exception("LLVM_CONFIG is not set, and FileCheck and llvm-config are not on the PATH. Please point LLVM_CONFIG to the llvm-config binary, or install LLVM and put its binary directory on your PATH.") + +env = os.environ.copy() +env["PATH"] = llvm_bindir + ":" + env["PATH"] + +config.name = "Churchroad tests" +# True so that we use external shell. +config.test_format = lit.formats.ShTest(True) +config.environment = env +config.suffixes = [".v", ".sv", ".txt"] \ No newline at end of file diff --git a/tests/integration_tests/simple_mul.v b/tests/integration_tests/simple_mul.v new file mode 100644 index 0000000..12ede89 --- /dev/null +++ b/tests/integration_tests/simple_mul.v @@ -0,0 +1,28 @@ +// RUN: cargo run -- \ +// RUN: --filepath %s \ +// RUN: --top-module-name mul \ +// RUN: --architecture xilinx-ultrascale-plus \ +// RUN: --simulate \ +// RUN: --simulate-with-verilator-arg="--verilator_include_dir=$LAKEROAD_DIR/lakeroad-private/DSP48E2" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-DXIL_XECLIB" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-UNOPTFLAT" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-COMBDLY" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-LATCH" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-WIDTH" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-STMTDLY" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-CASEX" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-TIMESCALEMOD" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-PINMISSING" \ +// RUN: | FileCheck %s + +module mul(input [15:0] a, b, output [15:0] out); + assign out = a * b; +endmodule + +// TODO wrong module name +// CHECK: module top( +// CHECK: input [16-1:0] a, +// CHECK: input [16-1:0] b, +// CHECK: output [16-1:0] out, +// CHECK: ); +// CHECK: DSP48E2 #( \ No newline at end of file diff --git a/tests/integration_tests/wide_mul.v b/tests/integration_tests/wide_mul.v new file mode 100644 index 0000000..2af05d9 --- /dev/null +++ b/tests/integration_tests/wide_mul.v @@ -0,0 +1,29 @@ +// RUN: cargo run -- \ +// RUN: --filepath %s \ +// RUN: --top-module-name mul \ +// RUN: --architecture xilinx-ultrascale-plus \ +// RUN: --simulate \ +// RUN: --simulate-with-verilator-arg="--verilator_include_dir=$LAKEROAD_DIR/lakeroad-private/DSP48E2" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-DXIL_XECLIB" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-UNOPTFLAT" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-COMBDLY" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-LATCH" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-WIDTH" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-STMTDLY" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-CASEX" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-TIMESCALEMOD" \ +// RUN: --simulate-with-verilator-arg="--verilator_extra_arg=-Wno-PINMISSING" \ +// RUN: | FileCheck %s + +module mul(input [15:0] a, input [31:0] b, output [31:0] out); + assign out = a * b; +endmodule + +// TODO wrong module name +// CHECK: module top( +// CHECK: input [16-1:0] a, +// CHECK: input [32-1:0] b, +// CHECK: output [32-1:0] out, +// CHECK: ); +// CHECK: DSP48E2 #( +// CHECK: DSP48E2 #( \ No newline at end of file diff --git a/tests/interpreter_tests.rs b/tests/interpreter_tests.rs index 809259f..5a22222 100644 --- a/tests/interpreter_tests.rs +++ b/tests/interpreter_tests.rs @@ -1,13 +1,17 @@ // This file contains tests for the interpreter module. -use std::{fmt::Write, fs, io::Write as IOWrite, path::PathBuf, vec}; +use std::{fmt::Write, fs, io::Write as IOWrite, path::PathBuf, usize, vec}; -use egraph_serialize::NodeId; +use egraph_serialize::{ClassId, NodeId}; +use indexmap::IndexMap; use rand::{rngs::StdRng, RngCore, SeedableRng}; use egglog::{EGraph, SerializeConfig}; -use churchroad::{get_bitwidth_for_node, import_churchroad, interpret, InterpreterResult}; +use churchroad::{ + commands_from_verilog_file, get_bitwidth_for_node, global_greedy_dag::GlobalGreedyDagExtractor, + import_churchroad, interpret, InterpreterResult, +}; // Creates an EGraph from a Verilog file using Churchroad, and returns the serialized EGraph and the root node. fn prep_interpreter( @@ -15,42 +19,20 @@ fn prep_interpreter( test_output_dir: PathBuf, top_module_name: &str, out: &str, -) -> (egraph_serialize::EGraph, egraph_serialize::Node) { +) -> ( + egraph_serialize::EGraph, + IndexMap, + egraph_serialize::Node, +) { if std::env::var("CHURCHROAD_DIR").is_err() { panic!("Please set the CHURCHROAD_DIR environment variable!"); } - let churchroad_dir_str: String = std::env::var("CHURCHROAD_DIR").unwrap(); - - let churchroad_yosys_dir = - std::path::Path::new(&churchroad_dir_str).join("yosys-plugin/churchroad.so"); - let churchroad_src_path = test_output_dir.join(format!("{}.egg", top_module_name)); + let churchroad_commands = + commands_from_verilog_file(&module_verilog_path, top_module_name, true, true, [].into()); - let yosys_commands = format!( - "read_verilog -sv {}; prep -top {}; pmuxtree; write_lakeroad", - module_verilog_path.to_str().unwrap(), - top_module_name, - ); - - let yosys_proc = std::process::Command::new("yosys") - .arg("-m") - .arg(churchroad_yosys_dir) - .arg("-q") - .arg("-p") - .arg(yosys_commands) - .output(); - - let yosys_output = yosys_proc.unwrap(); - - if !yosys_output.status.success() { - panic!( - "Yosys failed, stderr: {:?}", - String::from_utf8(yosys_output.stderr) - ); - } - - std::fs::write(&churchroad_src_path, yosys_output.stdout).unwrap(); + std::fs::write(&churchroad_src_path, churchroad_commands).unwrap(); println!( "logged Churchroad source to: {}", churchroad_src_path.to_str().unwrap() @@ -60,15 +42,22 @@ fn prep_interpreter( let mut egraph: EGraph = EGraph::default(); import_churchroad(&mut egraph); egraph - .parse_and_run_program(&std::fs::read_to_string(churchroad_src_path).unwrap()) + .parse_and_run_program(None, &std::fs::read_to_string(churchroad_src_path).unwrap()) .unwrap(); egraph - .parse_and_run_program("(run-schedule (saturate typing))") + .parse_and_run_program(None, "(run-schedule (saturate typing))") .unwrap(); let serialized = egraph.serialize(SerializeConfig::default()); + let choices = GlobalGreedyDagExtractor { + // We don't care about only extracting legal structural Verilog + // constructs when interpreting. + structural_only: false, + } + .extract(&serialized, &[]); + let (_, is_output_node) = serialized .nodes .iter() @@ -93,7 +82,7 @@ fn prep_interpreter( // Each node should have a HasType node associated with it. for (node_id, node) in serialized.nodes.iter() { // if the node has op in the list, don't care - let list = vec!["Var", "Op1"]; + let list = ["Var", "Op1"]; if !list.contains(&node.op.as_str()) { continue; } @@ -101,13 +90,15 @@ fn prep_interpreter( } let output_id = is_output_node.children.last().unwrap(); - let (_, output_node) = serialized + let output_node = serialized .nodes .iter() .find(|(node_id, _)| **node_id == *output_id) - .unwrap(); + .unwrap() + .1 + .clone(); - (serialized.clone(), output_node.clone()) + (serialized, choices, output_node) } // TODO(@ninehusky): macroify this @@ -146,6 +137,11 @@ fn test_lut6_combinational_verilator() { std::env::temp_dir(), churchroad_dir .join("tests/interpreter_tests/verilog/xilinx_ultrascale_plus/LUT6-modified.v"), + // Here we can use the choices produced by the extractor, as the design + // is acyclic. Furthermore, this test loops forever without using the + // extractor, as the interpreter makes a bad choice for one of the + // eclasses. + true, ); } @@ -179,9 +175,17 @@ fn test_counter_verilator() { include_dirs, std::env::temp_dir(), churchroad_dir.join("tests/interpreter_tests/verilog/toy_examples/counter.sv"), + // Must be false as the counter is cyclic. Here we just have to hope + // that the interpreter makes a sane choice. + false, ); } +/// - use_choices: whether to use the choices produced by our extractor when +/// running the interpreter. The choices determine what node of each eclass +/// should be interpreted. If false, the interpreter will make its own choice. +/// NOTE: you should only set this to true if the design is not cyclic, as the +/// extractor does not currently support cyclic designs. fn verilator_vs_interpreter( num_test_cases: usize, num_clock_cycles: usize, @@ -192,6 +196,7 @@ fn verilator_vs_interpreter( include_dirs: Vec, test_output_dir: PathBuf, verilog_module_path: PathBuf, + use_choices: bool, ) { // create seeded rng let mut rng = StdRng::seed_from_u64(0xb0bacafe); @@ -214,7 +219,7 @@ fn verilator_vs_interpreter( }) .collect(); - let (serialized, root_node) = prep_interpreter( + let (serialized, choices, root_node) = prep_interpreter( verilog_module_path.clone(), test_output_dir.clone(), top_module_name, @@ -241,7 +246,14 @@ fn verilator_vs_interpreter( // return streams, or we should be able to memoize some way. This just // redoes a bunch of work each call. for timestep in 0..num_clock_cycles { - let result = interpret(&serialized, &root_node.eclass, timestep, &env).unwrap(); + let result = interpret( + &serialized, + &root_node.eclass, + timestep, + &env, + if use_choices { Some(&choices) } else { None }, + ) + .unwrap(); interpreter_results.push(result); } } @@ -308,28 +320,24 @@ fn run_verilator( let filename = verilog_module_path.file_name().unwrap().to_str().unwrap(); let test_module_input_list = { - let inputs_expr = format!( - "{}", - inputs - .iter() - .enumerate() - .map(|(i, (name, _))| format!(".{}(inputs[{}])", name, i)) - .collect::>() - .join(", ") - ); - let outputs_expr = format!( - "{}", - outputs - .iter() - .map(|(name, _)| format!(".{}({})", name, name)) - .collect::>() - .join(", ") - ); + let inputs_expr = inputs + .iter() + .enumerate() + .map(|(i, (name, _))| format!(".{}(inputs[{}])", name, i)) + .collect::>() + .join(", ") + .to_string(); + let outputs_expr = outputs + .iter() + .map(|(name, _)| format!(".{}({})", name, name)) + .collect::>() + .join(", ") + .to_string(); let mut final_expr = String::from(""); - if inputs_expr.len() > 0 { + if !inputs_expr.is_empty() { final_expr.push_str(inputs_expr.as_str()); } - if outputs_expr.len() > 0 { + if !outputs_expr.is_empty() { final_expr.push_str(", "); final_expr.push_str(outputs_expr.as_str()); }; @@ -342,15 +350,13 @@ fn run_verilator( // TODO(@ninehusky): this'll eventually need to include parameters as well, right? .replace( "{input_output_declarations}", - format!( - "{}", - outputs - .iter() - .map(|(name, bw)| format!("logic [{}:0] {};\n", bw - 1, name)) - .collect::>() - .join("\n") - ) - .as_str(), + outputs + .iter() + .map(|(name, bw)| format!("logic [{}:0] {};\n", bw - 1, name)) + .collect::>() + .join("\n") + .to_string() + .as_str(), ) .replace("{test_module_name}", top_module_name) .replace("{test_module_port_list}", test_module_input_list.as_str()) @@ -399,7 +405,7 @@ fn run_verilator( let verilator_output_dir = test_output_dir.join("obj_dir"); let executable_path = verilator_output_dir.join(executable_name); - std::fs::write(&testbench_path, &testbench_prog).unwrap(); + std::fs::write(&testbench_path, testbench_prog).unwrap(); // TODO(@ninehusky): We can get rid of the necessity for a Makefile after this PR is merged // into Verilator: https://github.com/verilator/verilator/pull/5031 @@ -478,7 +484,7 @@ fn run_verilator( let verilator_output_values: Vec = output_str .lines() // filter all lines that don't start with "output: " - .filter(|line| line.len() > 0 && line.starts_with("output: ")) + .filter(|line| !line.is_empty() && line.starts_with("output: ")) .map(|line| line.trim_start_matches("output: ").parse().unwrap()) .collect(); @@ -492,7 +498,7 @@ macro_rules! interpreter_test_verilog { $(#[$meta])* #[test] fn $test_name() { - let (serialized, root_node) = prep_interpreter( + let (serialized, _choices, root_node) = prep_interpreter( PathBuf::from($verilog_path), std::env::temp_dir(), $module_name, @@ -501,7 +507,12 @@ macro_rules! interpreter_test_verilog { assert_eq!( $expected, - interpret(&serialized, &root_node.eclass, $time, $env).unwrap() + // Note that we *may* need to start using _choices here, if we + // start hitting infinite loops because of bad choices of enode + // from eclass in the interpreter. However, in that case, we can + // only use choices if the design is acyclic. See the comment in + // the `verilator_vs_interpreter` function for more details. + interpret(&serialized, &root_node.eclass, $time, $env, None).unwrap() ); } }; @@ -514,10 +525,10 @@ macro_rules! interpreter_test_churchroad { let mut egraph: EGraph = EGraph::default(); import_churchroad(&mut egraph); - egraph.parse_and_run_program($churchroad_src).unwrap(); + egraph.parse_and_run_program(None, $churchroad_src).unwrap(); egraph - .parse_and_run_program("(run-schedule (saturate typing))") + .parse_and_run_program(None, "(run-schedule (saturate typing))") .unwrap(); let serialized = egraph.serialize(SerializeConfig::default()); @@ -541,7 +552,7 @@ macro_rules! interpreter_test_churchroad { .unwrap(); let interpreter_result = - interpret(&serialized, &output_node.eclass, $time, $env).unwrap(); + interpret(&serialized, &output_node.eclass, $time, $env, None).unwrap(); assert_eq!( $expected, interpreter_result, "(left: expected, right: interpreter_result)" diff --git a/tests/type_inference_tests.rs b/tests/type_inference_tests.rs index 5bfcd2b..5a246d8 100644 --- a/tests/type_inference_tests.rs +++ b/tests/type_inference_tests.rs @@ -10,9 +10,9 @@ macro_rules! type_inference_test { fn $test_name() { let mut egraph = EGraph::default(); import_churchroad(&mut egraph); - egraph.parse_and_run_program($churchroad_src).unwrap(); + egraph.parse_and_run_program(None, $churchroad_src).unwrap(); egraph - .parse_and_run_program("(run-schedule (saturate typing))") + .parse_and_run_program(None, "(run-schedule (saturate typing))") .unwrap(); // assert that everything has a type diff --git a/yosys-plugin/churchroad.cc b/yosys-plugin/churchroad.cc index 8490d07..805baec 100644 --- a/yosys-plugin/churchroad.cc +++ b/yosys-plugin/churchroad.cc @@ -33,6 +33,10 @@ PRIVATE_NAMESPACE_BEGIN struct LakeroadWorker { + std::string salt; + // Whether or not to generate let bindings for ports. + bool let_bindings; + std::map port_to_expr_map; std::ostream &f; SigMap sigmap; RTLIL::Module *module; @@ -148,1122 +152,7 @@ struct LakeroadWorker return " " + infostr; } - void ywmap_state(const SigSpec &sig) - { - if (ywmap_json.active()) - ywmap_states.emplace_back(sig); - } - - void ywmap_state(Cell *cell) - { - if (ywmap_json.active()) - ywmap_states.emplace_back(cell); - } - - void ywmap_input(const SigSpec &sig) - { - if (ywmap_json.active()) - ywmap_inputs.emplace_back(sig); - } - - void emit_ywmap_btor_sig(const ywmap_btor_sig &btor_sig) - { - if (btor_sig.cell == nullptr) - { - if (btor_sig.sig.empty()) - { - ywmap_json.value(nullptr); - return; - } - ywmap_json.begin_array(); - ywmap_json.compact(); - for (auto &chunk : btor_sig.sig.chunks()) - { - log_assert(chunk.is_wire()); - - ywmap_json.begin_object(); - ywmap_json.entry("path", witness_path(chunk.wire)); - ywmap_json.entry("width", chunk.width); - ywmap_json.entry("offset", chunk.offset); - ywmap_json.end_object(); - } - ywmap_json.end_array(); - } - else - { - ywmap_json.begin_object(); - ywmap_json.compact(); - ywmap_json.entry("path", witness_path(btor_sig.cell)); - Mem *mem = mem_cells[btor_sig.cell]; - ywmap_json.entry("width", mem->width); - ywmap_json.entry("size", mem->size); - ywmap_json.end_object(); - } - } - - void btorf_push(const string &id) - { - if (verbose) - { - f << indent << stringf(" ; begin %s\n", id.c_str()); - indent += " "; - } - } - - void btorf_pop(const string &id) - { - if (verbose) - { - indent = indent.substr(4); - f << indent << stringf(" ; end %s\n", id.c_str()); - } - } - - int get_bv_sid(int width) - { - if (sorts_bv.count(width) == 0) - { - int nid = next_nid++; - btorf("%d sort bitvec %d\n", nid, width); - sorts_bv[width] = nid; - } - return sorts_bv.at(width); - } - - int get_mem_sid(int abits, int dbits) - { - pair key(abits, dbits); - if (sorts_mem.count(key) == 0) - { - int addr_sid = get_bv_sid(abits); - int data_sid = get_bv_sid(dbits); - int nid = next_nid++; - btorf("%d sort array %d %d\n", nid, addr_sid, data_sid); - sorts_mem[key] = nid; - } - return sorts_mem.at(key); - } - - void add_nid_sig(int nid, const SigSpec &sig) - { - if (verbose) - f << indent << stringf("; %d %s\n", nid, log_signal(sig)); - - for (int i = 0; i < GetSize(sig); i++) - bit_nid[sig[i]] = make_pair(nid, i); - - sig_nid[sig] = nid; - nid_width[nid] = GetSize(sig); - } - - void export_cell(Cell *cell) - { - if (cell_recursion_guard.count(cell)) - { - string cell_list; - for (auto c : cell_recursion_guard) - cell_list += stringf("\n %s", log_id(c)); - log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell), cell_list.c_str()); - } - - cell_recursion_guard.insert(cell); - btorf_push(log_id(cell)); - - if (cell->type.in(ID($add), ID($sub), ID($mul), ID($and), ID($or), ID($xor), ID($xnor), ID($shl), ID($sshl), ID($shr), ID($sshr), - ID($shift), ID($shiftx), ID($concat), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_))) - { - string btor_op; - if (cell->type == ID($add)) - btor_op = "add"; - if (cell->type == ID($sub)) - btor_op = "sub"; - if (cell->type == ID($mul)) - btor_op = "mul"; - if (cell->type.in(ID($shl), ID($sshl))) - btor_op = "sll"; - if (cell->type == ID($shr)) - btor_op = "srl"; - if (cell->type == ID($sshr)) - btor_op = "sra"; - if (cell->type.in(ID($shift), ID($shiftx))) - btor_op = "shift"; - if (cell->type.in(ID($and), ID($_AND_))) - btor_op = "and"; - if (cell->type.in(ID($or), ID($_OR_))) - btor_op = "or"; - if (cell->type.in(ID($xor), ID($_XOR_))) - btor_op = "xor"; - if (cell->type == ID($concat)) - btor_op = "concat"; - if (cell->type == ID($_NAND_)) - btor_op = "nand"; - if (cell->type == ID($_NOR_)) - btor_op = "nor"; - if (cell->type.in(ID($xnor), ID($_XNOR_))) - btor_op = "xnor"; - log_assert(!btor_op.empty()); - - int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); - int width = std::max(width_ay, GetSize(cell->getPort(ID::B))); - - bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; - bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; - - if (btor_op == "shift" && !b_signed) - btor_op = "srl"; - - if (cell->type.in(ID($shl), ID($sshl), ID($shr), ID($sshr))) - b_signed = false; - - if (cell->type == ID($sshr) && !a_signed) - btor_op = "srl"; - - int sid = get_bv_sid(width); - int nid; - - int nid_a; - if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) - { - // sign-extend A up to the width of Y - int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed); - - // zero-extend the rest - int zeroes = get_sig_nid(Const(0, width - width_ay)); - nid_a = next_nid++; - btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded); - } - else - { - nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - } - - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - - if (btor_op == "shift") - { - int nid_r = next_nid++; - btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b); - - int nid_b_neg = next_nid++; - btorf("%d neg %d %d\n", nid_b_neg, sid, nid_b); - - int nid_l = next_nid++; - btorf("%d sll %d %d %d\n", nid_l, sid, nid_a, nid_b_neg); - - int sid_bit = get_bv_sid(1); - int nid_zero = get_sig_nid(Const(0, width)); - int nid_b_ltz = next_nid++; - btorf("%d slt %d %d %d\n", nid_b_ltz, sid_bit, nid_b, nid_zero); - - nid = next_nid++; - btorf("%d ite %d %d %d %d%s\n", nid, sid, nid_b_ltz, nid_l, nid_r, getinfo(cell).c_str()); - } - else - { - nid = next_nid++; - btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); - } - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - - if (GetSize(sig) < width) - { - int sid = get_bv_sid(GetSize(sig)); - int nid2 = next_nid++; - btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig) - 1); - nid = nid2; - } - - add_nid_sig(nid, sig); - goto okay; - } - - if (cell->type.in(ID($div), ID($mod), ID($modfloor))) - { - bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; - bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; - - string btor_op; - if (cell->type == ID($div)) - btor_op = "div"; - // "rem" = truncating modulo - if (cell->type == ID($mod)) - btor_op = "rem"; - // "mod" = flooring modulo - if (cell->type == ID($modfloor)) - { - // "umod" doesn't exist because it's the same as "urem" - btor_op = a_signed || b_signed ? "mod" : "rem"; - } - log_assert(!btor_op.empty()); - - int width = GetSize(cell->getPort(ID::Y)); - width = std::max(width, GetSize(cell->getPort(ID::A))); - width = std::max(width, GetSize(cell->getPort(ID::B))); - - int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - - int sid = get_bv_sid(width); - int nid = next_nid++; - btorf("%d %c%s %d %d %d%s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, - getinfo(cell).c_str()); - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - - if (GetSize(sig) < width) - { - int sid = get_bv_sid(GetSize(sig)); - int nid2 = next_nid++; - btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig) - 1); - nid = nid2; - } - - add_nid_sig(nid, sig); - goto okay; - } - - if (cell->type.in(ID($_ANDNOT_), ID($_ORNOT_))) - { - int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort(ID::A)); - int nid_b = get_sig_nid(cell->getPort(ID::B)); - - int nid1 = next_nid++; - int nid2 = next_nid++; - - if (cell->type == ID($_ANDNOT_)) - { - btorf("%d not %d %d\n", nid1, sid, nid_b); - btorf("%d and %d %d %d%s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str()); - } - - if (cell->type == ID($_ORNOT_)) - { - btorf("%d not %d %d\n", nid1, sid, nid_b); - btorf("%d or %d %d %d%s\n", nid2, sid, nid_a, nid1, getinfo(cell).c_str()); - } - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - add_nid_sig(nid2, sig); - goto okay; - } - - if (cell->type.in(ID($_OAI3_), ID($_AOI3_))) - { - int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort(ID::A)); - int nid_b = get_sig_nid(cell->getPort(ID::B)); - int nid_c = get_sig_nid(cell->getPort(ID::C)); - - int nid1 = next_nid++; - int nid2 = next_nid++; - int nid3 = next_nid++; - - if (cell->type == ID($_OAI3_)) - { - btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b); - btorf("%d and %d %d %d\n", nid2, sid, nid1, nid_c); - btorf("%d not %d %d%s\n", nid3, sid, nid2, getinfo(cell).c_str()); - } - - if (cell->type == ID($_AOI3_)) - { - btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b); - btorf("%d or %d %d %d\n", nid2, sid, nid1, nid_c); - btorf("%d not %d %d%s\n", nid3, sid, nid2, getinfo(cell).c_str()); - } - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - add_nid_sig(nid3, sig); - goto okay; - } - - if (cell->type.in(ID($_OAI4_), ID($_AOI4_))) - { - int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort(ID::A)); - int nid_b = get_sig_nid(cell->getPort(ID::B)); - int nid_c = get_sig_nid(cell->getPort(ID::C)); - int nid_d = get_sig_nid(cell->getPort(ID::D)); - - int nid1 = next_nid++; - int nid2 = next_nid++; - int nid3 = next_nid++; - int nid4 = next_nid++; - - if (cell->type == ID($_OAI4_)) - { - btorf("%d or %d %d %d\n", nid1, sid, nid_a, nid_b); - btorf("%d or %d %d %d\n", nid2, sid, nid_c, nid_d); - btorf("%d and %d %d %d\n", nid3, sid, nid1, nid2); - btorf("%d not %d %d%s\n", nid4, sid, nid3, getinfo(cell).c_str()); - } - - if (cell->type == ID($_AOI4_)) - { - btorf("%d and %d %d %d\n", nid1, sid, nid_a, nid_b); - btorf("%d and %d %d %d\n", nid2, sid, nid_c, nid_d); - btorf("%d or %d %d %d\n", nid3, sid, nid1, nid2); - btorf("%d not %d %d%s\n", nid4, sid, nid3, getinfo(cell).c_str()); - } - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - add_nid_sig(nid4, sig); - goto okay; - } - - if (cell->type.in(ID($lt), ID($le), ID($eq), ID($eqx), ID($ne), ID($nex), ID($ge), ID($gt))) - { - string btor_op; - if (cell->type == ID($lt)) - btor_op = "lt"; - if (cell->type == ID($le)) - btor_op = "lte"; - if (cell->type.in(ID($eq), ID($eqx))) - btor_op = "eq"; - if (cell->type.in(ID($ne), ID($nex))) - btor_op = "neq"; - if (cell->type == ID($ge)) - btor_op = "gte"; - if (cell->type == ID($gt)) - btor_op = "gt"; - log_assert(!btor_op.empty()); - - int width = 1; - width = std::max(width, GetSize(cell->getPort(ID::A))); - width = std::max(width, GetSize(cell->getPort(ID::B))); - - bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; - bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; - - int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - - int nid = next_nid++; - if (cell->type.in(ID($lt), ID($le), ID($ge), ID($gt))) - { - btorf("%d %c%s %d %d %d%s\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b, - getinfo(cell).c_str()); - } - else - { - btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); - } - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - - if (GetSize(sig) > 1) - { - int sid = get_bv_sid(GetSize(sig)); - int nid2 = next_nid++; - btorf("%d uext %d %d %d\n", nid2, sid, nid, GetSize(sig) - 1); - nid = nid2; - } - - add_nid_sig(nid, sig); - goto okay; - } - - if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos))) - { - string btor_op; - if (cell->type.in(ID($not), ID($_NOT_))) - btor_op = "not"; - if (cell->type == ID($neg)) - btor_op = "neg"; - - int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); - - bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; - int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - SigSpec sig = sigmap(cell->getPort(ID::Y)); - - // the $pos cell just passes through, all other cells need an actual operation applied - int nid = nid_a; - if (cell->type != ID($pos)) - { - log_assert(!btor_op.empty()); - int sid = get_bv_sid(width); - nid = next_nid++; - btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); - } - - if (GetSize(sig) < width) - { - int sid = get_bv_sid(GetSize(sig)); - int nid2 = next_nid++; - btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig) - 1); - nid = nid2; - } - - add_nid_sig(nid, sig); - goto okay; - } - - if (cell->type.in(ID($logic_and), ID($logic_or), ID($logic_not))) - { - string btor_op; - if (cell->type == ID($logic_and)) - btor_op = "and"; - if (cell->type == ID($logic_or)) - btor_op = "or"; - if (cell->type == ID($logic_not)) - btor_op = "not"; - log_assert(!btor_op.empty()); - - int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort(ID::A)); - int nid_b = btor_op != "not" ? get_sig_nid(cell->getPort(ID::B)) : 0; - - if (GetSize(cell->getPort(ID::A)) > 1) - { - int nid_red_a = next_nid++; - btorf("%d redor %d %d\n", nid_red_a, sid, nid_a); - nid_a = nid_red_a; - } - - if (btor_op != "not" && GetSize(cell->getPort(ID::B)) > 1) - { - int nid_red_b = next_nid++; - btorf("%d redor %d %d\n", nid_red_b, sid, nid_b); - nid_b = nid_red_b; - } - - int nid = next_nid++; - if (btor_op != "not") - btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); - else - btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - - if (GetSize(sig) > 1) - { - int sid = get_bv_sid(GetSize(sig)); - int zeros_nid = get_sig_nid(Const(0, GetSize(sig) - 1)); - int nid2 = next_nid++; - btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid); - nid = nid2; - } - - add_nid_sig(nid, sig); - goto okay; - } - - if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool), ID($reduce_xor), ID($reduce_xnor))) - { - string btor_op; - if (cell->type == ID($reduce_and)) - btor_op = "redand"; - if (cell->type.in(ID($reduce_or), ID($reduce_bool))) - btor_op = "redor"; - if (cell->type.in(ID($reduce_xor), ID($reduce_xnor))) - btor_op = "redxor"; - log_assert(!btor_op.empty()); - - int sid = get_bv_sid(1); - int nid_a = get_sig_nid(cell->getPort(ID::A)); - - int nid = next_nid++; - - if (cell->type == ID($reduce_xnor)) - { - int nid2 = next_nid++; - btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); - btorf("%d not %d %d\n", nid2, sid, nid); - nid = nid2; - } - else - { - btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str()); - } - - SigSpec sig = sigmap(cell->getPort(ID::Y)); - - if (GetSize(sig) > 1) - { - int sid = get_bv_sid(GetSize(sig)); - int zeros_nid = get_sig_nid(Const(0, GetSize(sig) - 1)); - int nid2 = next_nid++; - btorf("%d concat %d %d %d\n", nid2, sid, zeros_nid, nid); - nid = nid2; - } - - add_nid_sig(nid, sig); - goto okay; - } - - if (cell->type.in(ID($mux), ID($_MUX_), ID($_NMUX_))) - { - SigSpec sig_a = sigmap(cell->getPort(ID::A)); - SigSpec sig_b = sigmap(cell->getPort(ID::B)); - SigSpec sig_s = sigmap(cell->getPort(ID::S)); - SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - - int nid_a = get_sig_nid(sig_a); - int nid_b = get_sig_nid(sig_b); - int nid_s = get_sig_nid(sig_s); - - int sid = get_bv_sid(GetSize(sig_y)); - int nid = next_nid++; - - if (cell->type == ID($_NMUX_)) - { - int tmp = nid; - nid = next_nid++; - btorf("%d ite %d %d %d %d\n", tmp, sid, nid_s, nid_b, nid_a); - btorf("%d not %d %d%s\n", nid, sid, tmp, getinfo(cell).c_str()); - } - else - { - btorf("%d ite %d %d %d %d%s\n", nid, sid, nid_s, nid_b, nid_a, getinfo(cell).c_str()); - } - - add_nid_sig(nid, sig_y); - goto okay; - } - - if (cell->type == ID($pmux)) - { - SigSpec sig_a = sigmap(cell->getPort(ID::A)); - SigSpec sig_b = sigmap(cell->getPort(ID::B)); - SigSpec sig_s = sigmap(cell->getPort(ID::S)); - SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - - int width = GetSize(sig_a); - int sid = get_bv_sid(width); - int nid = get_sig_nid(sig_a); - - for (int i = 0; i < GetSize(sig_s); i++) - { - int nid_b = get_sig_nid(sig_b.extract(i * width, width)); - int nid_s = get_sig_nid(sig_s.extract(i)); - int nid2 = next_nid++; - if (i == GetSize(sig_s) - 1) - btorf("%d ite %d %d %d %d%s\n", nid2, sid, nid_s, nid_b, nid, getinfo(cell).c_str()); - else - btorf("%d ite %d %d %d %d\n", nid2, sid, nid_s, nid_b, nid); - nid = nid2; - } - - add_nid_sig(nid, sig_y); - goto okay; - } - - if (cell->type.in(ID($dff), ID($ff), ID($anyinit), ID($_DFF_P_), ID($_DFF_N), ID($_FF_))) - { - SigSpec sig_d = sigmap(cell->getPort(ID::D)); - SigSpec sig_q = sigmap(cell->getPort(ID::Q)); - - if ((!info_filename.empty() || ywmap_json.active()) && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_))) - { - SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C)); - int nid = get_sig_nid(sig_c); - bool negedge = false; - - if (cell->type == ID($_DFF_N_)) - negedge = true; - - if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool()) - negedge = true; - - if (!info_filename.empty()) - info_clocks[nid] |= negedge ? 2 : 1; - - if (ywmap_json.active()) - ywmap_clock_bits[sig_c] |= negedge ? 2 : 1; - } - - IdString symbol; - - if (sig_q.is_wire()) - { - Wire *w = sig_q.as_wire(); - if (w->port_id == 0) - { - statewires.insert(w); - symbol = w->name; - } - } - - Const initval; - for (int i = 0; i < GetSize(sig_q); i++) - if (initbits.count(sig_q[i])) - initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0); - else - initval.bits.push_back(State::Sx); - - int nid_init_val = -1; - - if (!initval.is_fully_undef()) - nid_init_val = get_sig_nid(initval, -1, false, true); - - int sid = get_bv_sid(GetSize(sig_q)); - int nid = next_nid++; - - if (symbol.empty() || (!print_internal_names && symbol[0] == '$')) - btorf("%d state %d\n", nid, sid); - else - btorf("%d state %d %s\n", nid, sid, log_id(symbol)); - - if (cell->get_bool_attribute(ID(clk2fflogic))) - ywmap_state(cell->getPort(ID::D)); // For a clk2fflogic FF the named signal is the D input not the Q output - else - ywmap_state(sig_q); - - if (nid_init_val >= 0) - { - int nid_init = next_nid++; - if (verbose) - btorf("; initval = %s\n", log_signal(initval)); - btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val); - } - - ff_todo.push_back(make_pair(nid, cell)); - add_nid_sig(nid, sig_q); - goto okay; - } - - if (cell->type.in(ID($anyconst), ID($anyseq))) - { - SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - - int sid = get_bv_sid(GetSize(sig_y)); - int nid = next_nid++; - - btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str()); - - ywmap_state(sig_y); - - if (cell->type == ID($anyconst)) - { - int nid2 = next_nid++; - btorf("%d next %d %d %d\n", nid2, sid, nid, nid); - } - - add_nid_sig(nid, sig_y); - goto okay; - } - - if (cell->type == ID($initstate)) - { - SigSpec sig_y = sigmap(cell->getPort(ID::Y)); - - if (initstate_nid < 0) - { - int sid = get_bv_sid(1); - int one_nid = get_sig_nid(State::S1); - int zero_nid = get_sig_nid(State::S0); - initstate_nid = next_nid++; - btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str()); - btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid); - btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid); - - ywmap_state(sig_y); - } - - add_nid_sig(initstate_nid, sig_y); - goto okay; - } - - if (cell->is_mem_cell()) - { - Mem *mem = mem_cells[cell]; - - int abits = ceil_log2(mem->size); - - bool asyncwr = false; - bool syncwr = false; - - for (auto &port : mem->wr_ports) - { - if (port.clk_enable) - syncwr = true; - else - asyncwr = true; - } - - if (asyncwr && syncwr) - log_error("Memory %s.%s has mixed async/sync write ports.\n", log_id(module), log_id(mem->memid)); - - for (auto &port : mem->rd_ports) - { - if (port.clk_enable) - log_error("Memory %s.%s has sync read ports. Please use memory_nordff to convert them first.\n", - log_id(module), log_id(mem->memid)); - } - - int data_sid = get_bv_sid(mem->width); - int bool_sid = get_bv_sid(1); - int sid = get_mem_sid(abits, mem->width); - - int nid_init_val = -1; - - if (!mem->inits.empty()) - { - Const initdata = mem->get_init_data(); - bool constword = true; - Const firstword = initdata.extract(0, mem->width); - - for (int i = 1; i < mem->size; i++) - { - Const thisword = initdata.extract(i * mem->width, mem->width); - if (thisword != firstword) - { - constword = false; - break; - } - } - - if (constword) - { - if (verbose) - btorf("; initval = %s\n", log_signal(firstword)); - nid_init_val = get_sig_nid(firstword, -1, false, true); - } - else - { - nid_init_val = next_nid++; - btorf("%d state %d\n", nid_init_val, sid); - - ywmap_state(nullptr); - - for (int i = 0; i < mem->size; i++) - { - Const thisword = initdata.extract(i * mem->width, mem->width); - if (thisword.is_fully_undef()) - continue; - Const thisaddr(i, abits); - int nid_thisword = get_sig_nid(thisword, -1, false, true); - int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true); - int last_nid_init_val = nid_init_val; - nid_init_val = next_nid++; - if (verbose) - btorf("; initval[%d] = %s\n", i, log_signal(thisword)); - btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword); - } - } - } - - int nid = next_nid++; - int nid_head = nid; - - if (mem->memid[0] == '$') - btorf("%d state %d\n", nid, sid); - else - btorf("%d state %d %s\n", nid, sid, log_id(mem->memid)); - - ywmap_state(cell); - - if (nid_init_val >= 0) - { - int nid_init = next_nid++; - btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val); - } - - if (asyncwr) - { - for (auto &port : mem->wr_ports) - { - SigSpec wa = port.addr; - wa.extend_u0(abits); - - int wa_nid = get_sig_nid(wa); - int wd_nid = get_sig_nid(port.data); - int we_nid = get_sig_nid(port.en); - - int nid2 = next_nid++; - btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); - - int nid3 = next_nid++; - btorf("%d not %d %d\n", nid3, data_sid, we_nid); - - int nid4 = next_nid++; - btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); - - int nid5 = next_nid++; - btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); - - int nid6 = next_nid++; - btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); - - int nid7 = next_nid++; - btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); - - int nid8 = next_nid++; - btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); - - int nid9 = next_nid++; - btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); - - nid_head = nid9; - } - } - - for (auto &port : mem->rd_ports) - { - SigSpec ra = port.addr; - ra.extend_u0(abits); - - int ra_nid = get_sig_nid(ra); - int rd_nid = next_nid++; - - btorf("%d read %d %d %d\n", rd_nid, data_sid, nid_head, ra_nid); - - add_nid_sig(rd_nid, port.data); - } - - if (!asyncwr) - { - mem_todo.push_back(make_pair(nid, mem)); - } - else - { - int nid2 = next_nid++; - btorf("%d next %d %d %d\n", nid2, sid, nid, nid_head); - } - - goto okay; - } - - if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || - (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) - { - log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_btor`.\n", log_id(cell->type), - log_id(module), log_id(cell)); - } - if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || - cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") - { - log_error( - "Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_btor`.\n", - log_id(cell->type), log_id(module), log_id(cell)); - } - if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || - cell->type.str().substr(0, 5) == "$_SR_") - { - log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_btor`.\n", log_id(cell->type), - log_id(module), log_id(cell)); - } - log_error("Unsupported cell type %s for cell %s.%s.\n", log_id(cell->type), log_id(module), log_id(cell)); - - okay: - btorf_pop(log_id(cell)); - cell_recursion_guard.erase(cell); - } - - int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false) - { - int nid = -1; - sigmap.apply(sig); - - for (auto bit : sig) - if (bit == State::Sx) - goto has_undef_bits; - - if (0) - { - has_undef_bits: - SigSpec sig_mask_undef, sig_noundef; - int first_undef = -1; - - for (int i = 0; i < GetSize(sig); i++) - if (sig[i] == State::Sx) - { - if (first_undef < 0) - first_undef = i; - sig_mask_undef.append(State::S1); - sig_noundef.append(State::S0); - } - else - { - sig_mask_undef.append(State::S0); - sig_noundef.append(sig[i]); - } - - if (to_width < 0 || first_undef < to_width) - { - int sid = get_bv_sid(GetSize(sig)); - - int nid_input = next_nid++; - if (is_init) - { - btorf("%d state %d\n", nid_input, sid); - ywmap_state(sig); - } - else - { - btorf("%d input %d\n", nid_input, sid); - ywmap_input(sig); - } - - int nid_masked_input; - if (sig_mask_undef.is_fully_ones()) - { - nid_masked_input = nid_input; - } - else - { - int nid_mask_undef = get_sig_nid(sig_mask_undef); - nid_masked_input = next_nid++; - btorf("%d and %d %d %d\n", nid_masked_input, sid, nid_input, nid_mask_undef); - } - - if (sig_noundef.is_fully_zero()) - { - nid = nid_masked_input; - } - else - { - int nid_noundef = get_sig_nid(sig_noundef); - nid = next_nid++; - btorf("%d or %d %d %d\n", nid, sid, nid_masked_input, nid_noundef); - } - - goto extend_or_trim; - } - - sig = sig_noundef; - } - - if (sig_nid.count(sig) == 0) - { - // , - vector> nidbits; - - // collect all bits - for (int i = 0; i < GetSize(sig); i++) - { - SigBit bit = sig[i]; - - if (bit_nid.count(bit) == 0) - { - if (bit.wire == nullptr) - { - Const c(bit.data); - - while (i + GetSize(c) < GetSize(sig) && sig[i + GetSize(c)].wire == nullptr) - c.bits.push_back(sig[i + GetSize(c)].data); - - if (consts.count(c) == 0) - { - int sid = get_bv_sid(GetSize(c)); - int nid = next_nid++; - btorf("%d const %d %s\n", nid, sid, c.as_string().c_str()); - consts[c] = nid; - nid_width[nid] = GetSize(c); - } - - int nid = consts.at(c); - - for (int j = 0; j < GetSize(c); j++) - nidbits.push_back(make_pair(nid, j)); - - i += GetSize(c) - 1; - continue; - } - else - { - if (bit_cell.count(bit) == 0) - { - SigSpec s = bit; - - while (i + GetSize(s) < GetSize(sig) && sig[i + GetSize(s)].wire != nullptr && - bit_cell.count(sig[i + GetSize(s)]) == 0) - s.append(sig[i + GetSize(s)]); - - log_warning("No driver for signal %s.\n", log_signal(s)); - - int sid = get_bv_sid(GetSize(s)); - int nid = next_nid++; - btorf("%d input %d\n", nid, sid); - ywmap_input(s); - nid_width[nid] = GetSize(s); - - for (int j = 0; j < GetSize(s); j++) - nidbits.push_back(make_pair(nid, j)); - - i += GetSize(s) - 1; - continue; - } - else - { - export_cell(bit_cell.at(bit)); - log_assert(bit_nid.count(bit)); - } - } - } - - nidbits.push_back(bit_nid.at(bit)); - } - - int width = 0; - int nid = -1; - - // group bits and emit slice-concat chain - for (int i = 0; i < GetSize(nidbits); i++) - { - int nid2 = nidbits[i].first; - int lower = nidbits[i].second; - int upper = lower; - - while (i + 1 < GetSize(nidbits) && nidbits[i + 1].first == nidbits[i].first && - nidbits[i + 1].second == nidbits[i].second + 1) - upper++, i++; - - int nid3 = nid2; - - if (lower != 0 || upper + 1 != nid_width.at(nid2)) - { - int sid = get_bv_sid(upper - lower + 1); - nid3 = next_nid++; - btorf("%d slice %d %d %d %d\n", nid3, sid, nid2, upper, lower); - } - - int nid4 = nid3; - - if (nid >= 0) - { - int sid = get_bv_sid(width + upper - lower + 1); - nid4 = next_nid++; - btorf("%d concat %d %d %d\n", nid4, sid, nid3, nid); - } - - width += upper - lower + 1; - nid = nid4; - } - - sig_nid[sig] = nid; - nid_width[nid] = width; - } - - nid = sig_nid.at(sig); - - extend_or_trim: - if (to_width >= 0 && to_width != GetSize(sig)) - { - if (to_width < GetSize(sig)) - { - int sid = get_bv_sid(to_width); - int nid2 = next_nid++; - btorf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width - 1); - nid = nid2; - } - else - { - int sid = get_bv_sid(to_width); - int nid2 = next_nid++; - btorf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext", sid, nid, to_width - GetSize(sig)); - nid = nid2; - } - } - - return nid; - } - - LakeroadWorker(std::ostream &f, RTLIL::Module *module) : f(f), sigmap(module), module(module) {} + LakeroadWorker(std::ostream &f, RTLIL::Module *module, std::string &salt, bool let_bindings, std::map port_to_expr_map) : salt(salt), let_bindings(let_bindings), port_to_expr_map(port_to_expr_map), f(f), sigmap(module), module(module) {} void run() { @@ -1273,7 +162,7 @@ struct LakeroadWorker // IDs used to generate let expressions. int id = 0; auto get_new_id_str = [&]() - { return stringf("v%d", id++); }; + { return stringf("v%d%s%s", id++, salt.empty() ? "" : "-", salt.c_str()); }; // Get signal name. auto get_signal_name = [&](const SigSpec &sig) @@ -1542,7 +431,8 @@ struct LakeroadWorker // This is an assumption we're currently making. Doesn't have to be the // case. We may also need to extend the result in the future, when this // assertion fails. - if (cell->getPort(ID::Y).size() < max_width) { + if (cell->getPort(ID::Y).size() < max_width) + { op_str = stringf("(Op1 (Extract %d %d) %s)", cell->getPort(ID::Y).size() - 1, 0, op_str.c_str()); } @@ -1638,7 +528,7 @@ struct LakeroadWorker else if (cell->type == ID($pmux)) { // Don't support $pmux: require them to run pmuxtree instead. - log_error("Unsupported cell type %s for cell %s.%s -- please run `pmuxtree` before `write_lakeroad`.\n", + log_error("Unsupported cell type %s for cell %s.%s -- please run `pmuxtree` before `write_churchroad`.\n", log_id(cell->type), log_id(module), log_id(cell)); } else if (cell->has_attribute("\\src")) @@ -1650,6 +540,7 @@ struct LakeroadWorker std::vector> input_port_names_and_exprs; std::vector> output_port_names_and_exprs; + std::vector> input_parameter_names_and_exprs; for (auto connection : cell->connections()) { @@ -1670,30 +561,70 @@ struct LakeroadWorker } } + auto compile_const = [](RTLIL::Const c) + { + if ((c.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) == RTLIL::ConstFlags::CONST_FLAG_STRING) + { + return stringf("(Op0 (CRString \"%s\"))", c.decode_string().c_str()); + } + else + { + return stringf("(Op0 (BV %d %zu))", c.as_int(false), c.bits.size()); + } + }; + for (auto parameter : cell->parameters) + { + + input_parameter_names_and_exprs.push_back({parameter.first.c_str(), + compile_const(parameter.second)}); + } + // Generate the instance. // Cut the "\" off the front. // Check that it starts with "\" first, though. assert(cell->type[0] == '\\'); assert(cell->name[0] == '\\'); - f << stringf("(let %s (ModuleInstance \"%s\" (vec-of", cell->name.substr(1).c_str(), cell->type.substr(1).c_str()).c_str(); + // Create name with salt. + auto let_bound_name = stringf("%s-%s", cell->name.substr(1).c_str(), salt.c_str()); + f << stringf("(let %s (ModuleInstance \"%s\" ", let_bound_name.c_str(), cell->type.substr(1).c_str()).c_str(); + std::string closer = "(StringNil)"; + for (auto [parameter_name, _] : input_parameter_names_and_exprs) + { + assert(parameter_name[0] == '\\'); + f << stringf("(StringCons \"%s\"", parameter_name.substr(1).c_str()).c_str(); + closer.append(")"); + } + f << closer; + closer = "(ExprNil)"; + for (auto [_, expr] : input_parameter_names_and_exprs) + { + f << stringf("(ExprCons %s", expr.c_str()).c_str(); + closer.append(")"); + } + f << closer; + closer = "(StringNil)"; for (auto [port_name, _] : input_port_names_and_exprs) { assert(port_name[0] == '\\'); - f << stringf(" \"%s\"", port_name.substr(1).c_str()).c_str(); + f << stringf("(StringCons \"%s\"", port_name.substr(1).c_str()).c_str(); + closer.append(")"); } - f << ") (vec-of"; + f << closer; + closer = "(ExprNil)"; for (auto [_, expr] : input_port_names_and_exprs) { - f << stringf(" %s", expr.c_str()).c_str(); + f << stringf("(ExprCons %s", expr.c_str()).c_str(); + closer.append(")"); } - f << ")))\n"; + f << closer; + f << "))\n"; // Hook up the outputs. for (auto [port_name, expr] : output_port_names_and_exprs) { assert(port_name[0] == '\\'); assert(cell->name[0] == '\\'); - f << stringf("(union (GetOutput %s \"%s\") %s)\n", cell->name.substr(1).c_str(), port_name.substr(1).c_str(), expr.c_str()).c_str(); + f << stringf("(union (GetOutput %s \"%s\") %s)\n", let_bound_name.c_str(), port_name.substr(1).c_str(), expr.c_str()).c_str(); } } else @@ -1716,9 +647,17 @@ struct LakeroadWorker assert(signal_let_bound_name.count(sigspec)); auto let_bound_id = signal_let_bound_name.at(sigspec); - f << stringf("(let %s (Var \"%s\" %d))\n", signal_name.c_str(), signal_name.c_str(), GetSize(sigspec)).c_str(); - f << stringf("(IsPort \"%s\" \"%s\" (Input) %s)\n", /*module name*/ "", signal_name.c_str(), signal_name.c_str()).c_str(); - f << stringf("(union %s %s)\n", let_bound_id.c_str(), signal_name.c_str()).c_str(); + f << stringf("(IsPort \"%s\" \"%s\" (Input) %s)\n", /*module name*/ "", signal_name.c_str(), let_bound_id.c_str()).c_str(); + if (let_bindings) + { + f << stringf("(let %s (Var \"%s\" %d))\n", signal_name.c_str(), signal_name.c_str(), GetSize(sigspec)).c_str(); + f << stringf("(union %s %s)\n", let_bound_id.c_str(), signal_name.c_str()).c_str(); + } + // If port name is in port_to_expr_map, union it with the expression. + if (port_to_expr_map.count(signal_name)) + { + f << stringf("(union %s %s)\n", let_bound_id.c_str(), port_to_expr_map.at(signal_name).c_str()).c_str(); + } } // For each output, mark it as an output port using the IsPort relation. @@ -1737,289 +676,45 @@ struct LakeroadWorker assert(signal_let_bound_name.count(sigspec)); auto let_bound_id = signal_let_bound_name.at(sigspec); - f << stringf("(let %s %s)\n", signal_name_pre_sigmap.c_str(), let_bound_id.c_str()).c_str(); - f << stringf("(IsPort \"%s\" \"%s\" (Output) %s)\n", /*module name*/ "", signal_name_pre_sigmap.c_str(), signal_name_pre_sigmap.c_str()).c_str(); + f << stringf("(IsPort \"%s\" \"%s\" (Output) %s)\n", /*module name*/ "", signal_name_pre_sigmap.c_str(), let_bound_id.c_str()).c_str(); + if (let_bindings) + { + f << stringf("(let %s %s)\n", signal_name_pre_sigmap.c_str(), let_bound_id.c_str()).c_str(); + } + // If port name is in port_to_expr_map, union it with the expression. + if (port_to_expr_map.count(signal_name_pre_sigmap)) + { + f << stringf("(union %s %s)\n", let_bound_id.c_str(), port_to_expr_map.at(signal_name_pre_sigmap).c_str()).c_str(); + } } - // Run typing rules before deleting wires -- cyclic circuits can only be typed using Wire expresions to bootstrap the types. - f << "\n; run typing rules\n"; - f << "(run-schedule (saturate typing))\n"; + // Run typing rules before deleting wires -- cyclic circuits can only be typed using Wire expresions to bootstrap the types. + f << "\n; run typing and misc rules\n"; + f << "(run-schedule (saturate (seq typing misc)))\n"; // Delete Wire expressions. f << "\n; delete wire expressions\n"; - for (auto wire_expr : wire_exprs) - { - f << stringf("(delete %s)\n", wire_expr.c_str()).c_str(); - } - - return; - for (auto wire : module->wires()) - { - // Some kind of initialization thing? - // if (wire->attributes.count(ID::init)) { - // Const attrval = wire->attributes.at(ID::init); - // for (int i = 0; i < GetSize(wire) && i < GetSize(attrval); i++) - // if (attrval[i] == State::S0 || attrval[i] == State::S1) - // initbits[sigmap(SigBit(wire, i))] = (attrval[i] == State::S1); - // } - - // Skip if not an input? - if (!wire->port_id || !wire->port_input) - continue; - - SigSpec sig = sigmap(wire); - auto signal_name = std::string(log_signal(sig)); - assert(signal_name.size() > 1); - signal_name = signal_name.substr(1); - auto id_str = "v0"; - btorf("(let %s (Var %s %d))\n", id_str, signal_name.c_str(), GetSize(sig)); - - // if (!info_filename.empty()) { - // auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk); - // if (gclk_attr != wire->attributes.end()) { - // if (gclk_attr->second == State::S1) - // info_clocks[nid] |= 1; - // else if (gclk_attr->second == State::S0) - // info_clocks[nid] |= 2; - // } - // } - - // if (ywmap_json.active()) { - // for (int i = 0; i < GetSize(sig); i++) { - // auto input_bit = SigBit(wire, i); - // auto bit = sigmap(input_bit); - // if (!ywmap_clock_bits.count(bit)) - // continue; - // ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit]; - // } - // } - } - - // btorf_pop("inputs"); - - // for (auto cell : module->cells()) - // for (auto &conn : cell->connections()) { - // if (!cell->output(conn.first)) - // continue; - - // for (auto bit : sigmap(conn.second)) - // bit_cell[bit] = cell; - // } - - // for (auto wire : module->wires()) { - // if (!wire->port_id || !wire->port_output) - // continue; - - // btorf_push(stringf("output %s", log_id(wire))); - - // int nid = get_sig_nid(wire); - // btorf("%d output %d%s\n", next_nid++, nid, getinfo(wire).c_str()); - - // btorf_pop(stringf("output %s", log_id(wire))); - // } - - // for (auto wire : module->wires()) { - // if (wire->port_id || wire->name[0] == '$') - // continue; - - // btorf_push(stringf("wire %s", log_id(wire))); - - // int sid = get_bv_sid(GetSize(wire)); - // int nid = get_sig_nid(sigmap(wire)); - - // if (statewires.count(wire)) - // continue; - - // int this_nid = next_nid++; - // btorf("%d uext %d %d %d%s\n", this_nid, sid, nid, 0, getinfo(wire).c_str()); - // if (info_clocks.count(nid)) - // info_clocks[this_nid] |= info_clocks[nid]; - - // btorf_pop(stringf("wire %s", log_id(wire))); - // continue; - // } - - // while (!ff_todo.empty() || !mem_todo.empty()) { - // vector> todo; - // todo.swap(ff_todo); - - // for (auto &it : todo) { - // int nid = it.first; - // Cell *cell = it.second; - - // btorf_push(stringf("next %s", log_id(cell))); - - // SigSpec sig = sigmap(cell->getPort(ID::D)); - // int nid_q = get_sig_nid(sig); - // int sid = get_bv_sid(GetSize(sig)); - // btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str()); - - // btorf_pop(stringf("next %s", log_id(cell))); - // } - - // vector> mtodo; - // mtodo.swap(mem_todo); - - // for (auto &it : mtodo) { - // int nid = it.first; - // Mem *mem = it.second; - - // btorf_push(stringf("next %s", log_id(mem->memid))); - - // int abits = ceil_log2(mem->size); - - // int data_sid = get_bv_sid(mem->width); - // int bool_sid = get_bv_sid(1); - // int sid = get_mem_sid(abits, mem->width); - // int nid_head = nid; - - // for (auto &port : mem->wr_ports) { - // SigSpec wa = port.addr; - // wa.extend_u0(abits); - - // int wa_nid = get_sig_nid(wa); - // int wd_nid = get_sig_nid(port.data); - // int we_nid = get_sig_nid(port.en); - - // int nid2 = next_nid++; - // btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); - - // int nid3 = next_nid++; - // btorf("%d not %d %d\n", nid3, data_sid, we_nid); - - // int nid4 = next_nid++; - // btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); - - // int nid5 = next_nid++; - // btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); - - // int nid6 = next_nid++; - // btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); - - // int nid7 = next_nid++; - // btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); - - // int nid8 = next_nid++; - // btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); - - // int nid9 = next_nid++; - // btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); - - // nid_head = nid9; - // } - - // int nid2 = next_nid++; - // btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, (mem->cell ? getinfo(mem->cell) : - // getinfo(mem->mem)).c_str()); - - // btorf_pop(stringf("next %s", log_id(mem->memid))); - // } - // } - - // while (!bad_properties.empty()) { - // vector todo; - // bad_properties.swap(todo); - - // int sid = get_bv_sid(1); - // int cursor = 0; - - // while (cursor + 1 < GetSize(todo)) { - // int nid_a = todo[cursor++]; - // int nid_b = todo[cursor++]; - // int nid = next_nid++; - - // bad_properties.push_back(nid); - // btorf("%d or %d %d %d\n", nid, sid, nid_a, nid_b); - // } - - // if (!bad_properties.empty()) { - // if (cursor < GetSize(todo)) - // bad_properties.push_back(todo[cursor++]); - // log_assert(cursor == GetSize(todo)); - // } else { - // int nid = next_nid++; - // log_assert(cursor == 0); - // log_assert(GetSize(todo) == 1); - // btorf("%d bad %d\n", nid, todo[cursor]); - // } - // } - - // if (!info_filename.empty()) { - // for (auto &it : info_clocks) { - // switch (it.second) { - // case 1: - // infof("posedge %d\n", it.first); - // break; - // case 2: - // infof("negedge %d\n", it.first); - // break; - // case 3: - // infof("event %d\n", it.first); - // break; - // default: - // log_abort(); - // } - // } - - // std::ofstream f; - // f.open(info_filename.c_str(), std::ofstream::trunc); - // if (f.fail()) - // log_error("Can't open file `%s' for writing: %s\n", info_filename.c_str(), strerror(errno)); - // for (auto &it : info_lines) - // f << it; - // f.close(); - // } - - // if (ywmap_json.active()) { - // ywmap_json.begin_object(); - // ywmap_json.entry("version", "Yosys Witness BTOR map"); - // ywmap_json.entry("generator", yosys_version_str); - - // ywmap_json.name("clocks"); - // ywmap_json.begin_array(); - // for (auto &entry : ywmap_clock_inputs) { - // if (entry.second != 1 && entry.second != 2) - // continue; - // log_assert(entry.first.is_wire()); - // ywmap_json.begin_object(); - // ywmap_json.compact(); - // ywmap_json.entry("path", witness_path(entry.first.wire)); - // ywmap_json.entry("offset", entry.first.offset); - // ywmap_json.entry("edge", entry.second == 1 ? "posedge" : "negedge"); - // ywmap_json.end_object(); - // } - // ywmap_json.end_array(); - - // ywmap_json.name("inputs"); - // ywmap_json.begin_array(); - // for (auto &entry : ywmap_inputs) - // emit_ywmap_btor_sig(entry); - // ywmap_json.end_array(); - - // ywmap_json.name("states"); - // ywmap_json.begin_array(); - // for (auto &entry : ywmap_states) - // emit_ywmap_btor_sig(entry); - // ywmap_json.end_array(); - - // ywmap_json.end_object(); + f << "\n; TODO(@gussmith23): I'm not actually sure we want to delete wires. Sometimes there's nothing attached to a wire, e.g. when it's used to store the unused output of a module. We don't want to delete it in that case!\n"; + // for (auto wire_expr : wire_exprs) + // { + // f << stringf("(delete %s)\n", wire_expr.c_str()).c_str(); // } } }; -struct BtorBackend : public Backend +struct ChurchroadBackend : public Backend { - BtorBackend() : Backend("lakeroad", "write design to egglog Lakeroad IR") {} + ChurchroadBackend() : Backend("churchroad", "write design to egglog Churchroad IR") {} void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - // log("\n"); - // log(" write_btor [options] [filename]\n"); - // log("\n"); - // log("Write a BTOR description of the current design.\n"); - // log("\n"); - // log(" -v\n"); - // log(" Add comments and indentation to BTOR output file\n"); + log("\n"); + log(" write_churchroad [options] [filename]\n"); + log("\n"); + log("Write a Churchroad description of the current design.\n"); + log("\n"); + log(" -salt\n"); + log(" Salt string to add to all egglog commands.\n"); // log("\n"); // log(" -s\n"); // log(" Output only a single bad property for all asserts\n"); @@ -2063,28 +758,64 @@ struct BtorBackend : public Backend RTLIL::Module *topmod = design->top_module(); - size_t argidx = args.size(); + // Maps port names to egglog expression strings that they should be `union`ed with. + std::map port_to_expr_map; + std::string salt = ""; + bool let_bindings = false; + for (size_t arg_i = 1; arg_i < args.size();) + { + // Look for -portunion option + if (args[arg_i] == "-portunion") + { + log_assert(args.size() > arg_i + 2); + // Replace underscores with spaces. + // TODO(@gussmith23): Shouldn't be needed after we figure out quoting in Yosys commands. + port_to_expr_map[args[arg_i + 1]] = + std::regex_replace(args[arg_i + 2], std::regex("_"), " "); + arg_i += 3; + continue; + } - if (filename == "") - { - // The command itself is given as an arg - if (argidx > 1 && args[argidx - 1][0] != '-') + // Look for -salt option + if (args[arg_i] == "-salt") { - // extra_args and friends need to see this argument. - argidx -= 1; - filename = args[argidx]; + log_assert(args.size() > arg_i + 1); + salt = args[arg_i + 1]; + arg_i += 2; + continue; } + + // Look for filename as last argument. + if (arg_i == args.size() - 1 && args[arg_i][0] != '-') + { + // Confusingly, this is failing when filename is "" + // log_assert(filename.empty()); + filename = args[arg_i]; + arg_i++; + continue; + } + + // Look for -letbindings option + if (args[arg_i] == "-letbindings") + { + let_bindings = true; + arg_i += 1; + continue; + } + + log_error("Unrecognized option: %s", args[arg_i].c_str()); } + // Has to come after other arg parsing. - extra_args(f, filename, args, argidx); + extra_args(f, filename, args, args.size()); if (topmod == nullptr) log_cmd_error("No top module found.\n"); - LakeroadWorker(*f, topmod).run(); + LakeroadWorker(*f, topmod, salt, let_bindings, port_to_expr_map).run(); // *f << stringf("; end of yosys output\n"); } -} BtorBackend; +} ChurchroadBackend; PRIVATE_NAMESPACE_END diff --git a/yosys-plugin/tests/2bit-rca.sv b/yosys-plugin/tests/2bit-rca.sv index f9bc8f8..bb6fee8 100644 --- a/yosys-plugin/tests/2bit-rca.sv +++ b/yosys-plugin/tests/2bit-rca.sv @@ -1,5 +1,5 @@ // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top top; pmuxtree; prep; write_lakeroad' \ +// RUN: -p 'read_verilog -sv %s; prep -top top; pmuxtree; prep; write_churchroad' \ // RUN: | FileCheck %s module top @@ -57,29 +57,8 @@ endmodule // CHECK: (union v3 (Op2 (Xor) v5 v6)) // CHECK: (union v10 (Op2 (Xor) v7 v8)) // CHECK: (union v4 (Op2 (Xor) v10 v11)) -// CHECK: (let i_a (Var "i_a" 2)) -// CHECK: (IsPort "" "i_a" (Input) i_a) -// CHECK: (union v13 i_a) -// CHECK: (let i_b (Var "i_b" 2)) -// CHECK: (IsPort "" "i_b" (Input) i_b) -// CHECK: (union v14 i_b) -// CHECK: (let o_c v12) -// CHECK: (IsPort "" "o_c" (Output) o_c) -// CHECK: (let o_s v15) -// CHECK: (IsPort "" "o_s" (Output) o_s) -// CHECK: (delete (Wire "v0" 1)) -// CHECK: (delete (Wire "v1" 1)) -// CHECK: (delete (Wire "v2" 1)) -// CHECK: (delete (Wire "v3" 1)) -// CHECK: (delete (Wire "v4" 1)) -// CHECK: (delete (Wire "v5" 1)) -// CHECK: (delete (Wire "v6" 1)) -// CHECK: (delete (Wire "v7" 1)) -// CHECK: (delete (Wire "v8" 1)) -// CHECK: (delete (Wire "v9" 1)) -// CHECK: (delete (Wire "v10" 1)) -// CHECK: (delete (Wire "v11" 1)) -// CHECK: (delete (Wire "v12" 1)) -// CHECK: (delete (Wire "v13" 2)) -// CHECK: (delete (Wire "v14" 2)) -// CHECK: (delete (Wire "v15" 2)) +// CHECK: (IsPort "" "i_a" (Input) v13) +// CHECK: (IsPort "" "i_b" (Input) v14) +// CHECK: (IsPort "" "o_c" (Output) v12) +// CHECK: (IsPort "" "o_s" (Output) v15) +// CHECK: (run-schedule (saturate (seq typing misc))) diff --git a/yosys-plugin/tests/adder.sv b/yosys-plugin/tests/adder.sv index 6014773..19de79b 100644 --- a/yosys-plugin/tests/adder.sv +++ b/yosys-plugin/tests/adder.sv @@ -1,5 +1,5 @@ // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top test; pmuxtree; prep; write_lakeroad' \ +// RUN: -p 'read_verilog -sv %s; prep -top test; pmuxtree; prep; write_churchroad' \ // RUN: | FileCheck %s module test(input a, b, output out); @@ -10,14 +10,7 @@ endmodule // CHECK: (let v1 (Wire "v1" 1)) // CHECK: (let v2 (Wire "v2" 1)) // CHECK: (union v2 (Op2 (Add) v0 v1)) -// CHECK: (let a (Var "a" 1)) -// CHECK: (IsPort "" "a" (Input) a) -// CHECK: (union v0 a) -// CHECK: (let b (Var "b" 1)) -// CHECK: (IsPort "" "b" (Input) b) -// CHECK: (union v1 b) -// CHECK: (let out v2) -// CHECK: (IsPort "" "out" (Output) out) -// CHECK: (delete (Wire "v0" 1)) -// CHECK: (delete (Wire "v1" 1)) -// CHECK: (delete (Wire "v2" 1)) +// CHECK: (IsPort "" "a" (Input) v0) +// CHECK: (IsPort "" "b" (Input) v1) +// CHECK: (IsPort "" "out" (Output) v2) +// CHECK: (run-schedule (saturate (seq typing misc))) diff --git a/yosys-plugin/tests/concat.sv b/yosys-plugin/tests/concat.sv index 8f70307..7a2cae7 100644 --- a/yosys-plugin/tests/concat.sv +++ b/yosys-plugin/tests/concat.sv @@ -1,5 +1,5 @@ // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top test; write_lakeroad' \ +// RUN: -p 'read_verilog -sv %s; prep -top test; write_churchroad' \ // RUN: | FileCheck %s module test(input a, b, output[1:0] out); @@ -10,14 +10,7 @@ endmodule // CHECK: (let v1 (Wire "v1" 1)) // CHECK: (let v2 (Wire "v2" 2)) // CHECK: (union v2 (Op2 (Concat) v0 v1)) -// CHECK: (let a (Var "a" 1)) -// CHECK: (IsPort "" "a" (Input) a) -// CHECK: (union v0 a) -// CHECK: (let b (Var "b" 1)) -// CHECK: (IsPort "" "b" (Input) b) -// CHECK: (union v1 b) -// CHECK: (let out v2) -// CHECK: (IsPort "" "out" (Output) out) -// CHECK: (delete (Wire "v0" 1)) -// CHECK: (delete (Wire "v1" 1)) -// CHECK: (delete (Wire "v2" 2)) +// CHECK: (IsPort "" "a" (Input) v0) +// CHECK: (IsPort "" "b" (Input) v1) +// CHECK: (IsPort "" "out" (Output) v2) +// CHECK: (run-schedule (saturate (seq typing misc))) diff --git a/yosys-plugin/tests/dsp48e2.sv b/yosys-plugin/tests/dsp48e2.sv new file mode 100644 index 0000000..efc58c8 --- /dev/null +++ b/yosys-plugin/tests/dsp48e2.sv @@ -0,0 +1,262 @@ +// RUN: $YOSYS -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ +// RUN: -qp 'read_verilog -sv %s; hierarchy -top top; write_churchroad' \ +// RUN: | FileCheck %s + +module top(a, b, out); + wire [47:0] P_0; + input [15:0] a; + wire [15:0] a; + input [15:0] b; + wire [15:0] b; + output [15:0] out; + wire [15:0] out; + DSP48E2 #( + .ACASCREG(32'd0), + .ADREG(32'd0), + .ALUMODEREG(32'd0), + .AMULTSEL("AD"), + .AREG(32'd0), + .AUTORESET_PATDET("NO_RESET"), + .AUTORESET_PRIORITY("RESET"), + .A_INPUT("DIRECT"), + .BCASCREG(32'd0), + .BMULTSEL("B"), + .BREG(32'd0), + .B_INPUT("DIRECT"), + .CARRYINREG(32'd0), + .CARRYINSELREG(32'd1), + .CREG(32'd0), + .DREG(32'd0), + .INMODEREG(32'd1), + .IS_ALUMODE_INVERTED(4'h0), + .IS_CARRYIN_INVERTED(1'h0), + .IS_CLK_INVERTED(1'h0), + .IS_INMODE_INVERTED(5'h00), + .IS_OPMODE_INVERTED(9'h000), + .IS_RSTALLCARRYIN_INVERTED(1'h0), + .IS_RSTALUMODE_INVERTED(1'h0), + .IS_RSTA_INVERTED(1'h0), + .IS_RSTB_INVERTED(1'h0), + .IS_RSTCTRL_INVERTED(1'h0), + .IS_RSTC_INVERTED(1'h0), + .IS_RSTD_INVERTED(1'h0), + .IS_RSTINMODE_INVERTED(1'h0), + .IS_RSTM_INVERTED(1'h0), + .IS_RSTP_INVERTED(1'h0), + .MASK(48'h000000000000), + .MREG(32'd0), + .OPMODEREG(32'd0), + .PATTERN(48'h000000000000), + .PREADDINSEL("A"), + .PREG(32'd0), + .RND(48'h000000000000), + .SEL_MASK("MASK"), + .SEL_PATTERN("PATTERN"), + .USE_MULT("MULTIPLY"), + .USE_PATTERN_DETECT("NO_PATDET"), + .USE_SIMD("ONE48"), + .USE_WIDEXOR("FALSE"), + .XORSIMD("XOR12") + ) DSP48E2_0 ( + .A({ a[15], a[15], a[15], a[15], a[15], a[15], a[15], a[15], a[15], a[15], a[15], a[15], a[15], a[15], a }), + .ACIN(30'h00000000), + .ALUMODE(4'h7), + .B({ b[15], b[15], b }), + .BCIN(18'h00000), + .C(48'h000000000000), + .CARRYCASCIN(1'h0), + .CARRYIN(1'h0), + .CARRYINSEL(3'h6), + .CEA1(1'h1), + .CEA2(1'h1), + .CEAD(1'h1), + .CEALUMODE(1'h1), + .CEB1(1'h1), + .CEB2(1'h1), + .CEC(1'h1), + .CECARRYIN(1'h1), + .CECTRL(1'h1), + .CED(1'h1), + .CEINMODE(1'h1), + .CEM(1'h1), + .CEP(1'h1), + .CLK(1'h0), + .D(27'h0000000), + .INMODE(5'h1b), + .MULTSIGNIN(1'h0), + .OPMODE(9'h035), + .P({ P_0[47:16], out }), + .PCIN(48'h000000000000), + .RSTA(1'h0), + .RSTALLCARRYIN(1'h0), + .RSTALUMODE(1'h0), + .RSTB(1'h0), + .RSTC(1'h0), + .RSTCTRL(1'h0), + .RSTD(1'h0), + .RSTINMODE(1'h0), + .RSTM(1'h0), + .RSTP(1'h0) + ); + assign P_0[15] = out[15]; + assign P_0[14] = out[14]; + assign P_0[13] = out[13]; + assign P_0[12] = out[12]; + assign P_0[11] = out[11]; + assign P_0[10] = out[10]; + assign P_0[9] = out[9]; + assign P_0[8] = out[8]; + assign P_0[7] = out[7]; + assign P_0[6] = out[6]; + assign P_0[5] = out[5]; + assign P_0[4] = out[4]; + assign P_0[3] = out[3]; + assign P_0[2] = out[2]; + assign P_0[1] = out[1]; + assign P_0[0] = out[0]; +endmodule + +// DSP48E2 definition from Xilinx. Note that we keep the module empty for now -- +// we only need the input/output port definitions. + +/////////////////////////////////////////////////////////////////////////////// +// Copyright (c) 1995/2018 Xilinx, Inc. +// All Right Reserved. +/////////////////////////////////////////////////////////////////////////////// +// ____ ____ +// / /\/ / +// /___/ \ / Vendor : Xilinx +// \ \ \/ Version : 2018.3 +// \ \ Description : Xilinx Unified Simulation Library Component +// / / 48-bit Multi-Functional Arithmetic Block +// /___/ /\ Filename : DSP48E2.v +// \ \ / \ +// \___\/\___\ +// +/////////////////////////////////////////////////////////////////////////////// +// Revision: +// 07/15/12 - Migrate from E1. +// 12/10/12 - Add dynamic registers +// 01/10/13 - 694456 - DIN_in/D_in connectivity issue +// 01/11/13 - DIN, D_DATA data width change (26/24) sync4 yml +// 02/13/13 - PCIN_47A change from internal feedback to PCIN(47) pin +// 03/06/13 - 701316 - A_B_reg no clk when REG=0 +// 04/03/13 - yaml update +// 04/08/13 - 710304 - AREG, BREG, ACASCREG and BCASCREG dynamic registers mis sized. +// 04/22/13 - 714213 - ACOUT, BCOUT wrong logic +// 04/22/13 - 713695 - Zero mult result on USE_SIMD +// 04/22/13 - 713617 - CARRYCASCOUT behaviour +// 04/23/13 - 714772 - remove sensitivity to negedge GSR +// 04/23/13 - 713706 - change P_PDBK connection +// 05/07/13 - 716896 - AREG, BREG, ACASCREG and BCASCREG localparams mis sized. +// 05/07/13 - 716896 - ALUMODE/OPMODE_INV_REG mis sized +// 05/07/13 - 716896 - INMODE_INV_REG mis sized +// 05/07/13 - x_mac_cascd missing for sensitivity list. +// 10/22/14 - 808642 - Added #1 to $finish +// End Revision: +/////////////////////////////////////////////////////////////////////////////// + +module DSP48E2 #( + parameter integer ACASCREG = 1, + parameter integer ADREG = 1, + parameter integer ALUMODEREG = 1, + parameter AMULTSEL = "A", + parameter integer AREG = 1, + parameter AUTORESET_PATDET = "NO_RESET", + parameter AUTORESET_PRIORITY = "RESET", + parameter A_INPUT = "DIRECT", + parameter integer BCASCREG = 1, + parameter BMULTSEL = "B", + parameter integer BREG = 1, + parameter B_INPUT = "DIRECT", + parameter integer CARRYINREG = 1, + parameter integer CARRYINSELREG = 1, + parameter integer CREG = 1, + parameter integer DREG = 1, + parameter integer INMODEREG = 1, + parameter [3:0] IS_ALUMODE_INVERTED = 4'b0000, + parameter [0:0] IS_CARRYIN_INVERTED = 1'b0, + parameter [0:0] IS_CLK_INVERTED = 1'b0, + parameter [4:0] IS_INMODE_INVERTED = 5'b00000, + parameter [8:0] IS_OPMODE_INVERTED = 9'b000000000, + parameter [0:0] IS_RSTALLCARRYIN_INVERTED = 1'b0, + parameter [0:0] IS_RSTALUMODE_INVERTED = 1'b0, + parameter [0:0] IS_RSTA_INVERTED = 1'b0, + parameter [0:0] IS_RSTB_INVERTED = 1'b0, + parameter [0:0] IS_RSTCTRL_INVERTED = 1'b0, + parameter [0:0] IS_RSTC_INVERTED = 1'b0, + parameter [0:0] IS_RSTD_INVERTED = 1'b0, + parameter [0:0] IS_RSTINMODE_INVERTED = 1'b0, + parameter [0:0] IS_RSTM_INVERTED = 1'b0, + parameter [0:0] IS_RSTP_INVERTED = 1'b0, + parameter [47:0] MASK = 48'h3FFFFFFFFFFF, + parameter integer MREG = 1, + parameter integer OPMODEREG = 1, + parameter [47:0] PATTERN = 48'h000000000000, + parameter PREADDINSEL = "A", + parameter integer PREG = 1, + parameter [47:0] RND = 48'h000000000000, + parameter SEL_MASK = "MASK", + parameter SEL_PATTERN = "PATTERN", + parameter USE_MULT = "MULTIPLY", + parameter USE_PATTERN_DETECT = "NO_PATDET", + parameter USE_SIMD = "ONE48", + parameter USE_WIDEXOR = "FALSE", + parameter XORSIMD = "XOR24_48_96" +) ( + output [29:0] ACOUT, + output [17:0] BCOUT, + output CARRYCASCOUT, + output [3:0] CARRYOUT, + output MULTSIGNOUT, + output OVERFLOW, + output [47:0] P, + output PATTERNBDETECT, + output PATTERNDETECT, + output [47:0] PCOUT, + output UNDERFLOW, + output [7:0] XOROUT, + + input [29:0] A, + input [29:0] ACIN, + input [3:0] ALUMODE, + input [17:0] B, + input [17:0] BCIN, + input [47:0] C, + input CARRYCASCIN, + input CARRYIN, + input [2:0] CARRYINSEL, + input CEA1, + input CEA2, + input CEAD, + input CEALUMODE, + input CEB1, + input CEB2, + input CEC, + input CECARRYIN, + input CECTRL, + input CED, + input CEINMODE, + input CEM, + input CEP, + input CLK, + input [26:0] D, + input [4:0] INMODE, + input MULTSIGNIN, + input [8:0] OPMODE, + input [47:0] PCIN, + input RSTA, + input RSTALLCARRYIN, + input RSTALUMODE, + input RSTB, + input RSTC, + input RSTCTRL, + input RSTD, + input RSTINMODE, + input RSTM, + input RSTP +); + +endmodule + +// CHECK: (let DSP48E2_0- (ModuleInstance "DSP48E2" (StringCons "ACASCREG"(StringCons "ADREG"(StringCons "ALUMODEREG"(StringCons "AMULTSEL"(StringCons "AREG"(StringCons "AUTORESET_PATDET"(StringCons "AUTORESET_PRIORITY"(StringCons "A_INPUT"(StringCons "BCASCREG"(StringCons "BMULTSEL"(StringCons "BREG"(StringCons "B_INPUT"(StringCons "CARRYINREG"(StringCons "CARRYINSELREG"(StringCons "CREG"(StringCons "DREG"(StringCons "INMODEREG"(StringCons "IS_ALUMODE_INVERTED"(StringCons "IS_CARRYIN_INVERTED"(StringCons "IS_CLK_INVERTED"(StringCons "IS_INMODE_INVERTED"(StringCons "IS_OPMODE_INVERTED"(StringCons "IS_RSTALLCARRYIN_INVERTED"(StringCons "IS_RSTALUMODE_INVERTED"(StringCons "IS_RSTA_INVERTED"(StringCons "IS_RSTB_INVERTED"(StringCons "IS_RSTCTRL_INVERTED"(StringCons "IS_RSTC_INVERTED"(StringCons "IS_RSTD_INVERTED"(StringCons "IS_RSTINMODE_INVERTED"(StringCons "IS_RSTM_INVERTED"(StringCons "IS_RSTP_INVERTED"(StringCons "MASK"(StringCons "MREG"(StringCons "OPMODEREG"(StringCons "PATTERN"(StringCons "PREADDINSEL"(StringCons "PREG"(StringCons "RND"(StringCons "SEL_MASK"(StringCons "SEL_PATTERN"(StringCons "USE_MULT"(StringCons "USE_PATTERN_DETECT"(StringCons "USE_SIMD"(StringCons "USE_WIDEXOR"(StringCons "XORSIMD"(StringNil)))))))))))))))))))))))))))))))))))))))))))))))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (CRString "AD"))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (CRString "NO_RESET"))(ExprCons (Op0 (CRString "RESET"))(ExprCons (Op0 (CRString "DIRECT"))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (CRString "B"))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (CRString "DIRECT"))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 1 32))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 1 32))(ExprCons (Op0 (BV 0 4))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 5))(ExprCons (Op0 (BV 0 9))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 1))(ExprCons (Op0 (BV 0 48))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 0 48))(ExprCons (Op0 (CRString "A"))(ExprCons (Op0 (BV 0 32))(ExprCons (Op0 (BV 0 48))(ExprCons (Op0 (CRString "MASK"))(ExprCons (Op0 (CRString "PATTERN"))(ExprCons (Op0 (CRString "MULTIPLY"))(ExprCons (Op0 (CRString "NO_PATDET"))(ExprCons (Op0 (CRString "ONE48"))(ExprCons (Op0 (CRString "FALSE"))(ExprCons (Op0 (CRString "XOR12"))(ExprNil)))))))))))))))))))))))))))))))))))))))))))))))(StringCons "A"(StringCons "ACIN"(StringCons "ALUMODE"(StringCons "B"(StringCons "BCIN"(StringCons "C"(StringCons "CARRYCASCIN"(StringCons "CARRYIN"(StringCons "CARRYINSEL"(StringCons "CEA1"(StringCons "CEA2"(StringCons "CEAD"(StringCons "CEALUMODE"(StringCons "CEB1"(StringCons "CEB2"(StringCons "CEC"(StringCons "CECARRYIN"(StringCons "CECTRL"(StringCons "CED"(StringCons "CEINMODE"(StringCons "CEM"(StringCons "CEP"(StringCons "CLK"(StringCons "D"(StringCons "INMODE"(StringCons "MULTSIGNIN"(StringCons "OPMODE"(StringCons "PCIN"(StringCons "RSTA"(StringCons "RSTALLCARRYIN"(StringCons "RSTALUMODE"(StringCons "RSTB"(StringCons "RSTC"(StringCons "RSTCTRL"(StringCons "RSTD"(StringCons "RSTINMODE"(StringCons "RSTM"(StringCons "RSTP"(StringNil)))))))))))))))))))))))))))))))))))))))(ExprCons v13(ExprCons v24(ExprCons v25(ExprCons v15(ExprCons v26(ExprCons v27(ExprCons v28(ExprCons v28(ExprCons v29(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v30(ExprCons v28(ExprCons v31(ExprCons v32(ExprCons v28(ExprCons v33(ExprCons v27(ExprCons v28(ExprCons v28(ExprCons v28(ExprCons v28(ExprCons v28(ExprCons v28(ExprCons v28(ExprCons v28(ExprCons v28(ExprCons v28(ExprNil))))))))))))))))))))))))))))))))))))))))) diff --git a/yosys-plugin/tests/example.ys b/yosys-plugin/tests/example.ys index 79bd7c7..d346cd0 100644 --- a/yosys-plugin/tests/example.ys +++ b/yosys-plugin/tests/example.ys @@ -8,10 +8,7 @@ module test(input [1:0] a, input b, output o); endmodule EOF -write_lakeroad -# Write output to file.egg -write_lakeroad file.egg -!rm file.egg +write_churchroad # CHECK: (let v0 (Wire "v0" 2)) # CHECK: (let v1 (Wire "v1" 2)) @@ -20,15 +17,3 @@ write_lakeroad file.egg # CHECK: (let v4 (Op1 (ZeroExtend 2) v2)) # CHECK: (union v0 (Op2 (And) v1 v4)) # CHECK: (union v3 (Op1 (Extract 0 0) v0)) -# CHECK: (let a (Var "a" 2)) -# CHECK: (IsPort "" "a" (Input) a) -# CHECK: (union v1 a) -# CHECK: (let b (Var "b" 1)) -# CHECK: (IsPort "" "b" (Input) b) -# CHECK: (union v2 b) -# CHECK: (let o v3) -# CHECK: (IsPort "" "o" (Output) o) -# CHECK: (delete (Wire "v0" 2)) -# CHECK: (delete (Wire "v1" 2)) -# CHECK: (delete (Wire "v2" 1)) -# CHECK: (delete (Wire "v3" 1)) diff --git a/yosys-plugin/tests/extract-bug.sv b/yosys-plugin/tests/extract-bug.sv index 7ee9e55..2416ea1 100644 --- a/yosys-plugin/tests/extract-bug.sv +++ b/yosys-plugin/tests/extract-bug.sv @@ -5,7 +5,7 @@ // ... // // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top test; write_lakeroad' \ +// RUN: -p 'read_verilog -sv %s; prep -top test; write_churchroad' \ // RUN: | FileCheck %s module test(input [1:0] in, output out); @@ -14,11 +14,4 @@ endmodule // CHECK: (let v0 (Wire "v0" 2)) // CHECK: (let v1 (Wire "v1" 1)) -// CHECK: (union v1 (Op1 (Extract 1 1) v0)) -// CHECK: (let in (Var "in" 2)) -// CHECK: (IsPort "" "in" (Input) in) -// CHECK: (union v0 in) -// CHECK: (let out v1) -// CHECK: (IsPort "" "out" (Output) out) -// CHECK: (delete (Wire "v0" 2)) -// CHECK: (delete (Wire "v1" 1)) +// CHECK: (union v1 (Op1 (Extract 1 1) v0)) \ No newline at end of file diff --git a/yosys-plugin/tests/module-instance.sv b/yosys-plugin/tests/module-instance.sv index 05c7c76..5098764 100644 --- a/yosys-plugin/tests/module-instance.sv +++ b/yosys-plugin/tests/module-instance.sv @@ -1,5 +1,5 @@ // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top test; write_lakeroad' \ +// RUN: -p 'read_verilog -sv %s; prep -top test; write_churchroad' \ // RUN: | FileCheck %s module some_module(input a, b, output out); @@ -13,15 +13,9 @@ endmodule // CHECK: (let v0 (Wire "v0" 1)) // CHECK: (let v1 (Wire "v1" 1)) // CHECK: (let v2 (Wire "v2" 1)) -// CHECK: (let some_module_instance (ModuleInstance "some_module" (vec-of "a" "b") (vec-of v0 v1))) -// CHECK: (let a (Var "a" 1)) -// CHECK: (IsPort "" "a" (Input) a) -// CHECK: (union v0 a) -// CHECK: (let b (Var "b" 1)) -// CHECK: (IsPort "" "b" (Input) b) -// CHECK: (union v1 b) -// CHECK: (let out v2) -// CHECK: (IsPort "" "out" (Output) out) -// CHECK: (delete (Wire "v0" 1)) -// CHECK: (delete (Wire "v1" 1)) -// CHECK: (delete (Wire "v2" 1)) \ No newline at end of file +// CHECK: (let some_module_instance- (ModuleInstance "some_module" (StringNil)(ExprNil)(StringCons "a"(StringCons "b"(StringNil)))(ExprCons v0(ExprCons v1(ExprNil))))) +// CHECK: (union (GetOutput some_module_instance- "out") v2) +// CHECK: (IsPort "" "a" (Input) v0) +// CHECK: (IsPort "" "b" (Input) v1) +// CHECK: (IsPort "" "out" (Output) v2) +// CHECK: (run-schedule (saturate (seq typing misc))) diff --git a/yosys-plugin/tests/permuter.sv b/yosys-plugin/tests/permuter.sv index e31bc2f..75d49a0 100644 --- a/yosys-plugin/tests/permuter.sv +++ b/yosys-plugin/tests/permuter.sv @@ -22,7 +22,7 @@ // TODO(@gussmith23): are we in line with this license? // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top permuter_4x4_sim; pmuxtree; prep; write_lakeroad' \ +// RUN: -p 'read_verilog -sv %s; prep -top permuter_4x4_sim; pmuxtree; prep; write_churchroad' \ // RUN: | FileCheck %s module permuter_4x4_sim #( @@ -102,39 +102,4 @@ endmodule // CHECK: (union v18 (Op2 (Eq) v21 v25)) // CHECK: (let v26 (Op0 (BV 1 1))) // CHECK: (let v27 (Op1 (ZeroExtend 2) v26)) -// CHECK: (union v19 (Op2 (Eq) v21 v27)) -// CHECK: (let clk (Var "clk" 1)) -// CHECK: (IsPort "" "clk" (Input) clk) -// CHECK: (union v20 clk) -// CHECK: (let control (Var "control" 2)) -// CHECK: (IsPort "" "control" (Input) control) -// CHECK: (union v21 control) -// CHECK: (let din (Var "din" 16)) -// CHECK: (IsPort "" "din" (Input) din) -// CHECK: (union v22 din) -// CHECK: (let dout v23) -// CHECK: (IsPort "" "dout" (Output) dout) -// CHECK: (delete (Wire "v0" 16)) -// CHECK: (delete (Wire "v1" 1)) -// CHECK: (delete (Wire "v2" 16)) -// CHECK: (delete (Wire "v3" 16)) -// CHECK: (delete (Wire "v4" 8)) -// CHECK: (delete (Wire "v5" 12)) -// CHECK: (delete (Wire "v6" 16)) -// CHECK: (delete (Wire "v7" 16)) -// CHECK: (delete (Wire "v8" 8)) -// CHECK: (delete (Wire "v9" 12)) -// CHECK: (delete (Wire "v10" 16)) -// CHECK: (delete (Wire "v11" 4)) -// CHECK: (delete (Wire "v12" 4)) -// CHECK: (delete (Wire "v13" 4)) -// CHECK: (delete (Wire "v14" 4)) -// CHECK: (delete (Wire "v15" 8)) -// CHECK: (delete (Wire "v16" 8)) -// CHECK: (delete (Wire "v17" 1)) -// CHECK: (delete (Wire "v18" 1)) -// CHECK: (delete (Wire "v19" 1)) -// CHECK: (delete (Wire "v20" 1)) -// CHECK: (delete (Wire "v21" 2)) -// CHECK: (delete (Wire "v22" 16)) -// CHECK: (delete (Wire "v23" 16)) +// CHECK: (union v19 (Op2 (Eq) v21 v27)) \ No newline at end of file diff --git a/yosys-plugin/tests/shiftx.sv b/yosys-plugin/tests/shiftx.sv index 2265dbb..a5d9cbe 100644 --- a/yosys-plugin/tests/shiftx.sv +++ b/yosys-plugin/tests/shiftx.sv @@ -2,7 +2,7 @@ // encounters something like `mem[idx]` in a design. // // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top test; write_lakeroad' +// RUN: -p 'read_verilog -sv %s; prep -top test; write_churchroad' // | FileCheck %s module test diff --git a/yosys-plugin/tests/simple.sv b/yosys-plugin/tests/simple.sv index 39a1372..379f6e7 100644 --- a/yosys-plugin/tests/simple.sv +++ b/yosys-plugin/tests/simple.sv @@ -1,5 +1,5 @@ // RUN: $YOSYS -q -m $CHURCHROAD_DIR/yosys-plugin/churchroad.so \ -// RUN: -p 'read_verilog -sv %s; prep -top test; write_lakeroad' \ +// RUN: -p 'read_verilog -sv %s; prep -top test; write_churchroad' \ // RUN: | FileCheck %s module test(input a, b, output out); @@ -9,15 +9,4 @@ endmodule // CHECK: (let v0 (Wire "v0" 1)) // CHECK: (let v1 (Wire "v1" 1)) // CHECK: (let v2 (Wire "v2" 1)) -// CHECK: (union v2 (Op2 (And) v0 v1)) -// CHECK: (let a (Var "a" 1)) -// CHECK: (IsPort "" "a" (Input) a) -// CHECK: (union v0 a) -// CHECK: (let b (Var "b" 1)) -// CHECK: (IsPort "" "b" (Input) b) -// CHECK: (union v1 b) -// CHECK: (let out v2) -// CHECK: (IsPort "" "out" (Output) out) -// CHECK: (delete (Wire "v0" 1)) -// CHECK: (delete (Wire "v1" 1)) -// CHECK: (delete (Wire "v2" 1)) +// CHECK: (union v2 (Op2 (And) v0 v1)) \ No newline at end of file