--- /srv/reproducible-results/rbuild-debian/r-b-build.zR9MYIzi/b1/yosys_0.52-1_i386.changes +++ /srv/reproducible-results/rbuild-debian/r-b-build.zR9MYIzi/b2/yosys_0.52-1_i386.changes ├── Files │ @@ -1,7 +1,7 @@ │ │ 86a12c5265ef432030e39fabd96f0f3d 28731224 debug optional yosys-abc-dbgsym_0.52-1_i386.deb │ 0325c6c46e76d6ec3a6e6d0cdc0baa2c 5020116 electronics optional yosys-abc_0.52-1_i386.deb │ 94c2ab20f62ca0ce1870b5de85dbdbe3 91802040 debug optional yosys-dbgsym_0.52-1_i386.deb │ - e953f16e199c314ec3df186763a066f0 136136 electronics optional yosys-dev_0.52-1_i386.deb │ - ad8a3dfaacec8adc2e92db90289bf470 2916440 doc optional yosys-doc_0.52-1_all.deb │ + 998620d67d3097e8582080ce9d66982f 136260 electronics optional yosys-dev_0.52-1_i386.deb │ + 71496bd0c7c9f94b968328c1d60220dc 2917060 doc optional yosys-doc_0.52-1_all.deb │ dee5e80930b9a21ea836bd71dbecdabd 6424884 electronics optional yosys_0.52-1_i386.deb ├── yosys-dev_0.52-1_i386.deb │ ├── file list │ │ @@ -1,3 +1,3 @@ │ │ -rw-r--r-- 0 0 0 4 2025-04-11 08:41:09.000000 debian-binary │ │ -rw-r--r-- 0 0 0 2308 2025-04-11 08:41:09.000000 control.tar.xz │ │ --rw-r--r-- 0 0 0 133636 2025-04-11 08:41:09.000000 data.tar.xz │ │ +-rw-r--r-- 0 0 0 133760 2025-04-11 08:41:09.000000 data.tar.xz │ ├── control.tar.xz │ │ ├── control.tar │ │ │ ├── ./md5sums │ │ │ │ ├── ./md5sums │ │ │ │ │┄ Files differ │ ├── data.tar.xz │ │ ├── data.tar │ │ │ ├── file list │ │ │ │ @@ -1,11 +1,11 @@ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/bin/ │ │ │ │ --rwxr-xr-x 0 root (0) root (0) 3375 2025-04-11 08:41:09.000000 ./usr/bin/yosys-config │ │ │ │ +-rwxr-xr-x 0 root (0) root (0) 3873 2025-04-11 08:41:09.000000 ./usr/bin/yosys-config │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/doc/ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys-dev/ │ │ │ │ -rw-r--r-- 0 root (0) root (0) 2826 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys-dev/changelog.Debian.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 18593 2025-04-09 05:38:42.000000 ./usr/share/doc/yosys-dev/changelog.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 23806 2025-04-11 08:32:04.000000 ./usr/share/doc/yosys-dev/copyright │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/man/ │ │ │ ├── ./usr/bin/yosys-config │ │ │ │ @@ -4,15 +4,15 @@ │ │ │ │ { │ │ │ │ echo "" │ │ │ │ echo "Usage: $0 [--exec] [--prefix pf] args.." │ │ │ │ echo " $0 --build modname.so cppsources.." │ │ │ │ echo "" │ │ │ │ echo "Replacement args:" │ │ │ │ echo " --cxx g++" │ │ │ │ - echo " --cxxflags $( echo '-g -O2 -flto=auto -ffat-lto-objects -fstack-protector-strong -Wformat -Werror=format-security -Wall -Wextra -ggdb -I/usr/share/yosys/include -MD -MP -D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER=' | fmt -w60 | sed ':a;N;$!ba;s/\n/ \\\n /g' )" │ │ │ │ + echo " --cxxflags $( echo '-g -O2 -flto=auto -ffat-lto-objects -fstack-protector-strong -Wformat -Werror=format-security -Wall -Wextra -ggdb -I/usr/share/yosys/include -MD -MP -D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER=@CXXFLAGS@.52 -DYOSYS_MAJOR=0 -DYOSYS_MINOR=52 -DYOSYS_COMMIT=0.52 -std=c++17 -O3 -DYOSYS_ENABLE_READLINE -DYOSYS_ENABLE_PLUGINS -DYOSYS_ENABLE_GLOB -DYOSYS_ENABLE_ZLIB -I/usr/include/tcl8.6 -DYOSYS_ENABLE_TCL -DYOSYS_ENABLE_ABC -DYOSYS_ENABLE_COVER' | fmt -w60 | sed ':a;N;$!ba;s/\n/ \\\n /g' )" │ │ │ │ echo " --linkflags -rdynamic" │ │ │ │ echo " --ldflags (alias of --linkflags)" │ │ │ │ echo " --libs -lstdc++ -lm -lrt -lreadline -lffi -ldl -lz -ltcl8.6 -ltclstub8.6" │ │ │ │ echo " --ldlibs (alias of --libs)" │ │ │ │ echo " --bindir /usr/bin" │ │ │ │ echo " --datdir /usr/share/yosys" │ │ │ │ echo "" │ │ │ │ @@ -60,15 +60,15 @@ │ │ │ │ get_prefix=false │ │ │ │ continue │ │ │ │ fi │ │ │ │ case "$opt" in │ │ │ │ "$prefix"cxx) │ │ │ │ tokens=( "${tokens[@]}" g++ ) ;; │ │ │ │ "$prefix"cxxflags) │ │ │ │ - tokens=( "${tokens[@]}" -g -O2 -flto=auto -ffat-lto-objects -fstack-protector-strong -Wformat -Werror=format-security -Wall -Wextra -ggdb -I/usr/share/yosys/include -MD -MP -D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER= ) ;; │ │ │ │ + tokens=( "${tokens[@]}" -g -O2 -flto=auto -ffat-lto-objects -fstack-protector-strong -Wformat -Werror=format-security -Wall -Wextra -ggdb -I/usr/share/yosys/include -MD -MP -D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER=@CXXFLAGS@.52 -DYOSYS_MAJOR=0 -DYOSYS_MINOR=52 -DYOSYS_COMMIT=0.52 -std=c++17 -O3 -DYOSYS_ENABLE_READLINE -DYOSYS_ENABLE_PLUGINS -DYOSYS_ENABLE_GLOB -DYOSYS_ENABLE_ZLIB -I/usr/include/tcl8.6 -DYOSYS_ENABLE_TCL -DYOSYS_ENABLE_ABC -DYOSYS_ENABLE_COVER ) ;; │ │ │ │ "$prefix"linkflags) │ │ │ │ tokens=( "${tokens[@]}" -rdynamic ) ;; │ │ │ │ "$prefix"libs) │ │ │ │ tokens=( "${tokens[@]}" -lstdc++ -lm -lrt -lreadline -lffi -ldl -lz -ltcl8.6 -ltclstub8.6 ) ;; │ │ │ │ "$prefix"ldflags) │ │ │ │ tokens=( "${tokens[@]}" -rdynamic ) ;; │ │ │ │ "$prefix"ldlibs) ├── yosys-doc_0.52-1_all.deb │ ├── file list │ │ @@ -1,3 +1,3 @@ │ │ -rw-r--r-- 0 0 0 4 2025-04-11 08:41:09.000000 debian-binary │ │ -rw-r--r-- 0 0 0 888 2025-04-11 08:41:09.000000 control.tar.xz │ │ --rw-r--r-- 0 0 0 2915360 2025-04-11 08:41:09.000000 data.tar.xz │ │ +-rw-r--r-- 0 0 0 2915980 2025-04-11 08:41:09.000000 data.tar.xz │ ├── control.tar.xz │ │ ├── control.tar │ │ │ ├── ./control │ │ │ │ @@ -1,13 +1,13 @@ │ │ │ │ Package: yosys-doc │ │ │ │ Source: yosys │ │ │ │ Version: 0.52-1 │ │ │ │ Architecture: all │ │ │ │ Maintainer: Debian Electronics Team │ │ │ │ -Installed-Size: 3045 │ │ │ │ +Installed-Size: 3046 │ │ │ │ Suggests: yosys │ │ │ │ Section: doc │ │ │ │ Priority: optional │ │ │ │ Multi-Arch: foreign │ │ │ │ Homepage: https://github.com/YosysHQ/yosys │ │ │ │ Description: Framework for Verilog RTL synthesis (documentation) │ │ │ │ Yosys is a framework for Verilog RTL synthesis. It currently has extensive │ │ │ ├── ./md5sums │ │ │ │ ├── ./md5sums │ │ │ │ │┄ Files differ │ ├── data.tar.xz │ │ ├── data.tar │ │ │ ├── file list │ │ │ │ @@ -1,13 +1,13 @@ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/doc/ │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys/ │ │ │ │ --rw-r--r-- 0 root (0) root (0) 3060688 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys/yosyshqyosys.pdf │ │ │ │ +-rw-r--r-- 0 root (0) root (0) 3061202 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys/yosyshqyosys.pdf │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys-doc/ │ │ │ │ -rw-r--r-- 0 root (0) root (0) 2827 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys-doc/changelog.Debian.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 18593 2025-04-09 05:38:42.000000 ./usr/share/doc/yosys-doc/changelog.gz │ │ │ │ -rw-r--r-- 0 root (0) root (0) 23806 2025-04-11 08:32:04.000000 ./usr/share/doc/yosys-doc/copyright │ │ │ │ drwxr-xr-x 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/doc-base/ │ │ │ │ -rw-r--r-- 0 root (0) root (0) 245 2023-08-27 13:27:37.000000 ./usr/share/doc-base/yosys-doc.yosys-manual │ │ │ │ lrwxrwxrwx 0 root (0) root (0) 0 2025-04-11 08:41:09.000000 ./usr/share/doc/yosys/manual.pdf -> yosyshqyosys.pdf │ │ │ ├── ./usr/share/doc/yosys/yosyshqyosys.pdf │ │ │ │ ├── pdftotext {} - │ │ │ │ │ @@ -100,32 +100,32 @@ │ │ │ │ │ 4.2 Internal formats . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 155 │ │ │ │ │ 4.2.1 The RTL Intermediate Language (RTLIL) . . . . . . . . . . . . . . . . . . . . . . . . 156 │ │ │ │ │ 4.3 Working with the Yosys codebase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162 │ │ │ │ │ 4.3.1 Writing extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162 │ │ │ │ │ 4.3.2 Compiling with Verific library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171 │ │ │ │ │ 4.3.3 Writing a new backend using FunctionalIR . . . . . . . . . . . . . . . . . . . . . . . . 173 │ │ │ │ │ 4.3.4 Contributing to Yosys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186 │ │ │ │ │ -4.3.5 Testing Yosys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186 │ │ │ │ │ +4.3.5 Testing Yosys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 │ │ │ │ │ 4.4 Techmap by example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 │ │ │ │ │ -4.4.1 Mapping OR3X1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 187 │ │ │ │ │ +4.4.1 Mapping OR3X1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188 │ │ │ │ │ 4.4.2 Conditional techmap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 189 │ │ │ │ │ -4.4.3 Scripting in map modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190 │ │ │ │ │ +4.4.3 Scripting in map modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191 │ │ │ │ │ 4.4.4 Handling constant inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 192 │ │ │ │ │ -4.4.5 Handling shorted inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193 │ │ │ │ │ +4.4.5 Handling shorted inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194 │ │ │ │ │ 4.4.6 Notes on using techmap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195 │ │ │ │ │ -4.5 Notes on Verilog support in Yosys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195 │ │ │ │ │ -4.5.1 Unsupported Verilog-2005 Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195 │ │ │ │ │ -4.5.2 Verilog Attributes and non-standard features . . . . . . . . . . . . . . . . . . . . . . 195 │ │ │ │ │ -4.5.3 Non-standard or SystemVerilog features for formal verification . . . . . . . . . . . . . 199 │ │ │ │ │ +4.5 Notes on Verilog support in Yosys . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 │ │ │ │ │ +4.5.1 Unsupported Verilog-2005 Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 │ │ │ │ │ +4.5.2 Verilog Attributes and non-standard features . . . . . . . . . . . . . . . . . . . . . . 196 │ │ │ │ │ +4.5.3 Non-standard or SystemVerilog features for formal verification . . . . . . . . . . . . . 200 │ │ │ │ │ 4.5.4 Supported features from SystemVerilog . . . . . . . . . . . . . . . . . . . . . . . . . . 200 │ │ │ │ │ -4.6 Hashing and associative data structures in Yosys . . . . . . . . . . . . . . . . . . . . . . . . . 200 │ │ │ │ │ -4.6.1 Container classes based on hashing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 200 │ │ │ │ │ -4.6.2 The hash function . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201 │ │ │ │ │ +4.6 Hashing and associative data structures in Yosys . . . . . . . . . . . . . . . . . . . . . . . . . 201 │ │ │ │ │ +4.6.1 Container classes based on hashing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201 │ │ │ │ │ +4.6.2 The hash function . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 │ │ │ │ │ 4.6.3 Making a type hashable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202 │ │ │ │ │ -4.6.4 Porting plugins from the legacy interface . . . . . . . . . . . . . . . . . . . . . . . . . 202 │ │ │ │ │ +4.6.4 Porting plugins from the legacy interface . . . . . . . . . . . . . . . . . . . . . . . . . 203 │ │ │ │ │ │ │ │ │ │ 5 │ │ │ │ │ │ │ │ │ │ A primer on digital circuit synthesis │ │ │ │ │ 205 │ │ │ │ │ 5.1 Levels of abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 │ │ │ │ │ 5.1.1 System level . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 206 │ │ │ │ │ @@ -198,372 +198,372 @@ │ │ │ │ │ 8 │ │ │ │ │ │ │ │ │ │ Auxiliary programs │ │ │ │ │ 225 │ │ │ │ │ 8.1 yosys-config . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 225 │ │ │ │ │ 8.2 yosys-filterlib . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 │ │ │ │ │ 8.3 yosys-abc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 │ │ │ │ │ -8.4 yosys-smtbmc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226 │ │ │ │ │ +8.4 yosys-smtbmc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 227 │ │ │ │ │ 8.5 yosys-witness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 230 │ │ │ │ │ │ │ │ │ │ 9 │ │ │ │ │ │ │ │ │ │ Internal cell library │ │ │ │ │ -231 │ │ │ │ │ -9.1 Word-level cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231 │ │ │ │ │ -9.1.1 Unary operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 231 │ │ │ │ │ -9.1.2 Binary operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 237 │ │ │ │ │ -9.1.3 Multiplexers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257 │ │ │ │ │ -9.1.4 Registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 261 │ │ │ │ │ -9.1.5 Memories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271 │ │ │ │ │ -9.1.6 Finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 283 │ │ │ │ │ -9.1.7 Coarse arithmetics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 285 │ │ │ │ │ -9.1.8 Arbitrary logic functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293 │ │ │ │ │ -9.1.9 Specify rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 295 │ │ │ │ │ +233 │ │ │ │ │ +9.1 Word-level cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233 │ │ │ │ │ +9.1.1 Unary operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 233 │ │ │ │ │ +9.1.2 Binary operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 239 │ │ │ │ │ +9.1.3 Multiplexers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259 │ │ │ │ │ +9.1.4 Registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 263 │ │ │ │ │ +9.1.5 Memories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 273 │ │ │ │ │ +9.1.6 Finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 285 │ │ │ │ │ +9.1.7 Coarse arithmetics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 287 │ │ │ │ │ +9.1.8 Arbitrary logic functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 295 │ │ │ │ │ +9.1.9 Specify rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 297 │ │ │ │ │ iii │ │ │ │ │ │ │ │ │ │ 9.2 │ │ │ │ │ │ │ │ │ │ 9.3 │ │ │ │ │ │ │ │ │ │ -9.1.10 Formal verification cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 300 │ │ │ │ │ -9.1.11 Debugging cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 306 │ │ │ │ │ -9.1.12 Wire cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 309 │ │ │ │ │ -Gate-level cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 310 │ │ │ │ │ -9.2.1 Combinatorial cells (simple) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311 │ │ │ │ │ -9.2.2 Combinatorial cells (combined) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 315 │ │ │ │ │ -9.2.3 Flip-flop cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 321 │ │ │ │ │ -9.2.4 Latch cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 375 │ │ │ │ │ -9.2.5 Other gate-level cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 387 │ │ │ │ │ -Cell properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 388 │ │ │ │ │ +9.1.10 Formal verification cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 302 │ │ │ │ │ +9.1.11 Debugging cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 308 │ │ │ │ │ +9.1.12 Wire cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 311 │ │ │ │ │ +Gate-level cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 312 │ │ │ │ │ +9.2.1 Combinatorial cells (simple) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 313 │ │ │ │ │ +9.2.2 Combinatorial cells (combined) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 317 │ │ │ │ │ +9.2.3 Flip-flop cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 323 │ │ │ │ │ +9.2.4 Latch cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 377 │ │ │ │ │ +9.2.5 Other gate-level cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 389 │ │ │ │ │ +Cell properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 390 │ │ │ │ │ │ │ │ │ │ 10 Command line reference │ │ │ │ │ -389 │ │ │ │ │ -10.1 Yosys environment variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 390 │ │ │ │ │ -10.2 abc - use ABC for technology mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 391 │ │ │ │ │ -10.3 abc9 - use ABC9 for technology mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 394 │ │ │ │ │ -10.4 abc9_exe - use ABC9 for technology mapping . . . . . . . . . . . . . . . . . . . . . . . . . . 397 │ │ │ │ │ -10.5 abc9_ops - helper functions for ABC9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 399 │ │ │ │ │ -10.6 abc_new - (experimental) use ABC for SC technology mapping (new) . . . . . . . . . . . . . 401 │ │ │ │ │ -10.7 abstract - replace signals with abstract values during formal verification . . . . . . . . . . . . 402 │ │ │ │ │ -10.8 add - add objects to the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 403 │ │ │ │ │ -10.9 aigmap - map logic to and-inverter-graph circuit . . . . . . . . . . . . . . . . . . . . . . . . . 404 │ │ │ │ │ -10.10 alumacc - extract ALU and MACC cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 404 │ │ │ │ │ -10.11 anlogic_eqn - Anlogic: Calculate equations for luts . . . . . . . . . . . . . . . . . . . . . . . 404 │ │ │ │ │ -10.12 anlogic_fixcarry - Anlogic: fix carry chain . . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 │ │ │ │ │ -10.13 assertpmux - adds asserts for parallel muxes . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 │ │ │ │ │ -10.14 async2sync - convert async FF inputs to sync circuits . . . . . . . . . . . . . . . . . . . . . . 405 │ │ │ │ │ -10.15 attrmap - renaming attributes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 │ │ │ │ │ -10.16 attrmvcp - move or copy attributes from wires to driving cells . . . . . . . . . . . . . . . . . 406 │ │ │ │ │ -10.17 autoname - automatically assign names to objects . . . . . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ -10.18 blackbox - convert modules into blackbox modules . . . . . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ -10.19 bmuxmap - transform $bmux cells to trees of $mux cells . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ -10.20 booth - map $mul cells to Booth multipliers . . . . . . . . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ -10.21 box_derive - derive box modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 408 │ │ │ │ │ -10.22 bufnorm - (experimental) convert design into buffered-normalized form . . . . . . . . . . . . 408 │ │ │ │ │ -10.23 bugpoint - minimize testcases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410 │ │ │ │ │ -10.24 bwmuxmap - replace $bwmux cells with equivalent logic . . . . . . . . . . . . . . . . . . . . . 411 │ │ │ │ │ -10.25 cd - a shortcut for ‘select -module ’ . . . . . . . . . . . . . . . . . . . . . . . . . . . 411 │ │ │ │ │ -10.26 cellmatch - match cells to their targets in cell library . . . . . . . . . . . . . . . . . . . . . . 412 │ │ │ │ │ -10.27 check - check for obvious problems in the design . . . . . . . . . . . . . . . . . . . . . . . . . 412 │ │ │ │ │ -10.28 chformal - change formal constraints of the design . . . . . . . . . . . . . . . . . . . . . . . . 413 │ │ │ │ │ -10.29 chparam - re-evaluate modules with new parameters . . . . . . . . . . . . . . . . . . . . . . . 414 │ │ │ │ │ -10.30 chtype - change type of cells in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 414 │ │ │ │ │ -10.31 clean - remove unused cells and wires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 414 │ │ │ │ │ -10.32 clean_zerowidth - clean zero-width connections from the design . . . . . . . . . . . . . . . . 415 │ │ │ │ │ -10.33 clk2fflogic - convert clocked FFs to generic $ff cells . . . . . . . . . . . . . . . . . . . . . . . . 415 │ │ │ │ │ -10.34 clkbufmap - insert clock buffers on clock networks . . . . . . . . . . . . . . . . . . . . . . . . 415 │ │ │ │ │ -10.35 clockgate - extract clock gating out of flip flops . . . . . . . . . . . . . . . . . . . . . . . . . . 416 │ │ │ │ │ -10.36 connect - create or remove connections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 417 │ │ │ │ │ -10.37 connect_rpc - connect to RPC frontend . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 417 │ │ │ │ │ -10.38 connwrappers - match width of input-output port pairs . . . . . . . . . . . . . . . . . . . . . 418 │ │ │ │ │ -10.39 coolrunner2_fixup - insert necessary buffer cells for CoolRunner-II architecture . . . . . . . . 419 │ │ │ │ │ -10.40 coolrunner2_sop - break $sop cells into ANDTERM/ORTERM cells . . . . . . . . . . . . . . 419 │ │ │ │ │ -10.41 copy - copy modules in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419 │ │ │ │ │ -10.42 cover - print code coverage counters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419 │ │ │ │ │ +391 │ │ │ │ │ +10.1 Yosys environment variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 392 │ │ │ │ │ +10.2 abc - use ABC for technology mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 393 │ │ │ │ │ +10.3 abc9 - use ABC9 for technology mapping . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 396 │ │ │ │ │ +10.4 abc9_exe - use ABC9 for technology mapping . . . . . . . . . . . . . . . . . . . . . . . . . . 399 │ │ │ │ │ +10.5 abc9_ops - helper functions for ABC9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401 │ │ │ │ │ +10.6 abc_new - (experimental) use ABC for SC technology mapping (new) . . . . . . . . . . . . . 403 │ │ │ │ │ +10.7 abstract - replace signals with abstract values during formal verification . . . . . . . . . . . . 404 │ │ │ │ │ +10.8 add - add objects to the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 │ │ │ │ │ +10.9 aigmap - map logic to and-inverter-graph circuit . . . . . . . . . . . . . . . . . . . . . . . . . 406 │ │ │ │ │ +10.10 alumacc - extract ALU and MACC cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 406 │ │ │ │ │ +10.11 anlogic_eqn - Anlogic: Calculate equations for luts . . . . . . . . . . . . . . . . . . . . . . . 406 │ │ │ │ │ +10.12 anlogic_fixcarry - Anlogic: fix carry chain . . . . . . . . . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ +10.13 assertpmux - adds asserts for parallel muxes . . . . . . . . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ +10.14 async2sync - convert async FF inputs to sync circuits . . . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ +10.15 attrmap - renaming attributes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 407 │ │ │ │ │ +10.16 attrmvcp - move or copy attributes from wires to driving cells . . . . . . . . . . . . . . . . . 408 │ │ │ │ │ +10.17 autoname - automatically assign names to objects . . . . . . . . . . . . . . . . . . . . . . . . 409 │ │ │ │ │ +10.18 blackbox - convert modules into blackbox modules . . . . . . . . . . . . . . . . . . . . . . . . 409 │ │ │ │ │ +10.19 bmuxmap - transform $bmux cells to trees of $mux cells . . . . . . . . . . . . . . . . . . . . 409 │ │ │ │ │ +10.20 booth - map $mul cells to Booth multipliers . . . . . . . . . . . . . . . . . . . . . . . . . . . 409 │ │ │ │ │ +10.21 box_derive - derive box modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410 │ │ │ │ │ +10.22 bufnorm - (experimental) convert design into buffered-normalized form . . . . . . . . . . . . 410 │ │ │ │ │ +10.23 bugpoint - minimize testcases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 412 │ │ │ │ │ +10.24 bwmuxmap - replace $bwmux cells with equivalent logic . . . . . . . . . . . . . . . . . . . . . 413 │ │ │ │ │ +10.25 cd - a shortcut for ‘select -module ’ . . . . . . . . . . . . . . . . . . . . . . . . . . . 413 │ │ │ │ │ +10.26 cellmatch - match cells to their targets in cell library . . . . . . . . . . . . . . . . . . . . . . 414 │ │ │ │ │ +10.27 check - check for obvious problems in the design . . . . . . . . . . . . . . . . . . . . . . . . . 414 │ │ │ │ │ +10.28 chformal - change formal constraints of the design . . . . . . . . . . . . . . . . . . . . . . . . 415 │ │ │ │ │ +10.29 chparam - re-evaluate modules with new parameters . . . . . . . . . . . . . . . . . . . . . . . 416 │ │ │ │ │ +10.30 chtype - change type of cells in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 416 │ │ │ │ │ +10.31 clean - remove unused cells and wires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 416 │ │ │ │ │ +10.32 clean_zerowidth - clean zero-width connections from the design . . . . . . . . . . . . . . . . 417 │ │ │ │ │ +10.33 clk2fflogic - convert clocked FFs to generic $ff cells . . . . . . . . . . . . . . . . . . . . . . . . 417 │ │ │ │ │ +10.34 clkbufmap - insert clock buffers on clock networks . . . . . . . . . . . . . . . . . . . . . . . . 417 │ │ │ │ │ +10.35 clockgate - extract clock gating out of flip flops . . . . . . . . . . . . . . . . . . . . . . . . . . 418 │ │ │ │ │ +10.36 connect - create or remove connections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419 │ │ │ │ │ +10.37 connect_rpc - connect to RPC frontend . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 419 │ │ │ │ │ +10.38 connwrappers - match width of input-output port pairs . . . . . . . . . . . . . . . . . . . . . 420 │ │ │ │ │ +10.39 coolrunner2_fixup - insert necessary buffer cells for CoolRunner-II architecture . . . . . . . . 421 │ │ │ │ │ +10.40 coolrunner2_sop - break $sop cells into ANDTERM/ORTERM cells . . . . . . . . . . . . . . 421 │ │ │ │ │ +10.41 copy - copy modules in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 │ │ │ │ │ +10.42 cover - print code coverage counters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 │ │ │ │ │ │ │ │ │ │ iv │ │ │ │ │ │ │ │ │ │ - 10.43 cutpoint - adds formal cut points to the design . . . . . . . . . . . . . . . . . . . . . . . . . . 420 │ │ │ │ │ -10.44 debug - run command with debug log messages enabled . . . . . . . . . . . . . . . . . . . . . 420 │ │ │ │ │ -10.45 delete - delete objects in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 │ │ │ │ │ -10.46 deminout - demote inout ports to input or output . . . . . . . . . . . . . . . . . . . . . . . . 421 │ │ │ │ │ -10.47 demuxmap - transform $demux cells to $eq + $mux cells . . . . . . . . . . . . . . . . . . . . 421 │ │ │ │ │ -10.48 design - save, restore and reset current design . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 │ │ │ │ │ -10.49 dffinit - set INIT param on FF cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 423 │ │ │ │ │ -10.50 dfflegalize - convert FFs to types supported by the target . . . . . . . . . . . . . . . . . . . . 423 │ │ │ │ │ -10.51 dfflibmap - technology mapping of flip-flops . . . . . . . . . . . . . . . . . . . . . . . . . . . . 424 │ │ │ │ │ -10.52 dffunmap - unmap clock enable and synchronous reset from FFs . . . . . . . . . . . . . . . . 425 │ │ │ │ │ -10.53 dft_tag - create tagging logic for data flow tracking . . . . . . . . . . . . . . . . . . . . . . . 425 │ │ │ │ │ -10.54 dump - print parts of the design in RTLIL format . . . . . . . . . . . . . . . . . . . . . . . . 426 │ │ │ │ │ -10.55 echo - turning echoing back of commands on and off . . . . . . . . . . . . . . . . . . . . . . . 426 │ │ │ │ │ -10.56 edgetypes - list all types of edges in selection . . . . . . . . . . . . . . . . . . . . . . . . . . . 426 │ │ │ │ │ -10.57 efinix_fixcarry - Efinix: fix carry chain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427 │ │ │ │ │ -10.58 equiv_add - add a $equiv cell . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427 │ │ │ │ │ -10.59 equiv_induct - proving $equiv cells using temporal induction . . . . . . . . . . . . . . . . . . 427 │ │ │ │ │ -10.60 equiv_make - prepare a circuit for equivalence checking . . . . . . . . . . . . . . . . . . . . . 428 │ │ │ │ │ -10.61 equiv_mark - mark equivalence checking regions . . . . . . . . . . . . . . . . . . . . . . . . . 428 │ │ │ │ │ -10.62 equiv_miter - extract miter from equiv circuit . . . . . . . . . . . . . . . . . . . . . . . . . . 428 │ │ │ │ │ -10.63 equiv_opt - prove equivalence for optimized circuit . . . . . . . . . . . . . . . . . . . . . . . 429 │ │ │ │ │ -10.64 equiv_purge - purge equivalence checking module . . . . . . . . . . . . . . . . . . . . . . . . 430 │ │ │ │ │ -10.65 equiv_remove - remove $equiv cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 430 │ │ │ │ │ -10.66 equiv_simple - try proving simple $equiv instances . . . . . . . . . . . . . . . . . . . . . . . 431 │ │ │ │ │ -10.67 equiv_status - print status of equivalent checking module . . . . . . . . . . . . . . . . . . . . 431 │ │ │ │ │ -10.68 equiv_struct - structural equivalence checking . . . . . . . . . . . . . . . . . . . . . . . . . . 431 │ │ │ │ │ -10.69 eval - evaluate the circuit given an input . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 432 │ │ │ │ │ -10.70 example_dt - drivertools example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 432 │ │ │ │ │ -10.71 exec - execute commands in the operating system shell . . . . . . . . . . . . . . . . . . . . . 433 │ │ │ │ │ -10.72 expose - convert internal signals to module ports . . . . . . . . . . . . . . . . . . . . . . . . . 433 │ │ │ │ │ -10.73 extract - find subcircuits and replace them with cells . . . . . . . . . . . . . . . . . . . . . . 434 │ │ │ │ │ -10.74 extract_counter - Extract GreenPak4 counter cells . . . . . . . . . . . . . . . . . . . . . . . . 436 │ │ │ │ │ -10.75 extract_fa - find and extract full/half adders . . . . . . . . . . . . . . . . . . . . . . . . . . . 436 │ │ │ │ │ -10.76 extract_reduce - converts gate chains into $reduce_* cells . . . . . . . . . . . . . . . . . . . 437 │ │ │ │ │ -10.77 extractinv - extract explicit inverter cells for invertible cell pins . . . . . . . . . . . . . . . . . 437 │ │ │ │ │ -10.78 flatten - flatten design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 437 │ │ │ │ │ -10.79 flowmap - pack LUTs with FlowMap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 438 │ │ │ │ │ -10.80 fmcombine - combine two instances of a cell into one . . . . . . . . . . . . . . . . . . . . . . . 439 │ │ │ │ │ -10.81 fminit - set init values/sequences for formal . . . . . . . . . . . . . . . . . . . . . . . . . . . . 440 │ │ │ │ │ -10.82 formalff - prepare FFs for formal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 440 │ │ │ │ │ -10.83 freduce - perform functional reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 441 │ │ │ │ │ -10.84 fsm - extract and optimize finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . 442 │ │ │ │ │ -10.85 fsm_detect - finding FSMs in design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 442 │ │ │ │ │ -10.86 fsm_expand - expand FSM cells by merging logic into it . . . . . . . . . . . . . . . . . . . . 443 │ │ │ │ │ -10.87 fsm_export - exporting FSMs to KISS2 files . . . . . . . . . . . . . . . . . . . . . . . . . . . 443 │ │ │ │ │ -10.88 fsm_extract - extracting FSMs in design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 444 │ │ │ │ │ -10.89 fsm_info - print information on finite state machines . . . . . . . . . . . . . . . . . . . . . . 444 │ │ │ │ │ -10.90 fsm_map - mapping FSMs to basic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 444 │ │ │ │ │ -10.91 fsm_opt - optimize finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 444 │ │ │ │ │ -10.92 fsm_recode - recoding finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . 444 │ │ │ │ │ -10.93 fst2tb - generate testbench out of fst file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 445 │ │ │ │ │ -10.94 future - resolve future sampled value functions . . . . . . . . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ -10.95 gatemate_foldinv - fold inverters into Gatemate LUT trees . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ -10.96 glift - create GLIFT models and optimization problems . . . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ + 10.43 cutpoint - adds formal cut points to the design . . . . . . . . . . . . . . . . . . . . . . . . . . 422 │ │ │ │ │ +10.44 debug - run command with debug log messages enabled . . . . . . . . . . . . . . . . . . . . . 422 │ │ │ │ │ +10.45 delete - delete objects in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 423 │ │ │ │ │ +10.46 deminout - demote inout ports to input or output . . . . . . . . . . . . . . . . . . . . . . . . 423 │ │ │ │ │ +10.47 demuxmap - transform $demux cells to $eq + $mux cells . . . . . . . . . . . . . . . . . . . . 423 │ │ │ │ │ +10.48 design - save, restore and reset current design . . . . . . . . . . . . . . . . . . . . . . . . . . . 423 │ │ │ │ │ +10.49 dffinit - set INIT param on FF cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 425 │ │ │ │ │ +10.50 dfflegalize - convert FFs to types supported by the target . . . . . . . . . . . . . . . . . . . . 425 │ │ │ │ │ +10.51 dfflibmap - technology mapping of flip-flops . . . . . . . . . . . . . . . . . . . . . . . . . . . . 426 │ │ │ │ │ +10.52 dffunmap - unmap clock enable and synchronous reset from FFs . . . . . . . . . . . . . . . . 427 │ │ │ │ │ +10.53 dft_tag - create tagging logic for data flow tracking . . . . . . . . . . . . . . . . . . . . . . . 427 │ │ │ │ │ +10.54 dump - print parts of the design in RTLIL format . . . . . . . . . . . . . . . . . . . . . . . . 428 │ │ │ │ │ +10.55 echo - turning echoing back of commands on and off . . . . . . . . . . . . . . . . . . . . . . . 428 │ │ │ │ │ +10.56 edgetypes - list all types of edges in selection . . . . . . . . . . . . . . . . . . . . . . . . . . . 428 │ │ │ │ │ +10.57 efinix_fixcarry - Efinix: fix carry chain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 429 │ │ │ │ │ +10.58 equiv_add - add a $equiv cell . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 429 │ │ │ │ │ +10.59 equiv_induct - proving $equiv cells using temporal induction . . . . . . . . . . . . . . . . . . 429 │ │ │ │ │ +10.60 equiv_make - prepare a circuit for equivalence checking . . . . . . . . . . . . . . . . . . . . . 430 │ │ │ │ │ +10.61 equiv_mark - mark equivalence checking regions . . . . . . . . . . . . . . . . . . . . . . . . . 430 │ │ │ │ │ +10.62 equiv_miter - extract miter from equiv circuit . . . . . . . . . . . . . . . . . . . . . . . . . . 430 │ │ │ │ │ +10.63 equiv_opt - prove equivalence for optimized circuit . . . . . . . . . . . . . . . . . . . . . . . 431 │ │ │ │ │ +10.64 equiv_purge - purge equivalence checking module . . . . . . . . . . . . . . . . . . . . . . . . 432 │ │ │ │ │ +10.65 equiv_remove - remove $equiv cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 432 │ │ │ │ │ +10.66 equiv_simple - try proving simple $equiv instances . . . . . . . . . . . . . . . . . . . . . . . 433 │ │ │ │ │ +10.67 equiv_status - print status of equivalent checking module . . . . . . . . . . . . . . . . . . . . 433 │ │ │ │ │ +10.68 equiv_struct - structural equivalence checking . . . . . . . . . . . . . . . . . . . . . . . . . . 433 │ │ │ │ │ +10.69 eval - evaluate the circuit given an input . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 434 │ │ │ │ │ +10.70 example_dt - drivertools example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 434 │ │ │ │ │ +10.71 exec - execute commands in the operating system shell . . . . . . . . . . . . . . . . . . . . . 435 │ │ │ │ │ +10.72 expose - convert internal signals to module ports . . . . . . . . . . . . . . . . . . . . . . . . . 435 │ │ │ │ │ +10.73 extract - find subcircuits and replace them with cells . . . . . . . . . . . . . . . . . . . . . . 436 │ │ │ │ │ +10.74 extract_counter - Extract GreenPak4 counter cells . . . . . . . . . . . . . . . . . . . . . . . . 438 │ │ │ │ │ +10.75 extract_fa - find and extract full/half adders . . . . . . . . . . . . . . . . . . . . . . . . . . . 438 │ │ │ │ │ +10.76 extract_reduce - converts gate chains into $reduce_* cells . . . . . . . . . . . . . . . . . . . 439 │ │ │ │ │ +10.77 extractinv - extract explicit inverter cells for invertible cell pins . . . . . . . . . . . . . . . . . 439 │ │ │ │ │ +10.78 flatten - flatten design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 439 │ │ │ │ │ +10.79 flowmap - pack LUTs with FlowMap . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 440 │ │ │ │ │ +10.80 fmcombine - combine two instances of a cell into one . . . . . . . . . . . . . . . . . . . . . . . 441 │ │ │ │ │ +10.81 fminit - set init values/sequences for formal . . . . . . . . . . . . . . . . . . . . . . . . . . . . 442 │ │ │ │ │ +10.82 formalff - prepare FFs for formal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 442 │ │ │ │ │ +10.83 freduce - perform functional reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 443 │ │ │ │ │ +10.84 fsm - extract and optimize finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . 444 │ │ │ │ │ +10.85 fsm_detect - finding FSMs in design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 444 │ │ │ │ │ +10.86 fsm_expand - expand FSM cells by merging logic into it . . . . . . . . . . . . . . . . . . . . 445 │ │ │ │ │ +10.87 fsm_export - exporting FSMs to KISS2 files . . . . . . . . . . . . . . . . . . . . . . . . . . . 445 │ │ │ │ │ +10.88 fsm_extract - extracting FSMs in design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ +10.89 fsm_info - print information on finite state machines . . . . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ +10.90 fsm_map - mapping FSMs to basic logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ +10.91 fsm_opt - optimize finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ +10.92 fsm_recode - recoding finite state machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . 446 │ │ │ │ │ +10.93 fst2tb - generate testbench out of fst file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 447 │ │ │ │ │ +10.94 future - resolve future sampled value functions . . . . . . . . . . . . . . . . . . . . . . . . . . 448 │ │ │ │ │ +10.95 gatemate_foldinv - fold inverters into Gatemate LUT trees . . . . . . . . . . . . . . . . . . . 448 │ │ │ │ │ +10.96 glift - create GLIFT models and optimization problems . . . . . . . . . . . . . . . . . . . . . 448 │ │ │ │ │ │ │ │ │ │ v │ │ │ │ │ │ │ │ │ │ - 10.97 greenpak4_dffinv - merge greenpak4 inverters and DFF/latches . . . . . . . . . . . . . . . . 448 │ │ │ │ │ -10.98 help - display help messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 448 │ │ │ │ │ -10.99 hierarchy - check, expand and clean up design hierarchy . . . . . . . . . . . . . . . . . . . . . 448 │ │ │ │ │ -10.100hilomap - technology mapping of constant hi- and/or lo-drivers . . . . . . . . . . . . . . . . . 450 │ │ │ │ │ -10.101history - show last interactive commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 450 │ │ │ │ │ -10.102ice40_braminit - iCE40: perform SB_RAM40_4K initialization from file . . . . . . . . . . . 450 │ │ │ │ │ -10.103ice40_dsp - iCE40: map multipliers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 451 │ │ │ │ │ -10.104ice40_opt - iCE40: perform simple optimizations . . . . . . . . . . . . . . . . . . . . . . . . . 451 │ │ │ │ │ -10.105ice40_wrapcarry - iCE40: wrap carries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 451 │ │ │ │ │ -10.106insbuf - insert buffer cells for connected wires . . . . . . . . . . . . . . . . . . . . . . . . . . . 452 │ │ │ │ │ -10.107internal_stats - print internal statistics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 452 │ │ │ │ │ -10.108iopadmap - technology mapping of i/o pads (or buffers) . . . . . . . . . . . . . . . . . . . . . 452 │ │ │ │ │ -10.109jny - write design and metadata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453 │ │ │ │ │ -10.110json - write design in JSON format . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453 │ │ │ │ │ -10.111keep_hierarchy - selectively add the keep_hierarchy attribute . . . . . . . . . . . . . . . . . 454 │ │ │ │ │ -10.112lattice_gsr - Lattice: handle GSR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 454 │ │ │ │ │ -10.113libcache - control caching of technology library data parsed from liberty files . . . . . . . . . 455 │ │ │ │ │ -10.114license - print license terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 455 │ │ │ │ │ -10.115log - print text and log files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 456 │ │ │ │ │ -10.116logger - set logger properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 456 │ │ │ │ │ -10.117ls - list modules or objects in modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 457 │ │ │ │ │ -10.118ltp - print longest topological path . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 457 │ │ │ │ │ -10.119lut2mux - convert $lut to $_MUX_ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 458 │ │ │ │ │ -10.120maccmap - mapping macc cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 458 │ │ │ │ │ -10.121memory - translate memories to basic cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . 458 │ │ │ │ │ -10.122memory_bmux2rom - convert muxes to ROMs . . . . . . . . . . . . . . . . . . . . . . . . . . 458 │ │ │ │ │ -10.123memory_bram - map memories to block rams . . . . . . . . . . . . . . . . . . . . . . . . . . 459 │ │ │ │ │ -10.124memory_collect - creating multi-port memory cells . . . . . . . . . . . . . . . . . . . . . . . 461 │ │ │ │ │ -10.125memory_dff - merge input/output DFFs into memory read ports . . . . . . . . . . . . . . . 461 │ │ │ │ │ -10.126memory_libmap - map memories to cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 461 │ │ │ │ │ -10.127memory_map - translate multiport memories to basic cells . . . . . . . . . . . . . . . . . . . 462 │ │ │ │ │ -10.128memory_memx - emulate vlog sim behavior for mem ports . . . . . . . . . . . . . . . . . . . 462 │ │ │ │ │ -10.129memory_narrow - split up wide memory ports . . . . . . . . . . . . . . . . . . . . . . . . . . 463 │ │ │ │ │ -10.130memory_nordff - extract read port FFs from memories . . . . . . . . . . . . . . . . . . . . . 463 │ │ │ │ │ -10.131memory_share - consolidate memory ports . . . . . . . . . . . . . . . . . . . . . . . . . . . . 463 │ │ │ │ │ -10.132memory_unpack - unpack multi-port memory cells . . . . . . . . . . . . . . . . . . . . . . . 463 │ │ │ │ │ -10.133microchip_dffopt - MICROCHIP: optimize FF control signal usage . . . . . . . . . . . . . . 464 │ │ │ │ │ -10.134microchip_dsp - MICROCHIP: pack resources into DSPs . . . . . . . . . . . . . . . . . . . . 464 │ │ │ │ │ -10.135miter - automatically create a miter circuit . . . . . . . . . . . . . . . . . . . . . . . . . . . . 464 │ │ │ │ │ -10.136mutate - generate or apply design mutations . . . . . . . . . . . . . . . . . . . . . . . . . . . 465 │ │ │ │ │ -10.137muxcover - cover trees of MUX cells with wider MUXes . . . . . . . . . . . . . . . . . . . . . 467 │ │ │ │ │ -10.138muxpack - $mux/$pmux cascades to $pmux . . . . . . . . . . . . . . . . . . . . . . . . . . . 467 │ │ │ │ │ -10.139nlutmap - map to LUTs of different sizes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 468 │ │ │ │ │ -10.140nx_carry - NanoXplore: create carry cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 468 │ │ │ │ │ -10.141onehot - optimize $eq cells for onehot signals . . . . . . . . . . . . . . . . . . . . . . . . . . . 468 │ │ │ │ │ -10.142opt - perform simple optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 468 │ │ │ │ │ -10.143opt_clean - remove unused cells and wires . . . . . . . . . . . . . . . . . . . . . . . . . . . . 469 │ │ │ │ │ -10.144opt_demorgan - Optimize reductions with DeMorgan equivalents . . . . . . . . . . . . . . . 469 │ │ │ │ │ -10.145opt_dff - perform DFF optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 470 │ │ │ │ │ -10.146opt_expr - perform const folding and simple expression rewriting . . . . . . . . . . . . . . . 470 │ │ │ │ │ -10.147opt_ffinv - push inverters through FFs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 471 │ │ │ │ │ -10.148opt_lut - optimize LUT cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 471 │ │ │ │ │ -10.149opt_lut_ins - discard unused LUT inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 471 │ │ │ │ │ -10.150opt_mem - optimize memories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 472 │ │ │ │ │ + 10.97 greenpak4_dffinv - merge greenpak4 inverters and DFF/latches . . . . . . . . . . . . . . . . 450 │ │ │ │ │ +10.98 help - display help messages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 450 │ │ │ │ │ +10.99 hierarchy - check, expand and clean up design hierarchy . . . . . . . . . . . . . . . . . . . . . 450 │ │ │ │ │ +10.100hilomap - technology mapping of constant hi- and/or lo-drivers . . . . . . . . . . . . . . . . . 452 │ │ │ │ │ +10.101history - show last interactive commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 452 │ │ │ │ │ +10.102ice40_braminit - iCE40: perform SB_RAM40_4K initialization from file . . . . . . . . . . . 452 │ │ │ │ │ +10.103ice40_dsp - iCE40: map multipliers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453 │ │ │ │ │ +10.104ice40_opt - iCE40: perform simple optimizations . . . . . . . . . . . . . . . . . . . . . . . . . 453 │ │ │ │ │ +10.105ice40_wrapcarry - iCE40: wrap carries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 453 │ │ │ │ │ +10.106insbuf - insert buffer cells for connected wires . . . . . . . . . . . . . . . . . . . . . . . . . . . 454 │ │ │ │ │ +10.107internal_stats - print internal statistics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 454 │ │ │ │ │ +10.108iopadmap - technology mapping of i/o pads (or buffers) . . . . . . . . . . . . . . . . . . . . . 454 │ │ │ │ │ +10.109jny - write design and metadata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 455 │ │ │ │ │ +10.110json - write design in JSON format . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 455 │ │ │ │ │ +10.111keep_hierarchy - selectively add the keep_hierarchy attribute . . . . . . . . . . . . . . . . . 456 │ │ │ │ │ +10.112lattice_gsr - Lattice: handle GSR . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 456 │ │ │ │ │ +10.113libcache - control caching of technology library data parsed from liberty files . . . . . . . . . 457 │ │ │ │ │ +10.114license - print license terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 457 │ │ │ │ │ +10.115log - print text and log files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 458 │ │ │ │ │ +10.116logger - set logger properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 458 │ │ │ │ │ +10.117ls - list modules or objects in modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 459 │ │ │ │ │ +10.118ltp - print longest topological path . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 459 │ │ │ │ │ +10.119lut2mux - convert $lut to $_MUX_ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 460 │ │ │ │ │ +10.120maccmap - mapping macc cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 460 │ │ │ │ │ +10.121memory - translate memories to basic cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . 460 │ │ │ │ │ +10.122memory_bmux2rom - convert muxes to ROMs . . . . . . . . . . . . . . . . . . . . . . . . . . 460 │ │ │ │ │ +10.123memory_bram - map memories to block rams . . . . . . . . . . . . . . . . . . . . . . . . . . 461 │ │ │ │ │ +10.124memory_collect - creating multi-port memory cells . . . . . . . . . . . . . . . . . . . . . . . 463 │ │ │ │ │ +10.125memory_dff - merge input/output DFFs into memory read ports . . . . . . . . . . . . . . . 463 │ │ │ │ │ +10.126memory_libmap - map memories to cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 463 │ │ │ │ │ +10.127memory_map - translate multiport memories to basic cells . . . . . . . . . . . . . . . . . . . 464 │ │ │ │ │ +10.128memory_memx - emulate vlog sim behavior for mem ports . . . . . . . . . . . . . . . . . . . 464 │ │ │ │ │ +10.129memory_narrow - split up wide memory ports . . . . . . . . . . . . . . . . . . . . . . . . . . 465 │ │ │ │ │ +10.130memory_nordff - extract read port FFs from memories . . . . . . . . . . . . . . . . . . . . . 465 │ │ │ │ │ +10.131memory_share - consolidate memory ports . . . . . . . . . . . . . . . . . . . . . . . . . . . . 465 │ │ │ │ │ +10.132memory_unpack - unpack multi-port memory cells . . . . . . . . . . . . . . . . . . . . . . . 465 │ │ │ │ │ +10.133microchip_dffopt - MICROCHIP: optimize FF control signal usage . . . . . . . . . . . . . . 466 │ │ │ │ │ +10.134microchip_dsp - MICROCHIP: pack resources into DSPs . . . . . . . . . . . . . . . . . . . . 466 │ │ │ │ │ +10.135miter - automatically create a miter circuit . . . . . . . . . . . . . . . . . . . . . . . . . . . . 466 │ │ │ │ │ +10.136mutate - generate or apply design mutations . . . . . . . . . . . . . . . . . . . . . . . . . . . 467 │ │ │ │ │ +10.137muxcover - cover trees of MUX cells with wider MUXes . . . . . . . . . . . . . . . . . . . . . 469 │ │ │ │ │ +10.138muxpack - $mux/$pmux cascades to $pmux . . . . . . . . . . . . . . . . . . . . . . . . . . . 469 │ │ │ │ │ +10.139nlutmap - map to LUTs of different sizes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 470 │ │ │ │ │ +10.140nx_carry - NanoXplore: create carry cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 470 │ │ │ │ │ +10.141onehot - optimize $eq cells for onehot signals . . . . . . . . . . . . . . . . . . . . . . . . . . . 470 │ │ │ │ │ +10.142opt - perform simple optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 470 │ │ │ │ │ +10.143opt_clean - remove unused cells and wires . . . . . . . . . . . . . . . . . . . . . . . . . . . . 471 │ │ │ │ │ +10.144opt_demorgan - Optimize reductions with DeMorgan equivalents . . . . . . . . . . . . . . . 471 │ │ │ │ │ +10.145opt_dff - perform DFF optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 472 │ │ │ │ │ +10.146opt_expr - perform const folding and simple expression rewriting . . . . . . . . . . . . . . . 472 │ │ │ │ │ +10.147opt_ffinv - push inverters through FFs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473 │ │ │ │ │ +10.148opt_lut - optimize LUT cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473 │ │ │ │ │ +10.149opt_lut_ins - discard unused LUT inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473 │ │ │ │ │ +10.150opt_mem - optimize memories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 474 │ │ │ │ │ │ │ │ │ │ vi │ │ │ │ │ │ │ │ │ │ - 10.151opt_mem_feedback - convert memory read-to-write port feedback paths to write enables . . 472 │ │ │ │ │ -10.152opt_mem_priority - remove priority relations between write ports that can never collide . . 472 │ │ │ │ │ -10.153opt_mem_widen - optimize memories where all ports are wide . . . . . . . . . . . . . . . . . 473 │ │ │ │ │ -10.154opt_merge - consolidate identical cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473 │ │ │ │ │ -10.155opt_muxtree - eliminate dead trees in multiplexer trees . . . . . . . . . . . . . . . . . . . . . 473 │ │ │ │ │ -10.156opt_reduce - simplify large MUXes and AND/OR gates . . . . . . . . . . . . . . . . . . . . . 473 │ │ │ │ │ -10.157opt_share - merge mutually exclusive cells of the same type that share an input signal . . . 474 │ │ │ │ │ -10.158paramap - renaming cell parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 474 │ │ │ │ │ -10.159peepopt - collection of peephole optimizers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 475 │ │ │ │ │ -10.160plugin - load and list loaded plugins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 475 │ │ │ │ │ -10.161pmux2shiftx - transform $pmux cells to $shiftx cells . . . . . . . . . . . . . . . . . . . . . . . 476 │ │ │ │ │ -10.162pmuxtree - transform $pmux cells to trees of $mux cells . . . . . . . . . . . . . . . . . . . . . 476 │ │ │ │ │ -10.163portarcs - derive port arcs for propagation delay . . . . . . . . . . . . . . . . . . . . . . . . . 476 │ │ │ │ │ -10.164portlist - list (top-level) ports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477 │ │ │ │ │ -10.165prep - generic synthesis script . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477 │ │ │ │ │ -10.166printattrs - print attributes of selected objects . . . . . . . . . . . . . . . . . . . . . . . . . . 478 │ │ │ │ │ -10.167proc - translate processes to netlists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 479 │ │ │ │ │ -10.168proc_arst - detect asynchronous resets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 479 │ │ │ │ │ -10.169proc_clean - remove empty parts of processes . . . . . . . . . . . . . . . . . . . . . . . . . . 480 │ │ │ │ │ -10.170proc_dff - extract flip-flops from processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 480 │ │ │ │ │ -10.171proc_dlatch - extract latches from processes . . . . . . . . . . . . . . . . . . . . . . . . . . . 480 │ │ │ │ │ -10.172proc_init - convert initial block to init attributes . . . . . . . . . . . . . . . . . . . . . . . . 480 │ │ │ │ │ -10.173proc_memwr - extract memory writes from processes . . . . . . . . . . . . . . . . . . . . . . 481 │ │ │ │ │ -10.174proc_mux - convert decision trees to multiplexers . . . . . . . . . . . . . . . . . . . . . . . . 481 │ │ │ │ │ -10.175proc_prune - remove redundant assignments . . . . . . . . . . . . . . . . . . . . . . . . . . . 481 │ │ │ │ │ -10.176proc_rmdead - eliminate dead trees in decision trees . . . . . . . . . . . . . . . . . . . . . . . 481 │ │ │ │ │ -10.177proc_rom - convert switches to ROMs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 481 │ │ │ │ │ -10.178qbfsat - solve a 2QBF-SAT problem in the circuit . . . . . . . . . . . . . . . . . . . . . . . . 482 │ │ │ │ │ -10.179ql_bram_merge - Infers QuickLogic k6n10f BRAM pairs that can operate independently . . 483 │ │ │ │ │ -10.180ql_bram_types - Change TDP36K type to subtypes . . . . . . . . . . . . . . . . . . . . . . . 483 │ │ │ │ │ -10.181ql_dsp_io_regs - change types of QL_DSP2 depending on configuration . . . . . . . . . . . 483 │ │ │ │ │ -10.182ql_dsp_macc - infer QuickLogic multiplier-accumulator DSP cells . . . . . . . . . . . . . . . 484 │ │ │ │ │ -10.183ql_dsp_simd - merge QuickLogic K6N10f DSP pairs to operate in SIMD mode . . . . . . . . 484 │ │ │ │ │ -10.184ql_ioff - Infer I/O FFs for qlf_k6n10f architecture . . . . . . . . . . . . . . . . . . . . . . . . 484 │ │ │ │ │ -10.185read - load HDL designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 484 │ │ │ │ │ -10.186read_aiger - read AIGER file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 485 │ │ │ │ │ -10.187read_blif - read BLIF file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 486 │ │ │ │ │ -10.188read_json - read JSON file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 486 │ │ │ │ │ -10.189read_liberty - read cells from liberty file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 486 │ │ │ │ │ -10.190read_rtlil - read modules from RTLIL file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 487 │ │ │ │ │ -10.191read_verilog - read modules from Verilog file . . . . . . . . . . . . . . . . . . . . . . . . . . . 488 │ │ │ │ │ -10.192read_verilog_file_list - parse a Verilog file list . . . . . . . . . . . . . . . . . . . . . . . . . . 491 │ │ │ │ │ -10.193read_xaiger2 - (experimental) read XAIGER file . . . . . . . . . . . . . . . . . . . . . . . . . 491 │ │ │ │ │ -10.194recover_names - Execute a lossy mapping command and recover original netnames . . . . . 492 │ │ │ │ │ -10.195rename - rename object in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492 │ │ │ │ │ -10.196rmports - remove module ports with no connections . . . . . . . . . . . . . . . . . . . . . . . 493 │ │ │ │ │ -10.197sat - solve a SAT problem in the circuit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 493 │ │ │ │ │ -10.198scatter - add additional intermediate nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 497 │ │ │ │ │ -10.199scc - detect strongly connected components (logic loops) . . . . . . . . . . . . . . . . . . . . 497 │ │ │ │ │ -10.200scratchpad - get/set values in the scratchpad . . . . . . . . . . . . . . . . . . . . . . . . . . . 498 │ │ │ │ │ -10.201script - execute commands from file or wire . . . . . . . . . . . . . . . . . . . . . . . . . . . . 498 │ │ │ │ │ -10.202select - modify and view the list of selected objects . . . . . . . . . . . . . . . . . . . . . . . . 499 │ │ │ │ │ -10.203setattr - set/unset attributes on objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 503 │ │ │ │ │ -10.204setenv - set an environment variable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 504 │ │ │ │ │ + 10.151opt_mem_feedback - convert memory read-to-write port feedback paths to write enables . . 474 │ │ │ │ │ +10.152opt_mem_priority - remove priority relations between write ports that can never collide . . 474 │ │ │ │ │ +10.153opt_mem_widen - optimize memories where all ports are wide . . . . . . . . . . . . . . . . . 475 │ │ │ │ │ +10.154opt_merge - consolidate identical cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 475 │ │ │ │ │ +10.155opt_muxtree - eliminate dead trees in multiplexer trees . . . . . . . . . . . . . . . . . . . . . 475 │ │ │ │ │ +10.156opt_reduce - simplify large MUXes and AND/OR gates . . . . . . . . . . . . . . . . . . . . . 475 │ │ │ │ │ +10.157opt_share - merge mutually exclusive cells of the same type that share an input signal . . . 476 │ │ │ │ │ +10.158paramap - renaming cell parameters . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 476 │ │ │ │ │ +10.159peepopt - collection of peephole optimizers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477 │ │ │ │ │ +10.160plugin - load and list loaded plugins . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477 │ │ │ │ │ +10.161pmux2shiftx - transform $pmux cells to $shiftx cells . . . . . . . . . . . . . . . . . . . . . . . 478 │ │ │ │ │ +10.162pmuxtree - transform $pmux cells to trees of $mux cells . . . . . . . . . . . . . . . . . . . . . 478 │ │ │ │ │ +10.163portarcs - derive port arcs for propagation delay . . . . . . . . . . . . . . . . . . . . . . . . . 478 │ │ │ │ │ +10.164portlist - list (top-level) ports . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 479 │ │ │ │ │ +10.165prep - generic synthesis script . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 479 │ │ │ │ │ +10.166printattrs - print attributes of selected objects . . . . . . . . . . . . . . . . . . . . . . . . . . 480 │ │ │ │ │ +10.167proc - translate processes to netlists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 481 │ │ │ │ │ +10.168proc_arst - detect asynchronous resets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 481 │ │ │ │ │ +10.169proc_clean - remove empty parts of processes . . . . . . . . . . . . . . . . . . . . . . . . . . 482 │ │ │ │ │ +10.170proc_dff - extract flip-flops from processes . . . . . . . . . . . . . . . . . . . . . . . . . . . . 482 │ │ │ │ │ +10.171proc_dlatch - extract latches from processes . . . . . . . . . . . . . . . . . . . . . . . . . . . 482 │ │ │ │ │ +10.172proc_init - convert initial block to init attributes . . . . . . . . . . . . . . . . . . . . . . . . 482 │ │ │ │ │ +10.173proc_memwr - extract memory writes from processes . . . . . . . . . . . . . . . . . . . . . . 483 │ │ │ │ │ +10.174proc_mux - convert decision trees to multiplexers . . . . . . . . . . . . . . . . . . . . . . . . 483 │ │ │ │ │ +10.175proc_prune - remove redundant assignments . . . . . . . . . . . . . . . . . . . . . . . . . . . 483 │ │ │ │ │ +10.176proc_rmdead - eliminate dead trees in decision trees . . . . . . . . . . . . . . . . . . . . . . . 483 │ │ │ │ │ +10.177proc_rom - convert switches to ROMs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 483 │ │ │ │ │ +10.178qbfsat - solve a 2QBF-SAT problem in the circuit . . . . . . . . . . . . . . . . . . . . . . . . 484 │ │ │ │ │ +10.179ql_bram_merge - Infers QuickLogic k6n10f BRAM pairs that can operate independently . . 485 │ │ │ │ │ +10.180ql_bram_types - Change TDP36K type to subtypes . . . . . . . . . . . . . . . . . . . . . . . 485 │ │ │ │ │ +10.181ql_dsp_io_regs - change types of QL_DSP2 depending on configuration . . . . . . . . . . . 485 │ │ │ │ │ +10.182ql_dsp_macc - infer QuickLogic multiplier-accumulator DSP cells . . . . . . . . . . . . . . . 486 │ │ │ │ │ +10.183ql_dsp_simd - merge QuickLogic K6N10f DSP pairs to operate in SIMD mode . . . . . . . . 486 │ │ │ │ │ +10.184ql_ioff - Infer I/O FFs for qlf_k6n10f architecture . . . . . . . . . . . . . . . . . . . . . . . . 486 │ │ │ │ │ +10.185read - load HDL designs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 486 │ │ │ │ │ +10.186read_aiger - read AIGER file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 487 │ │ │ │ │ +10.187read_blif - read BLIF file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 488 │ │ │ │ │ +10.188read_json - read JSON file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 488 │ │ │ │ │ +10.189read_liberty - read cells from liberty file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 488 │ │ │ │ │ +10.190read_rtlil - read modules from RTLIL file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 489 │ │ │ │ │ +10.191read_verilog - read modules from Verilog file . . . . . . . . . . . . . . . . . . . . . . . . . . . 490 │ │ │ │ │ +10.192read_verilog_file_list - parse a Verilog file list . . . . . . . . . . . . . . . . . . . . . . . . . . 493 │ │ │ │ │ +10.193read_xaiger2 - (experimental) read XAIGER file . . . . . . . . . . . . . . . . . . . . . . . . . 493 │ │ │ │ │ +10.194recover_names - Execute a lossy mapping command and recover original netnames . . . . . 494 │ │ │ │ │ +10.195rename - rename object in the design . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 494 │ │ │ │ │ +10.196rmports - remove module ports with no connections . . . . . . . . . . . . . . . . . . . . . . . 495 │ │ │ │ │ +10.197sat - solve a SAT problem in the circuit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 495 │ │ │ │ │ +10.198scatter - add additional intermediate nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 499 │ │ │ │ │ +10.199scc - detect strongly connected components (logic loops) . . . . . . . . . . . . . . . . . . . . 499 │ │ │ │ │ +10.200scratchpad - get/set values in the scratchpad . . . . . . . . . . . . . . . . . . . . . . . . . . . 500 │ │ │ │ │ +10.201script - execute commands from file or wire . . . . . . . . . . . . . . . . . . . . . . . . . . . . 500 │ │ │ │ │ +10.202select - modify and view the list of selected objects . . . . . . . . . . . . . . . . . . . . . . . . 501 │ │ │ │ │ +10.203setattr - set/unset attributes on objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 505 │ │ │ │ │ +10.204setenv - set an environment variable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 506 │ │ │ │ │ │ │ │ │ │ vii │ │ │ │ │ │ │ │ │ │ - 10.205setparam - set/unset parameters on objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . 504 │ │ │ │ │ -10.206setundef - replace undef values with defined constants . . . . . . . . . . . . . . . . . . . . . . 504 │ │ │ │ │ -10.207share - perform sat-based resource sharing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 505 │ │ │ │ │ -10.208shell - enter interactive command mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 505 │ │ │ │ │ -10.209show - generate schematics using graphviz . . . . . . . . . . . . . . . . . . . . . . . . . . . . 506 │ │ │ │ │ -10.210shregmap - map shift registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 508 │ │ │ │ │ -10.211sim - simulate the circuit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 509 │ │ │ │ │ -10.212simplemap - mapping simple coarse-grain cells . . . . . . . . . . . . . . . . . . . . . . . . . . 511 │ │ │ │ │ -10.213splice - create explicit splicing cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 512 │ │ │ │ │ -10.214splitcells - split up multi-bit cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 512 │ │ │ │ │ -10.215splitnets - split up multi-bit nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 513 │ │ │ │ │ -10.216sta - perform static timing analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 513 │ │ │ │ │ -10.217stat - print some statistics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 513 │ │ │ │ │ -10.218submod - moving part of a module to a new submodule . . . . . . . . . . . . . . . . . . . . . 514 │ │ │ │ │ -10.219supercover - add hi/lo cover cells for each wire bit . . . . . . . . . . . . . . . . . . . . . . . . 515 │ │ │ │ │ -10.220synth - generic synthesis script . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 515 │ │ │ │ │ -10.221synth_achronix - synthesis for Achronix Speedster22i FPGAs. . . . . . . . . . . . . . . . . . 517 │ │ │ │ │ -10.222synth_anlogic - synthesis for Anlogic FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . 518 │ │ │ │ │ -10.223synth_coolrunner2 - synthesis for Xilinx Coolrunner-II CPLDs . . . . . . . . . . . . . . . . . 520 │ │ │ │ │ -10.224synth_easic - synthesis for eASIC platform . . . . . . . . . . . . . . . . . . . . . . . . . . . . 522 │ │ │ │ │ -10.225synth_ecp5 - synthesis for ECP5 FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 523 │ │ │ │ │ -10.226synth_efinix - synthesis for Efinix FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 527 │ │ │ │ │ -10.227synth_fabulous - FABulous synthesis script . . . . . . . . . . . . . . . . . . . . . . . . . . . . 528 │ │ │ │ │ -10.228synth_gatemate - synthesis for Cologne Chip GateMate FPGAs . . . . . . . . . . . . . . . . 532 │ │ │ │ │ -10.229synth_gowin - synthesis for Gowin FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 535 │ │ │ │ │ -10.230synth_greenpak4 - synthesis for GreenPAK4 FPGAs . . . . . . . . . . . . . . . . . . . . . . 537 │ │ │ │ │ -10.231synth_ice40 - synthesis for iCE40 FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 539 │ │ │ │ │ -10.232synth_intel - synthesis for Intel (Altera) FPGAs. . . . . . . . . . . . . . . . . . . . . . . . . 542 │ │ │ │ │ -10.233synth_intel_alm - synthesis for ALM-based Intel (Altera) FPGAs. . . . . . . . . . . . . . . . 545 │ │ │ │ │ -10.234synth_lattice - synthesis for Lattice FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . 547 │ │ │ │ │ -10.235synth_microchip - synthesis for Microchip FPGAs . . . . . . . . . . . . . . . . . . . . . . . . 551 │ │ │ │ │ -10.236synth_nanoxplore - synthesis for NanoXplore FPGAs . . . . . . . . . . . . . . . . . . . . . . 554 │ │ │ │ │ -10.237synth_nexus - synthesis for Lattice Nexus FPGAs . . . . . . . . . . . . . . . . . . . . . . . . 557 │ │ │ │ │ -10.238synth_quicklogic - Synthesis for QuickLogic FPGAs . . . . . . . . . . . . . . . . . . . . . . . 560 │ │ │ │ │ -10.239synth_sf2 - synthesis for SmartFusion2 and IGLOO2 FPGAs . . . . . . . . . . . . . . . . . . 563 │ │ │ │ │ -10.240synth_xilinx - synthesis for Xilinx FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 565 │ │ │ │ │ -10.241synthprop - synthesize SVA properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 569 │ │ │ │ │ -10.242tcl - execute a TCL script file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 569 │ │ │ │ │ -10.243techmap - generic technology mapper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 570 │ │ │ │ │ -10.244tee - redirect command output to file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 573 │ │ │ │ │ -10.245test_abcloop - automatically test handling of loops in abc command . . . . . . . . . . . . . . 573 │ │ │ │ │ -10.246test_autotb - generate simple test benches . . . . . . . . . . . . . . . . . . . . . . . . . . . . 574 │ │ │ │ │ -10.247test_cell - automatically test the implementation of a cell type . . . . . . . . . . . . . . . . . 574 │ │ │ │ │ -10.248test_generic - test the generic compute graph . . . . . . . . . . . . . . . . . . . . . . . . . . 576 │ │ │ │ │ -10.249test_pmgen - test pass for pmgen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 576 │ │ │ │ │ -10.250torder - print cells in topological order . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 576 │ │ │ │ │ -10.251trace - redirect command output to file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 577 │ │ │ │ │ -10.252tribuf - infer tri-state buffers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 577 │ │ │ │ │ -10.253uniquify - create unique copies of modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 577 │ │ │ │ │ -10.254verific - load Verilog and VHDL designs using Verific . . . . . . . . . . . . . . . . . . . . . . 578 │ │ │ │ │ -10.255verilog_defaults - set default options for read_verilog . . . . . . . . . . . . . . . . . . . . . . 580 │ │ │ │ │ -10.256verilog_defines - define and undefine verilog defines . . . . . . . . . . . . . . . . . . . . . . . 580 │ │ │ │ │ -10.257viz - visualize data flow graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 581 │ │ │ │ │ -10.258wbflip - flip the whitebox attribute . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 582 │ │ │ │ │ + 10.205setparam - set/unset parameters on objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . 506 │ │ │ │ │ +10.206setundef - replace undef values with defined constants . . . . . . . . . . . . . . . . . . . . . . 506 │ │ │ │ │ +10.207share - perform sat-based resource sharing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 507 │ │ │ │ │ +10.208shell - enter interactive command mode . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 507 │ │ │ │ │ +10.209show - generate schematics using graphviz . . . . . . . . . . . . . . . . . . . . . . . . . . . . 508 │ │ │ │ │ +10.210shregmap - map shift registers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 510 │ │ │ │ │ +10.211sim - simulate the circuit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 511 │ │ │ │ │ +10.212simplemap - mapping simple coarse-grain cells . . . . . . . . . . . . . . . . . . . . . . . . . . 513 │ │ │ │ │ +10.213splice - create explicit splicing cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 514 │ │ │ │ │ +10.214splitcells - split up multi-bit cells . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 514 │ │ │ │ │ +10.215splitnets - split up multi-bit nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 515 │ │ │ │ │ +10.216sta - perform static timing analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 515 │ │ │ │ │ +10.217stat - print some statistics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 515 │ │ │ │ │ +10.218submod - moving part of a module to a new submodule . . . . . . . . . . . . . . . . . . . . . 516 │ │ │ │ │ +10.219supercover - add hi/lo cover cells for each wire bit . . . . . . . . . . . . . . . . . . . . . . . . 517 │ │ │ │ │ +10.220synth - generic synthesis script . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 517 │ │ │ │ │ +10.221synth_achronix - synthesis for Achronix Speedster22i FPGAs. . . . . . . . . . . . . . . . . . 519 │ │ │ │ │ +10.222synth_anlogic - synthesis for Anlogic FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . 520 │ │ │ │ │ +10.223synth_coolrunner2 - synthesis for Xilinx Coolrunner-II CPLDs . . . . . . . . . . . . . . . . . 522 │ │ │ │ │ +10.224synth_easic - synthesis for eASIC platform . . . . . . . . . . . . . . . . . . . . . . . . . . . . 524 │ │ │ │ │ +10.225synth_ecp5 - synthesis for ECP5 FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 525 │ │ │ │ │ +10.226synth_efinix - synthesis for Efinix FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 529 │ │ │ │ │ +10.227synth_fabulous - FABulous synthesis script . . . . . . . . . . . . . . . . . . . . . . . . . . . . 530 │ │ │ │ │ +10.228synth_gatemate - synthesis for Cologne Chip GateMate FPGAs . . . . . . . . . . . . . . . . 534 │ │ │ │ │ +10.229synth_gowin - synthesis for Gowin FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 537 │ │ │ │ │ +10.230synth_greenpak4 - synthesis for GreenPAK4 FPGAs . . . . . . . . . . . . . . . . . . . . . . 539 │ │ │ │ │ +10.231synth_ice40 - synthesis for iCE40 FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 541 │ │ │ │ │ +10.232synth_intel - synthesis for Intel (Altera) FPGAs. . . . . . . . . . . . . . . . . . . . . . . . . 544 │ │ │ │ │ +10.233synth_intel_alm - synthesis for ALM-based Intel (Altera) FPGAs. . . . . . . . . . . . . . . . 547 │ │ │ │ │ +10.234synth_lattice - synthesis for Lattice FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . 549 │ │ │ │ │ +10.235synth_microchip - synthesis for Microchip FPGAs . . . . . . . . . . . . . . . . . . . . . . . . 553 │ │ │ │ │ +10.236synth_nanoxplore - synthesis for NanoXplore FPGAs . . . . . . . . . . . . . . . . . . . . . . 556 │ │ │ │ │ +10.237synth_nexus - synthesis for Lattice Nexus FPGAs . . . . . . . . . . . . . . . . . . . . . . . . 559 │ │ │ │ │ +10.238synth_quicklogic - Synthesis for QuickLogic FPGAs . . . . . . . . . . . . . . . . . . . . . . . 562 │ │ │ │ │ +10.239synth_sf2 - synthesis for SmartFusion2 and IGLOO2 FPGAs . . . . . . . . . . . . . . . . . . 565 │ │ │ │ │ +10.240synth_xilinx - synthesis for Xilinx FPGAs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 567 │ │ │ │ │ +10.241synthprop - synthesize SVA properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 571 │ │ │ │ │ +10.242tcl - execute a TCL script file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 571 │ │ │ │ │ +10.243techmap - generic technology mapper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 572 │ │ │ │ │ +10.244tee - redirect command output to file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 575 │ │ │ │ │ +10.245test_abcloop - automatically test handling of loops in abc command . . . . . . . . . . . . . . 575 │ │ │ │ │ +10.246test_autotb - generate simple test benches . . . . . . . . . . . . . . . . . . . . . . . . . . . . 576 │ │ │ │ │ +10.247test_cell - automatically test the implementation of a cell type . . . . . . . . . . . . . . . . . 576 │ │ │ │ │ +10.248test_generic - test the generic compute graph . . . . . . . . . . . . . . . . . . . . . . . . . . 578 │ │ │ │ │ +10.249test_pmgen - test pass for pmgen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 578 │ │ │ │ │ +10.250torder - print cells in topological order . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 578 │ │ │ │ │ +10.251trace - redirect command output to file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 579 │ │ │ │ │ +10.252tribuf - infer tri-state buffers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 579 │ │ │ │ │ +10.253uniquify - create unique copies of modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 579 │ │ │ │ │ +10.254verific - load Verilog and VHDL designs using Verific . . . . . . . . . . . . . . . . . . . . . . 580 │ │ │ │ │ +10.255verilog_defaults - set default options for read_verilog . . . . . . . . . . . . . . . . . . . . . . 582 │ │ │ │ │ +10.256verilog_defines - define and undefine verilog defines . . . . . . . . . . . . . . . . . . . . . . . 582 │ │ │ │ │ +10.257viz - visualize data flow graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 583 │ │ │ │ │ +10.258wbflip - flip the whitebox attribute . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 584 │ │ │ │ │ │ │ │ │ │ viii │ │ │ │ │ │ │ │ │ │ - 10.259wrapcell - wrap individual cells into new modules . . . . . . . . . . . . . . . . . . . . . . . . 582 │ │ │ │ │ -10.260wreduce - reduce the word size of operations if possible . . . . . . . . . . . . . . . . . . . . . 583 │ │ │ │ │ -10.261write_aiger - write design to AIGER file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 583 │ │ │ │ │ -10.262write_aiger2 - (experimental) write design to AIGER file . . . . . . . . . . . . . . . . . . . . 584 │ │ │ │ │ -10.263write_blif - write design to BLIF file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 584 │ │ │ │ │ -10.264write_btor - write design to BTOR file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 586 │ │ │ │ │ -10.265write_cxxrtl - convert design to C++ RTL simulation . . . . . . . . . . . . . . . . . . . . . . 586 │ │ │ │ │ -10.266write_edif - write design to EDIF netlist file . . . . . . . . . . . . . . . . . . . . . . . . . . . 591 │ │ │ │ │ -10.267write_file - write a text to a file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 592 │ │ │ │ │ -10.268write_firrtl - write design to a FIRRTL file . . . . . . . . . . . . . . . . . . . . . . . . . . . . 592 │ │ │ │ │ -10.269write_functional_cxx - convert design to C++ using the functional backend . . . . . . . . . 592 │ │ │ │ │ -10.270write_functional_rosette - Generate Rosette compatible Racket from Functional IR . . . . . 593 │ │ │ │ │ -10.271write_functional_smt2 - Generate SMT-LIB from Functional IR . . . . . . . . . . . . . . . . 593 │ │ │ │ │ -10.272write_intersynth - write design to InterSynth netlist file . . . . . . . . . . . . . . . . . . . . . 593 │ │ │ │ │ -10.273write_jny - generate design metadata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 593 │ │ │ │ │ -10.274write_json - write design to a JSON file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 594 │ │ │ │ │ -10.275write_rtlil - write design to RTLIL file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 599 │ │ │ │ │ -10.276write_simplec - convert design to simple C code . . . . . . . . . . . . . . . . . . . . . . . . . 599 │ │ │ │ │ -10.277write_smt2 - write design to SMT-LIBv2 file . . . . . . . . . . . . . . . . . . . . . . . . . . . 600 │ │ │ │ │ -10.278write_smv - write design to SMV file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 603 │ │ │ │ │ -10.279write_spice - write design to SPICE netlist file . . . . . . . . . . . . . . . . . . . . . . . . . . 603 │ │ │ │ │ -10.280write_table - write design as connectivity table . . . . . . . . . . . . . . . . . . . . . . . . . 604 │ │ │ │ │ -10.281write_verilog - write design to Verilog file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 604 │ │ │ │ │ -10.282write_xaiger - write design to XAIGER file . . . . . . . . . . . . . . . . . . . . . . . . . . . . 606 │ │ │ │ │ -10.283write_xaiger2 - (experimental) write module to XAIGER file . . . . . . . . . . . . . . . . . . 606 │ │ │ │ │ -10.284xilinx_dffopt - Xilinx: optimize FF control signal usage . . . . . . . . . . . . . . . . . . . . . 607 │ │ │ │ │ -10.285xilinx_dsp - Xilinx: pack resources into DSPs . . . . . . . . . . . . . . . . . . . . . . . . . . 607 │ │ │ │ │ -10.286xilinx_srl - Xilinx shift register extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 608 │ │ │ │ │ -10.287xprop - formal x propagation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 608 │ │ │ │ │ -10.288zinit - add inverters so all FF are zero-initialized . . . . . . . . . . . . . . . . . . . . . . . . . 609 │ │ │ │ │ + 10.259wrapcell - wrap individual cells into new modules . . . . . . . . . . . . . . . . . . . . . . . . 584 │ │ │ │ │ +10.260wreduce - reduce the word size of operations if possible . . . . . . . . . . . . . . . . . . . . . 585 │ │ │ │ │ +10.261write_aiger - write design to AIGER file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 585 │ │ │ │ │ +10.262write_aiger2 - (experimental) write design to AIGER file . . . . . . . . . . . . . . . . . . . . 586 │ │ │ │ │ +10.263write_blif - write design to BLIF file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 586 │ │ │ │ │ +10.264write_btor - write design to BTOR file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 588 │ │ │ │ │ +10.265write_cxxrtl - convert design to C++ RTL simulation . . . . . . . . . . . . . . . . . . . . . . 588 │ │ │ │ │ +10.266write_edif - write design to EDIF netlist file . . . . . . . . . . . . . . . . . . . . . . . . . . . 593 │ │ │ │ │ +10.267write_file - write a text to a file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 594 │ │ │ │ │ +10.268write_firrtl - write design to a FIRRTL file . . . . . . . . . . . . . . . . . . . . . . . . . . . . 594 │ │ │ │ │ +10.269write_functional_cxx - convert design to C++ using the functional backend . . . . . . . . . 594 │ │ │ │ │ +10.270write_functional_rosette - Generate Rosette compatible Racket from Functional IR . . . . . 595 │ │ │ │ │ +10.271write_functional_smt2 - Generate SMT-LIB from Functional IR . . . . . . . . . . . . . . . . 595 │ │ │ │ │ +10.272write_intersynth - write design to InterSynth netlist file . . . . . . . . . . . . . . . . . . . . . 595 │ │ │ │ │ +10.273write_jny - generate design metadata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 595 │ │ │ │ │ +10.274write_json - write design to a JSON file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 596 │ │ │ │ │ +10.275write_rtlil - write design to RTLIL file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 601 │ │ │ │ │ +10.276write_simplec - convert design to simple C code . . . . . . . . . . . . . . . . . . . . . . . . . 601 │ │ │ │ │ +10.277write_smt2 - write design to SMT-LIBv2 file . . . . . . . . . . . . . . . . . . . . . . . . . . . 602 │ │ │ │ │ +10.278write_smv - write design to SMV file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 605 │ │ │ │ │ +10.279write_spice - write design to SPICE netlist file . . . . . . . . . . . . . . . . . . . . . . . . . . 605 │ │ │ │ │ +10.280write_table - write design as connectivity table . . . . . . . . . . . . . . . . . . . . . . . . . 606 │ │ │ │ │ +10.281write_verilog - write design to Verilog file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 606 │ │ │ │ │ +10.282write_xaiger - write design to XAIGER file . . . . . . . . . . . . . . . . . . . . . . . . . . . . 608 │ │ │ │ │ +10.283write_xaiger2 - (experimental) write module to XAIGER file . . . . . . . . . . . . . . . . . . 608 │ │ │ │ │ +10.284xilinx_dffopt - Xilinx: optimize FF control signal usage . . . . . . . . . . . . . . . . . . . . . 609 │ │ │ │ │ +10.285xilinx_dsp - Xilinx: pack resources into DSPs . . . . . . . . . . . . . . . . . . . . . . . . . . 609 │ │ │ │ │ +10.286xilinx_srl - Xilinx shift register extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 610 │ │ │ │ │ +10.287xprop - formal x propagation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 610 │ │ │ │ │ +10.288zinit - add inverters so all FF are zero-initialized . . . . . . . . . . . . . . . . . . . . . . . . . 611 │ │ │ │ │ Bibliography │ │ │ │ │ │ │ │ │ │ -611 │ │ │ │ │ +613 │ │ │ │ │ │ │ │ │ │ Property Index │ │ │ │ │ │ │ │ │ │ -613 │ │ │ │ │ +615 │ │ │ │ │ │ │ │ │ │ Internal cell reference │ │ │ │ │ │ │ │ │ │ -615 │ │ │ │ │ +617 │ │ │ │ │ │ │ │ │ │ Command Reference │ │ │ │ │ │ │ │ │ │ -619 │ │ │ │ │ +621 │ │ │ │ │ │ │ │ │ │ Tag Index │ │ │ │ │ │ │ │ │ │ -623 │ │ │ │ │ +625 │ │ │ │ │ │ │ │ │ │ ix │ │ │ │ │ │ │ │ │ │ x │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ @@ -15519,15 +15519,20 @@ │ │ │ │ │ │ │ │ │ │ To find the compile options used for a given Yosys build, call yosys-config --cxxflags. This documentation was built with the following compile options: │ │ │ │ │ --cxxflags │ │ │ │ │ │ │ │ │ │ -g -O2 -flto=auto -ffat-lto-objects \ │ │ │ │ │ -fstack-protector-strong -Wformat -Werror=format-security \ │ │ │ │ │ -Wall -Wextra -ggdb -I/usr/share/yosys/include -MD -MP \ │ │ │ │ │ --D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER= │ │ │ │ │ +-D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER=@CXXFLAGS@.52 \ │ │ │ │ │ +-DYOSYS_MAJOR=0 -DYOSYS_MINOR=52 -DYOSYS_COMMIT=0.52 \ │ │ │ │ │ +-std=c++17 -O3 -DYOSYS_ENABLE_READLINE \ │ │ │ │ │ +-DYOSYS_ENABLE_PLUGINS -DYOSYS_ENABLE_GLOB \ │ │ │ │ │ +-DYOSYS_ENABLE_ZLIB -I/usr/include/tcl8.6 \ │ │ │ │ │ +-DYOSYS_ENABLE_TCL -DYOSYS_ENABLE_ABC -DYOSYS_ENABLE_COVER │ │ │ │ │ │ │ │ │ │ ò Note │ │ │ │ │ The YosysHQ specific extensions are only available with the TabbyCAD suite. │ │ │ │ │ │ │ │ │ │ Required Verific features │ │ │ │ │ The following features, along with their corresponding Yosys build parameters, are required for the YosysVerific patch: │ │ │ │ │ • RTL elaboration with │ │ │ │ │ @@ -15539,24 +15544,23 @@ │ │ │ │ │ database/DBCompileFlags.h: │ │ │ │ │ DB_PRESERVE_INITIAL_VALUE │ │ │ │ │ │ │ │ │ │ ò Note │ │ │ │ │ Yosys+Verific builds may compile without these features, but we provide no guarantees and cannot offer │ │ │ │ │ support if they are disabled or the Yosys-Verific patch is not used. │ │ │ │ │ │ │ │ │ │ -Optional Verific features │ │ │ │ │ -The following Verific features are available with TabbyCAD and can be enabled in Yosys builds: │ │ │ │ │ -• EDIF support with ENABLE_VERIFIC_EDIF, and │ │ │ │ │ - │ │ │ │ │ 172 │ │ │ │ │ │ │ │ │ │ Chapter 4. Yosys internals │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ +Optional Verific features │ │ │ │ │ +The following Verific features are available with TabbyCAD and can be enabled in Yosys builds: │ │ │ │ │ +• EDIF support with ENABLE_VERIFIC_EDIF, and │ │ │ │ │ • Liberty file support with ENABLE_VERIFIC_LIBERTY. │ │ │ │ │ Partially supported builds │ │ │ │ │ This section describes Yosys+Verific configurations which we have confirmed as working in the past, however │ │ │ │ │ they are not a part of our regular tests so we cannot guarantee they are still functional. │ │ │ │ │ To be able to compile Yosys with Verific, the Verific library must have support for at least one HDL language │ │ │ │ │ with RTL elaboration enabled. The following table lists a series of build configurations which are possible, │ │ │ │ │ but only provide a limited subset of features. Please note that support is limited without YosysHQ specific │ │ │ │ │ @@ -15621,24 +15625,24 @@ │ │ │ │ │ intermediate representation called FunctionalIR which maps more directly on those targets. │ │ │ │ │ FunctionalIR represents the design as a function (inputs, current_state) -> (outputs, next_state). │ │ │ │ │ This function is broken down into a series of assignments to variables. Each assignment is a simple operation, │ │ │ │ │ such as an addition. Complex operations are broken up into multiple steps. For example, an RTLIL addition │ │ │ │ │ will be translated into a sign/zero extension of the inputs, followed by an addition. │ │ │ │ │ Like SSA form, each variable is assigned to exactly once. We can thus treat variables and assignments │ │ │ │ │ as equivalent and, since this is a graph-like representation, those variables are also called “nodes”. Unlike │ │ │ │ │ -RTLIL’s cells and wires representation, this representation is strictly ordered (topologically sorted) with │ │ │ │ │ -definitions preceding their use. │ │ │ │ │ -Every node has a “sort” (the FunctionalIR term for what might otherwise be called a “type”). The sorts │ │ │ │ │ -available are │ │ │ │ │ 4.3. Working with the Yosys codebase │ │ │ │ │ │ │ │ │ │ 173 │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ +RTLIL’s cells and wires representation, this representation is strictly ordered (topologically sorted) with │ │ │ │ │ +definitions preceding their use. │ │ │ │ │ +Every node has a “sort” (the FunctionalIR term for what might otherwise be called a “type”). The sorts │ │ │ │ │ +available are │ │ │ │ │ • bit[n] for an n-bit bitvector, and │ │ │ │ │ • memory[n,m] for an immutable array of 2**n values of sort bit[m]. │ │ │ │ │ In terms of actual code, Yosys provides a class Functional::IR that represents a design in FunctionalIR. │ │ │ │ │ Functional::IR::from_module generates an instance from an RTLIL module. The entire design is stored │ │ │ │ │ as a whole in an internal data structure. To access the design, the Functional::Node class provides a │ │ │ │ │ reference to a particular node in the design. The Functional::IR class supports the syntax for(auto node │ │ │ │ │ : ir) to iterate over every node. │ │ │ │ │ @@ -15669,25 +15673,24 @@ │ │ │ │ │ Utility classes │ │ │ │ │ functional.h also provides utility classes that are independent of the main FunctionalIR representation but │ │ │ │ │ are likely to be useful for backends. │ │ │ │ │ Functional::Writer provides a simple formatting class that wraps a std::ostream and provides the following methods: │ │ │ │ │ • writer << value wraps os << value. │ │ │ │ │ • writer.print(fmt, value0, value1, value2, ...) replaces {0}, {1}, {2}, etc in the string fmt │ │ │ │ │ with value0, value1, value2, resp. Each value is formatted using os << value. It is also possible to │ │ │ │ │ -write {} to refer to one past the last index, i.e. {1} {} {} {7} {} is equivalent to {1} {2} {3} {7} │ │ │ │ │ -{8}. │ │ │ │ │ -• writer.print_with(fn, fmt, value0, value1, value2, ...) functions much the same as print │ │ │ │ │ -but it uses os << fn(value) to print each value and falls back to os << value if fn(value) is not │ │ │ │ │ - │ │ │ │ │ 174 │ │ │ │ │ │ │ │ │ │ Chapter 4. Yosys internals │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ +write {} to refer to one past the last index, i.e. {1} {} {} {7} {} is equivalent to {1} {2} {3} {7} │ │ │ │ │ +{8}. │ │ │ │ │ +• writer.print_with(fn, fmt, value0, value1, value2, ...) functions much the same as print │ │ │ │ │ +but it uses os << fn(value) to print each value and falls back to os << value if fn(value) is not │ │ │ │ │ legal. │ │ │ │ │ Functional::Scope keeps track of variable names in a target language. It is used to translate between │ │ │ │ │ different sets of legal characters and to avoid accidentally re-defining identifiers. Users should derive a class │ │ │ │ │ from Scope and supply the following: │ │ │ │ │ • Scope takes a template argument that specifies a type that’s used to uniquely distinguish variables. │ │ │ │ │ Typically this would be int (if variables are used for Functional::IR nodes) or IdString. │ │ │ │ │ • The derived class should provide a constructor that calls reserve for every reserved word in the target │ │ │ │ │ @@ -15715,28 +15718,28 @@ │ │ │ │ │ • writer.push() and writer.pop() are used to automatically close s-expressions. writer.pop() closes │ │ │ │ │ all s-expressions opened since the last call to writer.push(). │ │ │ │ │ • writer.comment(string) writes a comment on a separate-line. writer.comment(string, true) │ │ │ │ │ appends a comment to the last printed s-expression. │ │ │ │ │ • writer.flush() flushes any buffering and should be called before any direct access to the underlying │ │ │ │ │ std::ostream. It does not close unclosed parentheses. │ │ │ │ │ • The destructor calls flush but also closes all unclosed parentheses. │ │ │ │ │ -Example: A minimal functional backend │ │ │ │ │ -At its most basic, there are three steps we need to accomplish for a minimal functional backend. │ │ │ │ │ -First, we need to convert our design into FunctionalIR. This is most easily done by calling the │ │ │ │ │ -Functional::IR::from_module() static method with our top-level module, or iterating over and converting │ │ │ │ │ -each of the modules in our design. Second, we need to handle each of the Functional::Nodes in our design. │ │ │ │ │ -Iterating over the Functional::IR includes reading the module inputs and current state, but not writing │ │ │ │ │ -the results. So our final step is to handle the outputs and next state. │ │ │ │ │ │ │ │ │ │ 4.3. Working with the Yosys codebase │ │ │ │ │ │ │ │ │ │ 175 │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ +Example: A minimal functional backend │ │ │ │ │ +At its most basic, there are three steps we need to accomplish for a minimal functional backend. │ │ │ │ │ +First, we need to convert our design into FunctionalIR. This is most easily done by calling the │ │ │ │ │ +Functional::IR::from_module() static method with our top-level module, or iterating over and converting │ │ │ │ │ +each of the modules in our design. Second, we need to handle each of the Functional::Nodes in our design. │ │ │ │ │ +Iterating over the Functional::IR includes reading the module inputs and current state, but not writing │ │ │ │ │ +the results. So our final step is to handle the outputs and next state. │ │ │ │ │ In order to add an output command to Yosys, we implement the Yosys::Backend class and provide an │ │ │ │ │ instance of it: │ │ │ │ │ Listing 4.8: Example source code for a minimal functional backend, │ │ │ │ │ dummy.cc │ │ │ │ │ # include "kernel/functional.h" │ │ │ │ │ # include "kernel/yosys.h" │ │ │ │ │ USING_YOSYS_NAMESPACE │ │ │ │ │ @@ -15758,40 +15761,42 @@ │ │ │ │ │ auto ir = Functional::IR::from_module(module); │ │ │ │ │ *f << "module " << module->name.c_str() << "\n"; │ │ │ │ │ // write node functions │ │ │ │ │ for (auto node : ir) │ │ │ │ │ *f << " assign " << id2cstr(node.name()) │ │ │ │ │ << " = " << node.to_string() << "\n"; │ │ │ │ │ *f << "\n"; │ │ │ │ │ - │ │ │ │ │ -"; │ │ │ │ │ - │ │ │ │ │ // write outputs and next state │ │ │ │ │ for (auto output : ir.outputs()) │ │ │ │ │ *f << " " << id2cstr(output->kind) │ │ │ │ │ << " " << id2cstr(output->name) │ │ │ │ │ << " = " << id2cstr(output->value().name()) << "\n"; │ │ │ │ │ for (auto state : ir.states()) │ │ │ │ │ *f << " " << id2cstr(state->kind) │ │ │ │ │ +(continues on next page) │ │ │ │ │ + │ │ │ │ │ +176 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ +(continued from previous page) │ │ │ │ │ + │ │ │ │ │ << " " << id2cstr(state->name) │ │ │ │ │ << " = " << id2cstr(state->next_value().name()) << "\n │ │ │ │ │ │ │ │ │ │ +"; │ │ │ │ │ + │ │ │ │ │ ˓→ │ │ │ │ │ │ │ │ │ │ } │ │ │ │ │ } │ │ │ │ │ } FunctionalDummyBackend; │ │ │ │ │ PRIVATE_NAMESPACE_END │ │ │ │ │ - │ │ │ │ │ -176 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ Because we are using the Backend class, our "functional_dummy" is registered as the │ │ │ │ │ write_functional_dummy command. The execute method is the part that runs when the user calls │ │ │ │ │ the command, handling any options, preparing the output file for writing, and iterating over selected │ │ │ │ │ modules in the design. Since we don’t have any options here, we set argidx = 1 and call the extra_args() │ │ │ │ │ method. This method will read the command arguments, raising an error if there are any unexpected ones. │ │ │ │ │ It will also assign the pointer f to the output file, or stdout if none is given. │ │ │ │ │ ò Note │ │ │ │ │ @@ -15816,28 +15821,27 @@ │ │ │ │ │ write_functional_smt2 output. As a result, the SMT-LIB functional backend can be used as a starting point for implementing a Rosette backend. │ │ │ │ │ Full code listings for the initial SMT-LIB backend and the converted Rosette backend are included in the │ │ │ │ │ Yosys source repository under backends/functional as smtlib.cc and smtlib_rosette.cc respectively. │ │ │ │ │ Note that the Rosette language is an extension of the Racket language; this guide tends to refer to Racket │ │ │ │ │ when talking about the underlying semantics/syntax of the language. │ │ │ │ │ The major changes from the SMT-LIB backend are as follows: │ │ │ │ │ • all of the Smt prefixes in names are replaced with Smtr to mean smtlib_rosette; │ │ │ │ │ +4.3. Working with the Yosys codebase │ │ │ │ │ + │ │ │ │ │ +177 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ • syntax is adjusted for Racket; │ │ │ │ │ • data structures for input/output/state are changed from using declare-datatype with statically typed │ │ │ │ │ fields, to using struct with no static typing; │ │ │ │ │ • the transfer function also loses its static typing; │ │ │ │ │ • sign/zero extension in Rosette use the output width instead of the number of extra bits, gaining static │ │ │ │ │ typing; │ │ │ │ │ • the single scope is traded for a global scope with local scope for each struct; │ │ │ │ │ - │ │ │ │ │ -4.3. Working with the Yosys codebase │ │ │ │ │ - │ │ │ │ │ -177 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ • initial state is provided as a constant value instead of a set of assertions; │ │ │ │ │ • and the -provides option is introduced to more easily use generated code within Rosette based applications. │ │ │ │ │ Scope │ │ │ │ │ Our first addition to the minimal backend above is that for both SMT-LIB and Rosette backends, we are │ │ │ │ │ now targetting real languages which bring with them their own sets of constraints with what we can use │ │ │ │ │ as identifiers. This is where the Functional::Scope class described above comes in; by using this class │ │ │ │ │ we can safely rename our identifiers in the generated output without worrying about collisions or illegal │ │ │ │ │ @@ -15867,37 +15871,32 @@ │ │ │ │ │ } │ │ │ │ │ }; │ │ │ │ │ For the reserved keywords we trade the SMT-LIB specification for Racket to prevent parts of our design │ │ │ │ │ from accidentally being treated as Racket code. We also no longer need to reserve pair, first, and second. │ │ │ │ │ In write_functional_smt2 these are used for combining the (inputs, current_state) and (outputs, │ │ │ │ │ next_state) into a single variable. Racket provides this functionality natively with cons, which we will see │ │ │ │ │ later. │ │ │ │ │ -Listing 4.10: diff of reserved_keywords list │ │ │ │ │ -const char *reserved_keywords[] = { │ │ │ │ │ -- // reserved keywords from the smtlib spec │ │ │ │ │ -- ... │ │ │ │ │ -+ // reserved keywords from the racket spec │ │ │ │ │ -+ ... │ │ │ │ │ -- │ │ │ │ │ - │ │ │ │ │ -// reserved for our own purposes │ │ │ │ │ -"pair", "Pair", "first", "second", │ │ │ │ │ -(continues on next page) │ │ │ │ │ │ │ │ │ │ 178 │ │ │ │ │ │ │ │ │ │ Chapter 4. Yosys internals │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ +Listing 4.10: diff of reserved_keywords list │ │ │ │ │ +const char *reserved_keywords[] = { │ │ │ │ │ +- // reserved keywords from the smtlib spec │ │ │ │ │ +- ... │ │ │ │ │ ++ // reserved keywords from the racket spec │ │ │ │ │ ++ ... │ │ │ │ │ + │ │ │ │ │ }; │ │ │ │ │ │ │ │ │ │ +// reserved for our own purposes │ │ │ │ │ +"pair", "Pair", "first", "second", │ │ │ │ │ "inputs", "state", │ │ │ │ │ "inputs", "state", "name", │ │ │ │ │ nullptr │ │ │ │ │ │ │ │ │ │ ò Note │ │ │ │ │ We skip over the actual list of reserved keywords from both the smtlib and racket specifications to save │ │ │ │ │ on space in this document. │ │ │ │ │ @@ -15924,49 +15923,42 @@ │ │ │ │ │ } │ │ │ │ │ Struct │ │ │ │ │ As we saw in the minimal backend above, the Functional::IR class tracks the set of inputs, the set of outputs, and the set of “state” variables. The SMT-LIB backend maps each of these sets into its own SmtStruct, │ │ │ │ │ with each variable getting a corresponding field in the struct and a specified Sort. write_functional_smt2 │ │ │ │ │ then defines each of these structs as a new datatype, with each element being strongly-typed. │ │ │ │ │ In Rosette, rather than defining new datatypes for our structs, we use the native struct. We also only │ │ │ │ │ declare each field by name because Racket provides less static typing. For ease of use, we provide the │ │ │ │ │ -expected type for each field as comments. │ │ │ │ │ -Listing 4.12: diff of write_definition method │ │ │ │ │ -- │ │ │ │ │ - │ │ │ │ │ -void write_definition(SExprWriter &w) { │ │ │ │ │ -w.open(list("declare-datatype", name)); │ │ │ │ │ -w.open(list()); │ │ │ │ │ -w.open(list(name)); │ │ │ │ │ -for(const auto &field : fields) │ │ │ │ │ -(continues on next page) │ │ │ │ │ │ │ │ │ │ 4.3. Working with the Yosys codebase │ │ │ │ │ │ │ │ │ │ 179 │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ +expected type for each field as comments. │ │ │ │ │ +Listing 4.12: diff of write_definition method │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ -} │ │ │ │ │ - │ │ │ │ │ +void write_definition(SExprWriter &w) { │ │ │ │ │ +w.open(list("declare-datatype", name)); │ │ │ │ │ +w.open(list()); │ │ │ │ │ +w.open(list(name)); │ │ │ │ │ +for(const auto &field : fields) │ │ │ │ │ w << list(field.accessor, field.sort.to_sexpr()); │ │ │ │ │ w.close(3); │ │ │ │ │ vector field_list; │ │ │ │ │ for(const auto &field : fields) { │ │ │ │ │ field_list.emplace_back(field.name); │ │ │ │ │ } │ │ │ │ │ w.push(); │ │ │ │ │ @@ -15974,14 +15966,15 @@ │ │ │ │ │ if (field_names.size()) { │ │ │ │ │ for (const auto &field : fields) { │ │ │ │ │ auto bv_type = field.sort.to_sexpr(); │ │ │ │ │ w.comment(field.name + " " + bv_type.to_string()); │ │ │ │ │ } │ │ │ │ │ } │ │ │ │ │ w.pop(); │ │ │ │ │ +} │ │ │ │ │ │ │ │ │ │ Each field is added to the SmtStruct with the insert method, which also reserves a unique name (or accessor) │ │ │ │ │ within the Scope. These accessors combine the struct name and field name and are globally unique, being │ │ │ │ │ used in the access method for reading values from the input/current state. │ │ │ │ │ Listing 4.13: Struct::access() method │ │ │ │ │ SExpr access(SExpr record, IdString name) { │ │ │ │ │ size_t i = field_names.at(name); │ │ │ │ │ @@ -16001,33 +15994,38 @@ │ │ │ │ │ ˓→scope(), name(name) {} │ │ │ │ │ + │ │ │ │ │ void insert(IdString field_name, SmtrSort sort) { │ │ │ │ │ field_names(field_name); │ │ │ │ │ auto accessor = scope.unique_name("\\" + name + "_" + RTLIL::unescape_ │ │ │ │ │ ˓→id(field_name)); │ │ │ │ │ fields.emplace_back(Field{sort, accessor}); │ │ │ │ │ +(continues on next page) │ │ │ │ │ + │ │ │ │ │ +180 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ +(continued from previous page) │ │ │ │ │ + │ │ │ │ │ + │ │ │ │ │ -auto base_name = local_scope.unique_name(field_name); │ │ │ │ │ + │ │ │ │ │ -auto accessor = name + "-" + base_name; │ │ │ │ │ + │ │ │ │ │ -global_scope.reserve(accessor); │ │ │ │ │ + │ │ │ │ │ -fields.emplace_back(Field{sort, accessor, base_name}); │ │ │ │ │ + │ │ │ │ │ } │ │ │ │ │ │ │ │ │ │ +auto base_name = local_scope.unique_name(field_name); │ │ │ │ │ +auto accessor = name + "-" + base_name; │ │ │ │ │ +global_scope.reserve(accessor); │ │ │ │ │ +fields.emplace_back(Field{sort, accessor, base_name}); │ │ │ │ │ + │ │ │ │ │ Finally, SmtStruct also provides a write_value template method which calls a provided function on each │ │ │ │ │ element in the struct. This is used later for assigning values to the output/next state pair. The only change │ │ │ │ │ - │ │ │ │ │ -180 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ here is to remove the check for zero-argument constructors since this is not necessary with Rosette structs. │ │ │ │ │ Listing 4.15: diff of write_value method │ │ │ │ │ template void write_value(SExprWriter &w, Fn fn) { │ │ │ │ │ if(field_names.empty()) { │ │ │ │ │ // Zero-argument constructors in SMTLIB must not be called as␣ │ │ │ │ │ ˓→functions. │ │ │ │ │ w << name; │ │ │ │ │ @@ -16065,63 +16063,71 @@ │ │ │ │ │ SExpr logical_shift_right(Node, Node a, Node b) override { return list("bvlshr", │ │ │ │ │ ˓→ n(a), extend(n(b), b.width(), a.width())); } │ │ │ │ │ SExpr arithmetic_shift_right(Node, Node a, Node b) override { return list( │ │ │ │ │ ˓→"bvashr", n(a), extend(n(b), b.width(), a.width())); } │ │ │ │ │ SExpr mux(Node, Node a, Node b, Node s) override { return list("ite", to_ │ │ │ │ │ ˓→bool(n(s)), n(b), n(a)); } │ │ │ │ │ SExpr constant(Node, RTLIL::Const const &value) override { return smt_ │ │ │ │ │ -˓→const(value); } │ │ │ │ │ -SExpr memory_read(Node, Node mem, Node addr) override { return list("select",␣ │ │ │ │ │ -˓→n(mem), n(addr)); } │ │ │ │ │ -SExpr memory_write(Node, Node mem, Node addr, Node data) override { return list( │ │ │ │ │ -˓→"store", n(mem), n(addr), n(data)); } │ │ │ │ │ -+ │ │ │ │ │ -SExpr mux(Node, Node a, Node b, Node s) override { return list("if", to_ │ │ │ │ │ -˓→bool(n(s)), n(b), n(a)); } │ │ │ │ │ -+ │ │ │ │ │ -SExpr constant(Node, RTLIL::Const const& value) override { return list("bv",␣ │ │ │ │ │ -˓→smt_const(value), value.size()); } │ │ │ │ │ ˓→ │ │ │ │ │ │ │ │ │ │ (continues on next page) │ │ │ │ │ │ │ │ │ │ 4.3. Working with the Yosys codebase │ │ │ │ │ │ │ │ │ │ 181 │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ (continued from previous page) │ │ │ │ │ │ │ │ │ │ +const(value); } │ │ │ │ │ +SExpr memory_read(Node, Node mem, Node addr) override { return list("select",␣ │ │ │ │ │ +˓→n(mem), n(addr)); } │ │ │ │ │ +SExpr memory_write(Node, Node mem, Node addr, Node data) override { return list( │ │ │ │ │ +˓→"store", n(mem), n(addr), n(data)); } │ │ │ │ │ ++ │ │ │ │ │ +SExpr mux(Node, Node a, Node b, Node s) override { return list("if", to_ │ │ │ │ │ +˓→bool(n(s)), n(b), n(a)); } │ │ │ │ │ ++ │ │ │ │ │ +SExpr constant(Node, RTLIL::Const const& value) override { return list("bv",␣ │ │ │ │ │ +˓→smt_const(value), value.size()); } │ │ │ │ │ + │ │ │ │ │ - │ │ │ │ │ SExpr memory_read(Node, Node mem, Node addr) override { return list("list-ref-bv │ │ │ │ │ -", n(mem), n(addr)); } │ │ │ │ │ +˓→", n(mem), n(addr)); } │ │ │ │ │ + │ │ │ │ │ SExpr memory_write(Node, Node mem, Node addr, Node data) override { return list( │ │ │ │ │ ˓→"list-set-bv", n(mem), n(addr), n(data)); } │ │ │ │ │ ˓→ │ │ │ │ │ │ │ │ │ │ +- │ │ │ │ │ + │ │ │ │ │ However there are some differences in the two formats with regards to how booleans are handled, with │ │ │ │ │ Rosette providing built-in functions for conversion. │ │ │ │ │ Listing 4.17: portion of Functional::AbstractVisitor implementation diff showing differences │ │ │ │ │ ++ │ │ │ │ │ ++ │ │ │ │ │ + │ │ │ │ │ SExpr from_bool(SExpr &&arg) { │ │ │ │ │ return list("ite", std::move(arg), "#b1", "#b0"); │ │ │ │ │ return list("bool->bitvector", std::move(arg)); │ │ │ │ │ } │ │ │ │ │ SExpr to_bool(SExpr &&arg) { │ │ │ │ │ return list("=", std::move(arg), "#b1"); │ │ │ │ │ return list("bitvector->bool", std::move(arg)); │ │ │ │ │ } │ │ │ │ │ │ │ │ │ │ -+ │ │ │ │ │ -+ │ │ │ │ │ - │ │ │ │ │ Of note here is the rare instance of the Rosette implementation gaining static typing rather than losing it. │ │ │ │ │ Where SMT_LIB calls zero/sign extension with the number of extra bits needed (given by out_width a.width()), Rosette instead specifies the type of the output (given by list("bitvector", out_width)). │ │ │ │ │ + │ │ │ │ │ +182 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ Listing 4.18: zero/sign extension implementation diff │ │ │ │ │ - │ │ │ │ │ │ │ │ │ │ SExpr zero_extend(Node, Node a, int out_width) override { return list(list("_", │ │ │ │ │ "zero_extend", out_width - a.width()), n(a)); } │ │ │ │ │ SExpr sign_extend(Node, Node a, int out_width) override { return list(list("_", │ │ │ │ │ ˓→"sign_extend", out_width - a.width()), n(a)); } │ │ │ │ │ @@ -16138,55 +16144,44 @@ │ │ │ │ │ backend. These are all handled by the SmtModule class, with the mapping from RTLIL module to FunctionalIR happening in the constructor. Each of the three SmtStructs; inputs, outputs, and state; are also │ │ │ │ │ created in the constructor, with each value in the corresponding lists in the IR being inserted. │ │ │ │ │ Listing 4.19: SmtModule constructor │ │ │ │ │ SmtModule(Module *module) │ │ │ │ │ : ir(Functional::IR::from_module(module)) │ │ │ │ │ , scope() │ │ │ │ │ , name(scope.unique_name(module->name)) │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -182 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ , input_struct(scope.unique_name(module->name.str() + "_Inputs"), scope) │ │ │ │ │ , output_struct(scope.unique_name(module->name.str() + "_Outputs"),␣ │ │ │ │ │ - │ │ │ │ │ -scope) │ │ │ │ │ - │ │ │ │ │ -˓→ │ │ │ │ │ - │ │ │ │ │ -{ │ │ │ │ │ - │ │ │ │ │ -} │ │ │ │ │ - │ │ │ │ │ +˓→scope) │ │ │ │ │ , state_struct(scope.unique_name(module->name.str() + "_State"), scope) │ │ │ │ │ +{ │ │ │ │ │ scope.reserve(name + "-initial"); │ │ │ │ │ for (auto input : ir.inputs()) │ │ │ │ │ input_struct.insert(input->name, input->sort); │ │ │ │ │ for (auto output : ir.outputs()) │ │ │ │ │ output_struct.insert(output->name, output->sort); │ │ │ │ │ for (auto state : ir.states()) │ │ │ │ │ state_struct.insert(state->name, state->sort); │ │ │ │ │ - │ │ │ │ │ +} │ │ │ │ │ Since Racket uses the - to access struct fields, the SmtrModule instead uses an underscore for the name of │ │ │ │ │ the initial state. │ │ │ │ │ Listing 4.20: diff of Module constructor │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ scope.reserve(name + "-initial"); │ │ │ │ │ scope.reserve(name + "_initial"); │ │ │ │ │ │ │ │ │ │ The write method is then responsible for writing the FunctionalIR to the output file, formatted for the │ │ │ │ │ corresponding backend. SmtModule::write() breaks the output file down into four parts: defining the │ │ │ │ │ three structs, declaring the pair datatype, defining the transfer function (inputs, current_state) -> │ │ │ │ │ +4.3. Working with the Yosys codebase │ │ │ │ │ + │ │ │ │ │ +183 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ (outputs, next_state) with write_eval, and declaring the initial state with write_initial. The only │ │ │ │ │ change for the SmtrModule is that the pair declaration isn’t needed. │ │ │ │ │ Listing 4.21: diff of Module::write() method │ │ │ │ │ void write(std::ostream &out) │ │ │ │ │ { │ │ │ │ │ SExprWriter w(out); │ │ │ │ │ input_struct.write_definition(w); │ │ │ │ │ @@ -16201,21 +16196,14 @@ │ │ │ │ │ write_eval(w); │ │ │ │ │ write_initial(w); │ │ │ │ │ } │ │ │ │ │ The write_eval method is where the FunctionalIR nodes, outputs, and next state are handled. Just │ │ │ │ │ as with the minimal backend, we iterate over the nodes with for(auto n : ir), and then use the │ │ │ │ │ Struct::write_value() method for the output_struct and state_struct to iterate over the outputs │ │ │ │ │ and next state respectively. │ │ │ │ │ - │ │ │ │ │ -4.3. Working with the Yosys codebase │ │ │ │ │ - │ │ │ │ │ -183 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ Listing 4.22: │ │ │ │ │ iterating │ │ │ │ │ SmtModule::write_eval() │ │ │ │ │ │ │ │ │ │ over │ │ │ │ │ │ │ │ │ │ FunctionalIR │ │ │ │ │ @@ -16234,19 +16222,26 @@ │ │ │ │ │ The main differences between our two backends here are syntactical. First we change the define-fun for │ │ │ │ │ the Racket style define which drops the explicitly typed inputs/outputs. And then we change the final │ │ │ │ │ result from a pair to the native cons which acts in much the same way, returning both the outputs and │ │ │ │ │ the next_state in a single variable. │ │ │ │ │ Listing 4.23: diff of Module::write_eval() transfer function declaration │ │ │ │ │ + │ │ │ │ │ │ │ │ │ │ +184 │ │ │ │ │ + │ │ │ │ │ w.open(list("define-fun", name, │ │ │ │ │ list(list("inputs", input_struct.name), │ │ │ │ │ list("state", state_struct.name)), │ │ │ │ │ list("Pair", output_struct.name, state_struct.name))); │ │ │ │ │ w.open(list("define", list(name, "inputs", "state"))); │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ Listing │ │ │ │ │ 4.24: │ │ │ │ │ diff │ │ │ │ │ Module::write_eval() │ │ │ │ │ │ │ │ │ │ of │ │ │ │ │ │ │ │ │ │ @@ -16268,41 +16263,27 @@ │ │ │ │ │ │ │ │ │ │ For the write_initial method, the SMT-LIB backend uses declare-const and asserts which must always │ │ │ │ │ hold true. For Rosette we instead define the initial state as any other variable that can be used by external │ │ │ │ │ code. This variable, [name]_initial, can then be used in the [name] function call; allowing the Rosette │ │ │ │ │ code to be used in the generation of the next_state, whereas the SMT-LIB code can only verify that a │ │ │ │ │ given next_state is correct. │ │ │ │ │ Listing 4.25: diff of Module::write_initial() method │ │ │ │ │ - │ │ │ │ │ -+ │ │ │ │ │ -+ │ │ │ │ │ -+ │ │ │ │ │ -+ │ │ │ │ │ - │ │ │ │ │ void write_initial(SExprWriter &w) │ │ │ │ │ { │ │ │ │ │ std::string initial = name + "-initial"; │ │ │ │ │ w << list("declare-const", initial, state_struct.name); │ │ │ │ │ ++ │ │ │ │ │ w.push(); │ │ │ │ │ ++ │ │ │ │ │ auto initial = name + "_initial"; │ │ │ │ │ ++ │ │ │ │ │ w.open(list("define", initial)); │ │ │ │ │ ++ │ │ │ │ │ w.open(list(state_struct.name)); │ │ │ │ │ for (auto state : ir.states()) { │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -184 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ -- │ │ │ │ │ - │ │ │ │ │ if(state->sort.is_signal()) │ │ │ │ │ w << list("assert", list("=", state_struct. │ │ │ │ │ ˓→access(initial, state->name), smt_const(state->initial_value_signal()))); │ │ │ │ │ else if(state->sort.is_memory()) { │ │ │ │ │ + │ │ │ │ │ if (state->sort.is_signal()) │ │ │ │ │ + │ │ │ │ │ @@ -16326,14 +16307,20 @@ │ │ │ │ │ w.close(); │ │ │ │ │ } │ │ │ │ │ } │ │ │ │ │ + │ │ │ │ │ w.pop(); │ │ │ │ │ } │ │ │ │ │ │ │ │ │ │ +4.3. Working with the Yosys codebase │ │ │ │ │ + │ │ │ │ │ +185 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ Backend │ │ │ │ │ The final part is the Backend itself, with much of the same boiler plate as the minimal backend. The main │ │ │ │ │ difference is that we use the Module to perform the actual processing. │ │ │ │ │ Listing 4.26: The FunctionalSmtBackend │ │ │ │ │ struct FunctionalSmtBackend : public Backend { │ │ │ │ │ FunctionalSmtBackend() : Backend("functional_smt2", "Generate SMT-LIB from␣ │ │ │ │ │ ˓→Functional IR") {} │ │ │ │ │ @@ -16343,33 +16330,23 @@ │ │ │ │ │ { │ │ │ │ │ log_header(design, "Executing Functional SMT Backend.\n"); │ │ │ │ │ │ │ │ │ │ ˓→ │ │ │ │ │ │ │ │ │ │ size_t argidx = 1; │ │ │ │ │ extra_args(f, filename, args, argidx, design); │ │ │ │ │ - │ │ │ │ │ -} │ │ │ │ │ - │ │ │ │ │ for (auto module : design->selected_modules()) { │ │ │ │ │ log("Processing module `%s`.\n", module->name.c_str()); │ │ │ │ │ SmtModule smt(module); │ │ │ │ │ smt.write(*f); │ │ │ │ │ } │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -4.3. Working with the Yosys codebase │ │ │ │ │ - │ │ │ │ │ -185 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ │ │ │ │ │ +} │ │ │ │ │ } FunctionalSmtBackend; │ │ │ │ │ + │ │ │ │ │ There are two additions here for Rosette. The first is that the output file needs to start with the #lang │ │ │ │ │ definition which tells the compiler/interpreter that we want to use the Rosette language module. The second │ │ │ │ │ is that the write_functional_rosette command takes an optional argument, -provides. If this argument │ │ │ │ │ is given, then the output file gets an additional line declaring that everything in the file should be exported │ │ │ │ │ for use; allowing the file to be treated as a Racket package with structs and mapping function available for │ │ │ │ │ use externally. │ │ │ │ │ Listing 4.27: relevant portion of diff of Backend::execute() │ │ │ │ │ @@ -16384,14 +16361,21 @@ │ │ │ │ │ *f << "(provide (all-defined-out))\n"; │ │ │ │ │ } │ │ │ │ │ │ │ │ │ │ 4.3.4 Contributing to Yosys │ │ │ │ │ ò Note │ │ │ │ │ For information on making a pull request on github, refer to our CONTRIBUTING.md file. │ │ │ │ │ Coding Style │ │ │ │ │ + │ │ │ │ │ +186 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ Formatting of code │ │ │ │ │ • Yosys code is using tabs for indentation. Tabs are 8 characters. │ │ │ │ │ • A continuation of a statement in the following line is indented by two additional tabs. │ │ │ │ │ • Lines are as long as you want them to be. A good rule of thumb is to break lines at about column 150. │ │ │ │ │ • Opening braces can be put on the same or next line as the statement opening the block (if, switch, │ │ │ │ │ for, while, do). Put the opening brace on its own line for larger blocks, especially blocks that contains │ │ │ │ │ blank lines. │ │ │ │ │ @@ -16401,21 +16385,14 @@ │ │ │ │ │ In general Yosys uses int instead of size_t. To avoid compiler warnings for implicit type casts, always use │ │ │ │ │ GetSize(foobar) instead of foobar.size(). (GetSize() is defined in kernel/yosys.h) │ │ │ │ │ Use range-based for loops whenever applicable. │ │ │ │ │ │ │ │ │ │ 4.3.5 Testing Yosys │ │ │ │ │ v Todo │ │ │ │ │ more about the included test suite and how to add tests │ │ │ │ │ - │ │ │ │ │ -186 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ Automatic testing │ │ │ │ │ The Yosys Git repo has automatic testing of builds and running of the included test suite on both Ubuntu │ │ │ │ │ and macOS, as well as across range of compiler versions. For up to date information, including OS versions, │ │ │ │ │ refer to the git actions page. │ │ │ │ │ v Todo │ │ │ │ │ are unit tests currently working │ │ │ │ │ │ │ │ │ │ @@ -16426,14 +16403,20 @@ │ │ │ │ │ • Verilog parameters are used extensively to customize the internal cell types. │ │ │ │ │ • Additional special parameters are used by techmap to communicate meta-data to the map files. │ │ │ │ │ • Special wires are used to instruct techmap how to handle a module in the map file. │ │ │ │ │ • Generate blocks and recursion are powerful tools for writing map files. │ │ │ │ │ Code examples used in this document are included in the Yosys code base under docs/source/ │ │ │ │ │ code_examples/techmap. │ │ │ │ │ │ │ │ │ │ +4.4. Techmap by example │ │ │ │ │ + │ │ │ │ │ +187 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ 4.4.1 Mapping OR3X1 │ │ │ │ │ v Todo │ │ │ │ │ add/expand supporting text │ │ │ │ │ │ │ │ │ │ ò Note │ │ │ │ │ This is a simple example for demonstration only. Techmap shouldn’t be used to implement basic logic │ │ │ │ │ optimization. │ │ │ │ │ @@ -16443,24 +16426,14 @@ │ │ │ │ │ parameter A_SIGNED = 0; │ │ │ │ │ parameter A_WIDTH = 0; │ │ │ │ │ parameter Y_WIDTH = 0; │ │ │ │ │ input [A_WIDTH-1:0] A; │ │ │ │ │ output [Y_WIDTH-1:0] Y; │ │ │ │ │ function integer min; │ │ │ │ │ input integer a, b; │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -4.4. Techmap by example │ │ │ │ │ - │ │ │ │ │ -187 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ begin │ │ │ │ │ if (a < b) │ │ │ │ │ min = a; │ │ │ │ │ else │ │ │ │ │ min = b; │ │ │ │ │ end │ │ │ │ │ endfunction │ │ │ │ │ @@ -16478,14 +16451,24 @@ │ │ │ │ │ assign Y = ybuf; │ │ │ │ │ end │ │ │ │ │ if (A_WIDTH == 3) begin │ │ │ │ │ wire ybuf; │ │ │ │ │ OR3X1 g (.A(A[0]), .B(A[1]), .C(A[2]), .Y(ybuf)); │ │ │ │ │ assign Y = ybuf; │ │ │ │ │ end │ │ │ │ │ +(continues on next page) │ │ │ │ │ + │ │ │ │ │ +188 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ +(continued from previous page) │ │ │ │ │ + │ │ │ │ │ if (A_WIDTH > 3) begin │ │ │ │ │ localparam next_stage_sz = (A_WIDTH+2) / 3; │ │ │ │ │ wire [next_stage_sz-1:0] next_stage; │ │ │ │ │ for (i = 0; i < next_stage_sz; i = i+1) begin │ │ │ │ │ localparam bits = min(A_WIDTH - 3*i, 3); │ │ │ │ │ assign next_stage[i] = |A[3*i +: bits]; │ │ │ │ │ end │ │ │ │ │ @@ -16502,16 +16485,14 @@ │ │ │ │ │ │ │ │ │ │ A[3] │ │ │ │ │ │ │ │ │ │ A[4] │ │ │ │ │ │ │ │ │ │ A[5] │ │ │ │ │ │ │ │ │ │ -188 │ │ │ │ │ - │ │ │ │ │ A │ │ │ │ │ B │ │ │ │ │ C │ │ │ │ │ │ │ │ │ │ A │ │ │ │ │ B │ │ │ │ │ C │ │ │ │ │ @@ -16522,33 +16503,29 @@ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ $6.genblk0.genblk4.g │ │ │ │ │ OR3X1 │ │ │ │ │ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ -A[6] │ │ │ │ │ - │ │ │ │ │ A │ │ │ │ │ B │ │ │ │ │ C │ │ │ │ │ │ │ │ │ │ $8.genblk0.genblk4.g │ │ │ │ │ OR3X1 │ │ │ │ │ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ +A[6] │ │ │ │ │ + │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ $1.genblk0.genblk5.next_stage[2] │ │ │ │ │ │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ Listing 4.29: red_or3x1_test.ys │ │ │ │ │ read_verilog red_or3x1_test.v │ │ │ │ │ hierarchy -check -top test │ │ │ │ │ techmap -map red_or3x1_map.v;; │ │ │ │ │ splitnets -ports │ │ │ │ │ show -prefix red_or3x1 -format dot -notitle -lib red_or3x1_cells.v │ │ │ │ │ Listing 4.30: red_or3x1_test.v │ │ │ │ │ @@ -16560,27 +16537,31 @@ │ │ │ │ │ │ │ │ │ │ 4.4.2 Conditional techmap │ │ │ │ │ • In some cases only cells with certain properties should be substituted. │ │ │ │ │ • The special wire _TECHMAP_FAIL_ can be used to disable a module in the map file for a certain set of │ │ │ │ │ parameters. │ │ │ │ │ • The wire _TECHMAP_FAIL_ must be set to a constant value. If it is non-zero then the module is disabled │ │ │ │ │ for this set of parameters. │ │ │ │ │ +4.4. Techmap by example │ │ │ │ │ + │ │ │ │ │ +189 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ • Example use-cases: │ │ │ │ │ – coarse-grain cell types that only operate on certain bit widths │ │ │ │ │ – memory resources for different memory geometries (width, depth, ports, etc.) │ │ │ │ │ Example: │ │ │ │ │ │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ A │ │ │ │ │ │ │ │ │ │ C │ │ │ │ │ │ │ │ │ │ -4.4. Techmap by example │ │ │ │ │ - │ │ │ │ │ A │ │ │ │ │ │ │ │ │ │ $1.g │ │ │ │ │ MYMUL │ │ │ │ │ │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ @@ -16588,23 +16569,19 @@ │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ $2 │ │ │ │ │ $mul │ │ │ │ │ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ -Y │ │ │ │ │ - │ │ │ │ │ Y1 │ │ │ │ │ │ │ │ │ │ -Y2 │ │ │ │ │ - │ │ │ │ │ -189 │ │ │ │ │ +Y │ │ │ │ │ │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ +Y2 │ │ │ │ │ │ │ │ │ │ Listing 4.31: sym_mul_map.v │ │ │ │ │ module \$mul (A, B, Y); │ │ │ │ │ parameter A_SIGNED = 0; │ │ │ │ │ parameter B_SIGNED = 0; │ │ │ │ │ parameter A_WIDTH = 1; │ │ │ │ │ parameter B_WIDTH = 1; │ │ │ │ │ @@ -16618,14 +16595,21 @@ │ │ │ │ │ Listing 4.32: sym_mul_test.v │ │ │ │ │ module test(A, B, C, Y1, Y2); │ │ │ │ │ input │ │ │ │ │ [7:0] A, B, C; │ │ │ │ │ output [7:0] Y1 = A * B; │ │ │ │ │ output [15:0] Y2 = A * C; │ │ │ │ │ endmodule │ │ │ │ │ + │ │ │ │ │ +190 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ Listing 4.33: sym_mul_test.ys │ │ │ │ │ read_verilog sym_mul_test.v │ │ │ │ │ hierarchy -check -top test │ │ │ │ │ techmap -map sym_mul_map.v;; │ │ │ │ │ show -prefix sym_mul -format dot -notitle -lib sym_mul_cells.v │ │ │ │ │ │ │ │ │ │ 4.4.3 Scripting in map modules │ │ │ │ │ @@ -16635,21 +16619,14 @@ │ │ │ │ │ that is executed as script. Then the wire is removed. Repeat. │ │ │ │ │ • You can even call techmap recursively! │ │ │ │ │ • Example use-cases: │ │ │ │ │ – Using always blocks in map module: call proc │ │ │ │ │ – Perform expensive optimizations (such as freduce ) on cells where this is known to work well. │ │ │ │ │ – Interacting with custom commands. │ │ │ │ │ ò Note │ │ │ │ │ - │ │ │ │ │ -190 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ PROTIP: │ │ │ │ │ Commands such as shell , show -pause, and dump can be used in the _TECHMAP_DO_* scripts for debugging map modules. │ │ │ │ │ Example: │ │ │ │ │ │ │ │ │ │ 2'00 │ │ │ │ │ 2'00 │ │ │ │ │ │ │ │ │ │ @@ -16666,19 +16643,19 @@ │ │ │ │ │ S │ │ │ │ │ │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ $15 │ │ │ │ │ $mux │ │ │ │ │ │ │ │ │ │ -Y │ │ │ │ │ - │ │ │ │ │ A[0] │ │ │ │ │ │ │ │ │ │ +Y │ │ │ │ │ A │ │ │ │ │ + │ │ │ │ │ 0:0 - 1:1 │ │ │ │ │ │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ $10 │ │ │ │ │ $add │ │ │ │ │ │ │ │ │ │ @@ -16695,14 +16672,20 @@ │ │ │ │ │ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ A[1] │ │ │ │ │ │ │ │ │ │ +4.4. Techmap by example │ │ │ │ │ + │ │ │ │ │ +191 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ Listing 4.34: mymul_map.v │ │ │ │ │ module MYMUL(A, B, Y); │ │ │ │ │ parameter WIDTH = 1; │ │ │ │ │ input [WIDTH-1:0] A, B; │ │ │ │ │ output reg [WIDTH-1:0] Y; │ │ │ │ │ wire [1023:0] _TECHMAP_DO_ = "proc; clean"; │ │ │ │ │ integer i; │ │ │ │ │ @@ -16717,24 +16700,14 @@ │ │ │ │ │ module test(A, B, Y); │ │ │ │ │ input [1:0] A, B; │ │ │ │ │ output [1:0] Y = A * B; │ │ │ │ │ endmodule │ │ │ │ │ Listing 4.36: mymul_test.ys │ │ │ │ │ read_verilog mymul_test.v │ │ │ │ │ hierarchy -check -top test │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -4.4. Techmap by example │ │ │ │ │ - │ │ │ │ │ -191 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ techmap -map sym_mul_map.v \ │ │ │ │ │ -map mymul_map.v;; │ │ │ │ │ rename test test_mapped │ │ │ │ │ read_verilog mymul_test.v │ │ │ │ │ miter -equiv test test_mapped miter │ │ │ │ │ flatten miter │ │ │ │ │ sat -verify -prove trigger 0 miter │ │ │ │ │ @@ -16744,14 +16717,21 @@ │ │ │ │ │ 4.4.4 Handling constant inputs │ │ │ │ │ • The special parameters _TECHMAP_CONSTMSK__ and _TECHMAP_CONSTVAL__ │ │ │ │ │ can be used to handle constant input values to cells. │ │ │ │ │ • The former contains 1-bits for all constant input bits on the port. │ │ │ │ │ • The latter contains the constant bits or undef (x) for non-constant bits. │ │ │ │ │ • Example use-cases: │ │ │ │ │ – Converting arithmetic (for example multiply to shift). │ │ │ │ │ + │ │ │ │ │ +192 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ – Identify constant addresses or enable bits in memory interfaces. │ │ │ │ │ Example: │ │ │ │ │ │ │ │ │ │ 4:0 - 7:3 │ │ │ │ │ A │ │ │ │ │ A │ │ │ │ │ 8'00000110 │ │ │ │ │ @@ -16770,24 +16750,14 @@ │ │ │ │ │ X │ │ │ │ │ │ │ │ │ │ Listing 4.37: mulshift_map.v │ │ │ │ │ module MYMUL(A, B, Y); │ │ │ │ │ parameter WIDTH = 1; │ │ │ │ │ input [WIDTH-1:0] A, B; │ │ │ │ │ output reg [WIDTH-1:0] Y; │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -192 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ parameter _TECHMAP_CONSTVAL_A_ = WIDTH'bx; │ │ │ │ │ parameter _TECHMAP_CONSTVAL_B_ = WIDTH'bx; │ │ │ │ │ reg _TECHMAP_FAIL_; │ │ │ │ │ wire [1023:0] _TECHMAP_DO_ = "proc; clean"; │ │ │ │ │ integer i; │ │ │ │ │ always @* begin │ │ │ │ │ _TECHMAP_FAIL_ <= 1; │ │ │ │ │ @@ -16801,14 +16771,24 @@ │ │ │ │ │ Y <= A << i; │ │ │ │ │ end │ │ │ │ │ end │ │ │ │ │ end │ │ │ │ │ endmodule │ │ │ │ │ Listing 4.38: mulshift_test.v │ │ │ │ │ module test (A, X, Y); │ │ │ │ │ +(continues on next page) │ │ │ │ │ + │ │ │ │ │ +4.4. Techmap by example │ │ │ │ │ + │ │ │ │ │ +193 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ +(continued from previous page) │ │ │ │ │ + │ │ │ │ │ input [7:0] A; │ │ │ │ │ output [7:0] X = A * 8'd 6; │ │ │ │ │ output [7:0] Y = A * 8'd 8; │ │ │ │ │ endmodule │ │ │ │ │ Listing 4.39: mulshift_test.ys │ │ │ │ │ read_verilog mulshift_test.v │ │ │ │ │ hierarchy -check -top test │ │ │ │ │ @@ -16829,31 +16809,26 @@ │ │ │ │ │ │ │ │ │ │ in │ │ │ │ │ │ │ │ │ │ the │ │ │ │ │ │ │ │ │ │ • The numbers 0-3 are reserved for 0, 1, x, and z respectively. │ │ │ │ │ • Example use-cases: │ │ │ │ │ - │ │ │ │ │ -4.4. Techmap by example │ │ │ │ │ - │ │ │ │ │ -193 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ – Detecting shared clock or control signals in memory interfaces. │ │ │ │ │ – In some cases this can be used for for optimization. │ │ │ │ │ Example: │ │ │ │ │ │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ A │ │ │ │ │ │ │ │ │ │ 1 │ │ │ │ │ │ │ │ │ │ +194 │ │ │ │ │ + │ │ │ │ │ A │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ A │ │ │ │ │ B │ │ │ │ │ │ │ │ │ │ $1 │ │ │ │ │ @@ -16866,14 +16841,18 @@ │ │ │ │ │ $5 │ │ │ │ │ $shl │ │ │ │ │ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ Y │ │ │ │ │ │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ Listing 4.40: addshift_map.v │ │ │ │ │ module \$add (A, B, Y); │ │ │ │ │ parameter A_SIGNED = 0; │ │ │ │ │ parameter B_SIGNED = 0; │ │ │ │ │ parameter A_WIDTH = 1; │ │ │ │ │ parameter B_WIDTH = 1; │ │ │ │ │ parameter Y_WIDTH = 1; │ │ │ │ │ @@ -16887,24 +16866,14 @@ │ │ │ │ │ _TECHMAP_CONNMAP_A_ != _TECHMAP_CONNMAP_B_; │ │ │ │ │ assign Y = A << 1; │ │ │ │ │ endmodule │ │ │ │ │ Listing 4.41: addshift_test.v │ │ │ │ │ module test (A, B, X, Y); │ │ │ │ │ input [7:0] A, B; │ │ │ │ │ output [7:0] X = A + B; │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -194 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ output [7:0] Y = A + A; │ │ │ │ │ endmodule │ │ │ │ │ Listing 4.42: addshift_test.ys │ │ │ │ │ read_verilog addshift_test.v │ │ │ │ │ hierarchy -check -top test │ │ │ │ │ techmap -map addshift_map.v;; │ │ │ │ │ show -prefix addshift -format dot -notitle │ │ │ │ │ @@ -16914,14 +16883,20 @@ │ │ │ │ │ • You can use the $__-prefix for internal cell types to avoid collisions with the user-namespace. But │ │ │ │ │ always use two underscores or the internal consistency checker will trigger on these cells. │ │ │ │ │ • Techmap has two major use cases: │ │ │ │ │ – Creating good logic-level representation of arithmetic functions. This also means using dedicated │ │ │ │ │ hardware resources such as half- and full-adder cells in ASICS or dedicated carry logic in FPGAs. │ │ │ │ │ – Mapping of coarse-grain resources such as block memory or DSP cells. │ │ │ │ │ │ │ │ │ │ +4.4. Techmap by example │ │ │ │ │ + │ │ │ │ │ +195 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ 4.5 Notes on Verilog support in Yosys │ │ │ │ │ v Todo │ │ │ │ │ how much of this is specific to the read_verilog and should be in The Verilog and AST frontends? │ │ │ │ │ │ │ │ │ │ 4.5.1 Unsupported Verilog-2005 Features │ │ │ │ │ The following Verilog-2005 features are not supported by Yosys and there are currently no plans to add │ │ │ │ │ support for them: │ │ │ │ │ @@ -16933,21 +16908,14 @@ │ │ │ │ │ 4.5.2 Verilog Attributes and non-standard features │ │ │ │ │ • The full_case attribute on case statements is supported (also the non-standard // synopsys │ │ │ │ │ full_case directive) │ │ │ │ │ • The parallel_case attribute on case statements is supported (also the non-standard // synopsys │ │ │ │ │ parallel_case directive) │ │ │ │ │ • The // synopsys translate_off and // synopsys translate_on directives are also supported (but │ │ │ │ │ the use of ` `ifdef .. `endif ` is strongly recommended instead). │ │ │ │ │ - │ │ │ │ │ -4.5. Notes on Verilog support in Yosys │ │ │ │ │ - │ │ │ │ │ -195 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ • The nomem2reg attribute on modules or arrays prohibits the automatic early conversion of arrays to │ │ │ │ │ separate registers. This is potentially dangerous. Usually the front-end has good reasons for converting │ │ │ │ │ an array to a list of registers. Prohibiting this step will likely result in incorrect synthesis results. │ │ │ │ │ • The mem2reg attribute on modules or arrays forces the early conversion of arrays to separate registers. │ │ │ │ │ • The nomeminit attribute on modules or arrays prohibits the creation of initialized memories. This │ │ │ │ │ effectively puts mem2reg on all memories that are written to in an initial block and are not ROMs. │ │ │ │ │ • The nolatches attribute on modules or always-blocks prohibits the generation of logic-loops for latches. │ │ │ │ │ @@ -16962,14 +16930,21 @@ │ │ │ │ │ • The onehot attribute on wires mark them as one-hot state register. This is used for example for │ │ │ │ │ memory port sharing and set by the fsm_map pass. │ │ │ │ │ • The blackbox attribute on modules is used to mark empty stub modules that have the same ports │ │ │ │ │ as the real thing but do not contain information on the internal configuration. This modules are only │ │ │ │ │ used by the synthesis passes to identify input and output ports of cells. The Verilog backend also │ │ │ │ │ does not output blackbox modules on default. read_verilog , unless called with -noblackbox will │ │ │ │ │ automatically set the blackbox attribute on any empty module it reads. │ │ │ │ │ + │ │ │ │ │ +196 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ • The noblackbox attribute set on an empty module prevents read_verilog from automatically setting │ │ │ │ │ the blackbox attribute on the module. │ │ │ │ │ • The whitebox attribute on modules triggers the same behavior as blackbox, but is for whitebox │ │ │ │ │ modules, i.e. library modules that contain a behavioral model of the cell type. │ │ │ │ │ • The lib_whitebox attribute overwrites whitebox when read_verilog is run in -lib mode. Otherwise │ │ │ │ │ it’s automatically removed. │ │ │ │ │ • The dynports attribute is used by the Verilog front-end to mark modules that have ports with a width │ │ │ │ │ @@ -16984,21 +16959,14 @@ │ │ │ │ │ • The keep_hierarchy attribute on cells and modules keeps the flatten command from flattening the │ │ │ │ │ indicated cells and modules. │ │ │ │ │ • The gate_cost_equivalent attribute on a module can be used to specify the estimated cost of the │ │ │ │ │ module as a number of basic gate instances. See the help message of command keep_hierarchy which │ │ │ │ │ interprets this attribute. │ │ │ │ │ • The init attribute on wires is set by the frontend when a register is initialized “FPGA-style” with │ │ │ │ │ reg foo = val. It can be used during synthesis to add the necessary reset logic. │ │ │ │ │ - │ │ │ │ │ -196 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ • The top attribute on a module marks this module as the top of the design hierarchy. The hierarchy │ │ │ │ │ command sets this attribute when called with -top. Other commands, such as flatten and various │ │ │ │ │ backends use this attribute to determine the top module. │ │ │ │ │ • The src attribute is set on cells and wires created by to the string : │ │ │ │ │ by the HDL front-end and is then carried through the synthesis. When entities are combined, a new │ │ │ │ │ |-separated string is created that contains all the strings from the original entities. │ │ │ │ │ • The defaultvalue attribute is used to store default values for module inputs. The attribute is attached │ │ │ │ │ @@ -17014,14 +16982,21 @@ │ │ │ │ │ by the clkbufmap pass. │ │ │ │ │ • The clkbuf_inv attribute can be set on an output port of a module with the value set to the name │ │ │ │ │ of an input port of that module. When the clkbufmap would otherwise insert a clock buffer on this │ │ │ │ │ output, it will instead try inserting the clock buffer on the input port (this is used to implement clock │ │ │ │ │ inverter cells that clock buffer insertion will “see through”). │ │ │ │ │ • The clkbuf_inhibit is the default attribute to set on a wire to prevent automatic clock buffer insertion │ │ │ │ │ by clkbufmap . This behaviour can be overridden by providing a custom selection to clkbufmap . │ │ │ │ │ + │ │ │ │ │ +4.5. Notes on Verilog support in Yosys │ │ │ │ │ + │ │ │ │ │ +197 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ • The invertible_pin attribute can be set on a port to mark it as invertible via a cell parameter. The │ │ │ │ │ name of the inversion parameter is specified as the value of this attribute. The value of the inversion │ │ │ │ │ parameter must be of the same width as the port, with 1 indicating an inverted bit and 0 indicating a │ │ │ │ │ non-inverted bit. │ │ │ │ │ • The iopad_external_pin attribute on a blackbox module’s port marks it as the external-facing pin │ │ │ │ │ of an I/O pad, and prevents iopadmap from inserting another pad cell on it. │ │ │ │ │ • The module attribute abc9_lut is an integer attribute indicating to abc9 that this module describes │ │ │ │ │ @@ -17034,21 +17009,14 @@ │ │ │ │ │ • The module attribute abc9_flop is a boolean marking the module as a flip-flop. This allows abc9 to │ │ │ │ │ analyse its contents in order to perform sequential synthesis. │ │ │ │ │ • The frontend sets attributes always_comb, always_latch and always_ff on processes derived from │ │ │ │ │ SystemVerilog style always blocks according to the type of the always. These are checked for correctness │ │ │ │ │ in proc_dlatch. │ │ │ │ │ • The cell attribute wildcard_port_conns represents wildcard port connections (SystemVerilog .*). │ │ │ │ │ These are resolved to concrete connections to matching wires in hierarchy . │ │ │ │ │ - │ │ │ │ │ -4.5. Notes on Verilog support in Yosys │ │ │ │ │ - │ │ │ │ │ -197 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ • In addition to the (* ... *) attribute syntax, Yosys supports the non-standard {* ... *} attribute │ │ │ │ │ syntax to set default attributes for everything that comes after the {* ... *} statement. (Reset by │ │ │ │ │ adding an empty {* *} statement.) │ │ │ │ │ • In module parameter and port declarations, and cell port and parameter lists, a trailing comma is │ │ │ │ │ ignored. This simplifies writing Verilog code generators a bit in some cases. │ │ │ │ │ • Modules can be declared with module mod_name(...); (with three dots instead of a list of module │ │ │ │ │ ports). With this syntax it is sufficient to simply declare a module port as ‘input’ or ‘output’ in the │ │ │ │ │ @@ -17066,14 +17034,24 @@ │ │ │ │ │ or function is unused in this case and can be used to specify a behavioral model of the cell type for │ │ │ │ │ simulation. For example: │ │ │ │ │ module my_add3(A, B, C, Y); │ │ │ │ │ parameter WIDTH = 8; │ │ │ │ │ input [WIDTH-1:0] A, B, C; │ │ │ │ │ output [WIDTH-1:0] Y; │ │ │ │ │ ... │ │ │ │ │ +(continues on next page) │ │ │ │ │ + │ │ │ │ │ +198 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ +(continued from previous page) │ │ │ │ │ + │ │ │ │ │ endmodule │ │ │ │ │ module top; │ │ │ │ │ ... │ │ │ │ │ (* via_celltype = "my_add3 Y" *) │ │ │ │ │ (* via_celltype_defparam_WIDTH = 32 *) │ │ │ │ │ function [31:0] add3; │ │ │ │ │ input [31:0] A, B, C; │ │ │ │ │ @@ -17087,21 +17065,14 @@ │ │ │ │ │ type identifier. │ │ │ │ │ • Various enum_value_{value} attributes are added to wires of an enumerated type to give a map of │ │ │ │ │ possible enum items to their values. │ │ │ │ │ • The enum_base_type attribute is added to enum items to indicate which enum they belong to (enums │ │ │ │ │ – anonymous and otherwise – are automatically named with an auto-incrementing counter). Note that │ │ │ │ │ enums are currently not strongly typed. │ │ │ │ │ • A limited subset of DPI-C functions is supported. The plugin mechanism (see help plugin) can │ │ │ │ │ - │ │ │ │ │ -198 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ be used to load .so files with implementations of DPI-C routines. As a non-standard extension it is │ │ │ │ │ possible to specify a plugin alias using the : syntax. For example: │ │ │ │ │ module dpitest; │ │ │ │ │ import "DPI-C" function foo:round = real my_round (real); │ │ │ │ │ parameter real r = my_round(12.345); │ │ │ │ │ endmodule │ │ │ │ │ $ yosys -p 'plugin -a foo -i /lib/libm.so; read_verilog dpitest.v' │ │ │ │ │ @@ -17116,14 +17087,21 @@ │ │ │ │ │ to enable this functionality. (By default these blocks are ignored.) │ │ │ │ │ • The reprocess_after internal attribute is used by the Verilog frontend to mark cells with bindings │ │ │ │ │ which might depend on the specified instantiated module. Modules with such cells will be reprocessed │ │ │ │ │ during the hierarchy pass once the referenced module definition(s) become available. │ │ │ │ │ • The smtlib2_module attribute can be set on a blackbox module to specify a formal model directly │ │ │ │ │ using SMT-LIB 2. For such a module, the smtlib2_comb_expr attribute can be used on output ports │ │ │ │ │ to define their value using an SMT-LIB 2 expression. For example: │ │ │ │ │ + │ │ │ │ │ +4.5. Notes on Verilog support in Yosys │ │ │ │ │ + │ │ │ │ │ +199 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ (* blackbox *) │ │ │ │ │ (* smtlib2_module *) │ │ │ │ │ module submod(a, b); │ │ │ │ │ input [7:0] a; │ │ │ │ │ (* smtlib2_comb_expr = "(bvnot a)" *) │ │ │ │ │ output [7:0] b; │ │ │ │ │ endmodule │ │ │ │ │ @@ -17137,21 +17115,14 @@ │ │ │ │ │ • The system function $anyseq evaluates to any value, possibly a different value in each cycle. This is │ │ │ │ │ equivalent to declaring a reg as rand, but also works outside of checkers. (Yosys also supports rand │ │ │ │ │ variables outside checkers.) │ │ │ │ │ • The system functions $allconst and $allseq can be used to construct formal exist-forall problems. │ │ │ │ │ Assumptions only hold if the trace satisfies the assumption for all $allconst/$allseq values. For │ │ │ │ │ assertions and cover statements it is sufficient if just one $allconst/$allseq value triggers the property │ │ │ │ │ (similar to $anyconst/$anyseq). │ │ │ │ │ - │ │ │ │ │ -4.5. Notes on Verilog support in Yosys │ │ │ │ │ - │ │ │ │ │ -199 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ • Wires/registers declared using the anyconst/anyseq/allconst/allseq attribute (for example (* │ │ │ │ │ anyconst *) reg [7:0] foobar;) will behave as if driven by a $anyconst/$anyseq/$allconst/ │ │ │ │ │ $allseq function. │ │ │ │ │ • The SystemVerilog tasks $past, $stable, $rose and $fell are supported in any clocked block. │ │ │ │ │ • The syntax @($global_clock) can be used to create FFs that have no explicit clock input ($ff │ │ │ │ │ cells). The same can be achieved by using @(posedge ) or @(negedge ) when │ │ │ │ │ is marked with the (* gclk *) Verilog attribute. │ │ │ │ │ @@ -17167,14 +17138,21 @@ │ │ │ │ │ • Declaring free variables with rand and rand const is supported. │ │ │ │ │ • Checkers without a port list that do not need to be instantiated (but instead behave like a named │ │ │ │ │ block) are supported. │ │ │ │ │ • SystemVerilog packages are supported. Once a SystemVerilog file is read into a design with │ │ │ │ │ read_verilog , all its packages are available to SystemVerilog files being read into the same design │ │ │ │ │ afterwards. │ │ │ │ │ • typedefs are supported (including inside packages) │ │ │ │ │ + │ │ │ │ │ +200 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ – type casts are currently not supported │ │ │ │ │ • enums are supported (including inside packages) │ │ │ │ │ – but are currently not strongly typed │ │ │ │ │ • packed structs and unions are supported │ │ │ │ │ – arrays of packed structs/unions are currently not supported │ │ │ │ │ – structure literals are currently not supported │ │ │ │ │ • multidimensional arrays are supported │ │ │ │ │ @@ -17185,20 +17163,14 @@ │ │ │ │ │ • Assignments within expressions are supported. │ │ │ │ │ │ │ │ │ │ 4.6 Hashing and associative data structures in Yosys │ │ │ │ │ 4.6.1 Container classes based on hashing │ │ │ │ │ Yosys uses dict and pool as main container classes. dict is essentially a replacement │ │ │ │ │ for std::unordered_map and pool is a replacement for std::unordered_set. The main │ │ │ │ │ characteristics are: │ │ │ │ │ -200 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ • dict and pool are about 2x faster than the std containers │ │ │ │ │ (though this claim hasn’t been verified for over 10 years) │ │ │ │ │ • references to elements in a dict or pool are invalidated by │ │ │ │ │ insert and remove operations (similar to std::vector on push_back()). │ │ │ │ │ • some iterators are invalidated by erase(). specifically, iterators │ │ │ │ │ that have not passed the erased element yet are invalidated. (erase() itself returns valid iterator │ │ │ │ │ to the next element.) │ │ │ │ │ @@ -17213,22 +17185,33 @@ │ │ │ │ │ • dict and pool will have the same order of iteration across │ │ │ │ │ all compilers, standard libraries and architectures. │ │ │ │ │ In addition to dict and pool there is also an idict that creates a bijective map from K to │ │ │ │ │ the integers. For example: │ │ │ │ │ idict si; │ │ │ │ │ log("%d\n", si("hello")); │ │ │ │ │ log("%d\n", si("world")); │ │ │ │ │ + │ │ │ │ │ +// will print 42 │ │ │ │ │ +// will print 43 │ │ │ │ │ +(continues on next page) │ │ │ │ │ + │ │ │ │ │ +4.6. Hashing and associative data structures in Yosys │ │ │ │ │ + │ │ │ │ │ +201 │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ +(continued from previous page) │ │ │ │ │ + │ │ │ │ │ log("%d\n", si.at("world")); │ │ │ │ │ log("%d\n", si.at("dummy")); │ │ │ │ │ log("%s\n", si[42].c_str())); │ │ │ │ │ log("%s\n", si[43].c_str())); │ │ │ │ │ log("%s\n", si[44].c_str())); │ │ │ │ │ │ │ │ │ │ -// will print 42 │ │ │ │ │ -// will print 43 │ │ │ │ │ // will print 43 │ │ │ │ │ // will throw exception │ │ │ │ │ // will print hello │ │ │ │ │ // will print world │ │ │ │ │ // will throw exception │ │ │ │ │ │ │ │ │ │ It is not possible to remove elements from an idict. │ │ │ │ │ @@ -17245,20 +17228,14 @@ │ │ │ │ │ patterns within Yosys. In general, a good hash function typically folds values into a state accumulator with │ │ │ │ │ a mathematical function that is fast to compute and has some beneficial properties. One of these is the │ │ │ │ │ avalanche property, which demands that a small change such as flipping a bit or incrementing by one in the │ │ │ │ │ input produces a large, unpredictable change in the output. Additionally, the bit independence criterion │ │ │ │ │ states that any pair of output bits should change independently when any single input bit is inverted. These │ │ │ │ │ properties are important for avoiding hash collision on data patterns like the hash of a sequence not colliding │ │ │ │ │ with its permutation, not losing from the state the information added by hashing preceding elements, etc. │ │ │ │ │ -4.6. Hashing and associative data structures in Yosys │ │ │ │ │ - │ │ │ │ │ -201 │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ DJB2 lacks these properties. Instead, since Yosys hashes large numbers of data structures composed of │ │ │ │ │ incrementing integer IDs, Yosys abuses the predictability of DJB2 to get lower hash collisions, with regular │ │ │ │ │ nature of the hashes surviving through the interaction with the “modulo prime” operations in the associative │ │ │ │ │ data structures. For example, some most common objects in Yosys are interned IdStrings of incrementing │ │ │ │ │ indices or SigBits with bit offsets into wire (represented by its unique IdString name) as the typical case. │ │ │ │ │ This is what makes DJB2 a local optimum. Additionally, the ADD version of DJB2 (like above but with │ │ │ │ │ addition instead of XOR) is used to this end for some types, abandoning the general pattern of folding values │ │ │ │ │ @@ -17274,14 +17251,21 @@ │ │ │ │ │ By default it pulls the Hasher h through a Hasher │ │ │ │ │ T::hash_into(Hasher h) method. That’s the method you have to implement to make a record (class │ │ │ │ │ or struct) type easily hashable with Yosys hashlib associative data structures. │ │ │ │ │ hash_ops is specialized for built-in types like int or bool and treats pointers the same as integers, so it │ │ │ │ │ doesn’t dereference pointers. Since many RTLIL data structures like RTLIL::Wire carry their own unique │ │ │ │ │ index Hasher::hash_t hashidx_;, there are specializations for hash_ops and others in kernel/ │ │ │ │ │ hashlib.h that actually dereference the pointers and call hash_into on the instances pointed to. │ │ │ │ │ + │ │ │ │ │ +202 │ │ │ │ │ + │ │ │ │ │ +Chapter 4. Yosys internals │ │ │ │ │ + │ │ │ │ │ + YosysHQ Yosys, Version 0.52 │ │ │ │ │ + │ │ │ │ │ hash_ops is also specialized for simple compound types like std::pair by calling hash_into in │ │ │ │ │ sequence on its members. For flexible size containers like std::vector the size of the container is hashed │ │ │ │ │ first. That is also how implementing hashing for a custom record data type should be - unless there is strong │ │ │ │ │ reason to do otherwise, call h.eat(m) on the Hasher h you have received for each member in sequence and │ │ │ │ │ return h;. │ │ │ │ │ The hash_ops::hash(obj) method is not indended to be called when context of implementing │ │ │ │ │ the hashing for a record or other compound type. │ │ │ │ │ @@ -17300,24 +17284,14 @@ │ │ │ │ │ unsigned int T::hash() const { │ │ │ │ │ return mkhash(a, b); │ │ │ │ │ } │ │ │ │ │ # elif YS_HASHING_VERSION == 1 │ │ │ │ │ Hasher T::hash_into(Hasher h) const { │ │ │ │ │ h.eat(a); │ │ │ │ │ h.eat(b); │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ -202 │ │ │ │ │ - │ │ │ │ │ -Chapter 4. Yosys internals │ │ │ │ │ - │ │ │ │ │ - YosysHQ Yosys, Version 0.52 │ │ │ │ │ - │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ return h; │ │ │ │ │ } │ │ │ │ │ Hasher T::hash() const { │ │ │ │ │ Hasher h; │ │ │ │ │ h.eat(*this); │ │ │ │ │ return h; │ │ │ │ │ } │ │ │ │ │ @@ -18415,15 +18389,20 @@ │ │ │ │ │ Replacement args: │ │ │ │ │ --cxx │ │ │ │ │ g++ │ │ │ │ │ --cxxflags │ │ │ │ │ -g -O2 -flto=auto -ffat-lto-objects \ │ │ │ │ │ -fstack-protector-strong -Wformat -Werror=format-security \ │ │ │ │ │ -Wall -Wextra -ggdb -I/usr/share/yosys/include -MD -MP \ │ │ │ │ │ --D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER= │ │ │ │ │ +-D_YOSYS_ -fPIC -I/usr/include -DYOSYS_VER=@CXXFLAGS@.52 \ │ │ │ │ │ +-DYOSYS_MAJOR=0 -DYOSYS_MINOR=52 -DYOSYS_COMMIT=0.52 \ │ │ │ │ │ +-std=c++17 -O3 -DYOSYS_ENABLE_READLINE \ │ │ │ │ │ +-DYOSYS_ENABLE_PLUGINS -DYOSYS_ENABLE_GLOB \ │ │ │ │ │ +-DYOSYS_ENABLE_ZLIB -I/usr/include/tcl8.6 \ │ │ │ │ │ +-DYOSYS_ENABLE_TCL -DYOSYS_ENABLE_ABC -DYOSYS_ENABLE_COVER │ │ │ │ │ --linkflags │ │ │ │ │ -rdynamic │ │ │ │ │ --ldflags │ │ │ │ │ (alias of --linkflags) │ │ │ │ │ --libs │ │ │ │ │ -lstdc++ -lm -lrt -lreadline -lffi -ldl -lz -ltcl8.6 -ltclstub8.6 │ │ │ │ │ --ldlibs │ │ │ │ │ @@ -18435,25 +18414,25 @@ │ │ │ │ │ All other args are passed through as they are. │ │ │ │ │ Use --exec to call a command instead of generating output. Example usage: │ │ │ │ │ ./yosys-config --exec --cxx --cxxflags --ldflags -o plugin.so -shared plugin.cc --libs │ │ │ │ │ The above command can be abbreviated as: │ │ │ │ │ ./yosys-config --build plugin.so plugin.cc │ │ │ │ │ Use --prefix to change the prefix for the special args from '--' to │ │ │ │ │ something else. Example: │ │ │ │ │ -./yosys-config --prefix @ bindir: @bindir │ │ │ │ │ -The args --bindir and --datdir can be directly followed by a slash and │ │ │ │ │ -additional text. Example: │ │ │ │ │ (continues on next page) │ │ │ │ │ │ │ │ │ │ 225 │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ (continued from previous page) │ │ │ │ │ │ │ │ │ │ +./yosys-config --prefix @ bindir: @bindir │ │ │ │ │ +The args --bindir and --datdir can be directly followed by a slash and │ │ │ │ │ +additional text. Example: │ │ │ │ │ ./yosys-config --datdir/simlib.v │ │ │ │ │ │ │ │ │ │ 8.2 yosys-filterlib │ │ │ │ │ v Todo │ │ │ │ │ how does a filterlib rules-file work? │ │ │ │ │ The yosys-filterlib tool is a small utility that can be used to strip or extract information from a Liberty │ │ │ │ │ file. This can be useful for removing sensitive or proprietary information such as timing or other trade │ │ │ │ │ @@ -18489,29 +18468,25 @@ │ │ │ │ │ -T type │ │ │ │ │ specify output type (blif_mv (default), blif_mvs, blif, or none) │ │ │ │ │ -x │ │ │ │ │ equivalent to '-t none -T none' │ │ │ │ │ -b │ │ │ │ │ running in bridge mode │ │ │ │ │ │ │ │ │ │ -8.4 yosys-smtbmc │ │ │ │ │ -The yosys-smtbmc tool is a utility used by SBY for interacting with smt solvers. │ │ │ │ │ -yosys-smtbmc [options] │ │ │ │ │ --h, --help │ │ │ │ │ -show this message │ │ │ │ │ -(continues on next page) │ │ │ │ │ - │ │ │ │ │ 226 │ │ │ │ │ │ │ │ │ │ Chapter 8. Auxiliary programs │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ -(continued from previous page) │ │ │ │ │ - │ │ │ │ │ +8.4 yosys-smtbmc │ │ │ │ │ +The yosys-smtbmc tool is a utility used by SBY for interacting with smt solvers. │ │ │ │ │ +yosys-smtbmc [options] │ │ │ │ │ +-h, --help │ │ │ │ │ +show this message │ │ │ │ │ -t │ │ │ │ │ -t : │ │ │ │ │ -t :: │ │ │ │ │ default: skip_steps=0, step_size=1, num_steps=20 │ │ │ │ │ -g │ │ │ │ │ │ │ │ │ │ -i │ │ │ │ │ @@ -18539,30 +18514,30 @@ │ │ │ │ │ the AIGER witness file does not include the status and │ │ │ │ │ properties lines. │ │ │ │ │ --yw │ │ │ │ │ read a Yosys witness. │ │ │ │ │ --btorwit │ │ │ │ │ read a BTOR witness. │ │ │ │ │ --noinfo │ │ │ │ │ -only run the core proof, do not collect and print any │ │ │ │ │ -additional information (e.g. which assert failed) │ │ │ │ │ ---presat │ │ │ │ │ -check if the design with assumptions but without assertions │ │ │ │ │ -is SAT before checking if assertions are UNSAT. This will │ │ │ │ │ -detect if there are contradicting assumptions. In some cases │ │ │ │ │ (continues on next page) │ │ │ │ │ │ │ │ │ │ 8.4. yosys-smtbmc │ │ │ │ │ │ │ │ │ │ 227 │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ (continued from previous page) │ │ │ │ │ │ │ │ │ │ +only run the core proof, do not collect and print any │ │ │ │ │ +additional information (e.g. which assert failed) │ │ │ │ │ +--presat │ │ │ │ │ +check if the design with assumptions but without assertions │ │ │ │ │ +is SAT before checking if assertions are UNSAT. This will │ │ │ │ │ +detect if there are contradicting assumptions. In some cases │ │ │ │ │ this will also help to "warm up" the solver, potentially │ │ │ │ │ yielding a speedup. │ │ │ │ │ --final-only │ │ │ │ │ only check final constraints, assume base case │ │ │ │ │ --assume-skipped │ │ │ │ │ assume asserts in skipped steps in BMC. │ │ │ │ │ no assumptions are created for skipped steps │ │ │ │ │ @@ -18588,30 +18563,30 @@ │ │ │ │ │ file and only dump object below in design hierarchy. │ │ │ │ │ --noinit │ │ │ │ │ do not assume initial conditions in state 0 │ │ │ │ │ --dump-all │ │ │ │ │ when using -g or -i, create a dump file for each │ │ │ │ │ step. The character '%' is replaced in all dump │ │ │ │ │ filenames with the step number. │ │ │ │ │ ---append │ │ │ │ │ -add time steps at the end of the trace │ │ │ │ │ -when creating a counter example (this additional time │ │ │ │ │ -steps will still be constrained by assumptions) │ │ │ │ │ ---binary │ │ │ │ │ -dump anyconst values as raw bit strings │ │ │ │ │ (continues on next page) │ │ │ │ │ │ │ │ │ │ 228 │ │ │ │ │ │ │ │ │ │ Chapter 8. Auxiliary programs │ │ │ │ │ │ │ │ │ │ YosysHQ Yosys, Version 0.52 │ │ │ │ │ │ │ │ │ │ (continued from previous page) │ │ │ │ │ │ │ │ │ │ +--append │ │ │ │ │ +add time steps at the end of the trace │ │ │ │ │ +when creating a counter example (this additional time │ │ │ │ │ +steps will still be constrained by assumptions) │ │ │ │ │ +--binary │ │ │ │ │ +dump anyconst values as raw bit strings │ │ │ │ │ --keep-going │ │ │ │ │ continue BMC after the first failed assertion and report │ │ │ │ │ further failed assertions. To output multiple traces │ │ │ │ │ covering all found failed assertions, the character '%' is │ │ │ │ │ replaced in all dump filenames with an increasing number. │ │ │ │ │ In cover mode, don't stop when a cover trace contains a failed │ │ │ │ │ assertion. │ │ │ │ │ @@ -18638,29 +18613,30 @@ │ │ │ │ │ --timeout │ │ │ │ │ set the solver timeout to the specified value (in seconds). │ │ │ │ │ --logic │ │ │ │ │ use the specified SMT2 logic (e.g. QF_AUFBV) │ │ │ │ │ --dummy │ │ │ │ │ if solver is "dummy", read solver output from that file │ │ │ │ │ otherwise: write solver output to that file │ │ │ │ │ ---smt2-option