diff options
| -rw-r--r-- | CHANGELOG | 21 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | README.md | 12 | ||||
| -rw-r--r-- | frontends/verific/verific.cc | 1 | ||||
| -rw-r--r-- | manual/command-reference-manual.tex | 76 | ||||
| -rw-r--r-- | techlibs/gatemate/gatemate_foldinv.cc | 41 |
6 files changed, 86 insertions, 69 deletions
@@ -2,9 +2,28 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.18 .. Yosys 0.18-dev +Yosys 0.19 .. Yosys 0.19-dev -------------------------- +Yosys 0.18 .. Yosys 0.19 +-------------------------- + * New commands and options + - Added option "-rom-only" to "memory_libmap" pass + - Added option "-smtcheck" to "hierarchy" pass + - Added option "-keepdc" to "memory_libmap" pass + - Added option "-suffix" to "rename" pass + - Added "gatemate_foldinv" pass + + * Formal Verification + - Added support for $pos cell in btor backend + - Added the "smtlib2_module" and "smtlib2_comb_expr" attributes + + * GateMate support + - Added LUT tree mapping + + * Verific support + - Added option "-pp" to "verific -import" + Yosys 0.17 .. Yosys 0.18 -------------------------- * Various @@ -129,7 +129,7 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.18+48 +YOSYS_VER := 0.19+2 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -145,7 +145,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 19ce3b4.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline a45c131.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # @@ -505,6 +505,18 @@ Verilog Attributes and non-standard features 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: + + (* blackbox *) + (* smtlib2_module *) + module submod(a, b); + input [7:0] a; + (* smtlib2_comb_expr = "(bvnot a)" *) + output [7:0] b; + endmodule Non-standard or SystemVerilog features for formal verification ============================================================== diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 8ecf54472..fd6208e86 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2496,6 +2496,7 @@ struct VerificPass : public Pass { log("\n"); log(" -v, -vv\n"); log(" Verbose log messages. (-vv is even more verbose than -v.)\n"); + log("\n"); log(" -pp <filename>\n"); log(" Pretty print design after elaboration to specified file.\n"); log("\n"); diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 3a9259867..28b99f3a6 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -2256,6 +2256,16 @@ and simulus signal from FST file number of clock cycles to simulate (default: 20) \end{lstlisting} +\section{gatemate\_foldinv -- fold inverters into Gatemate LUT trees} +\label{cmd:gatemate_foldinv} +\begin{lstlisting}[numbers=left,frame=single] + gatemate_foldinv [selection] + + +This pass searches for $__CC_NOT cells and folds them into CC_LUT2, CC_L2T4 +and CC_L2T5 cells as created by LUT tree mapping. +\end{lstlisting} + \section{glift -- create GLIFT models and optimization problems} \label{cmd:glift} \begin{lstlisting}[numbers=left,frame=single] @@ -2950,6 +2960,12 @@ pass to word-wide DFFs and address decoders. -iattr for -attr, ignore case of <value>. + + -rom-only + only perform conversion for ROMs (memories with no write ports). + + -keepdc + when mapping ROMs, keep x-bits shared across read ports. \end{lstlisting} \section{memory\_memx -- emulate vlog sim behavior for mem ports} @@ -4226,10 +4242,12 @@ Assign names auto-generated from the src attribute to all selected wires and cells with private names. - rename -wire [selection] + rename -wire [selection] [-suffix <suffix>] Assign auto-generated names based on the wires they drive to all selected cells with private names. Ignores cells driving privatly named wires. +By default, the cell is named after the wire with the cell type as suffix. +The -suffix option can be used to set the suffix to the given string instead. rename -enumerate [-pattern <pattern>] [selection] @@ -5988,6 +6006,9 @@ This command runs synthesis for Cologne Chip AG GateMate FPGAs. -nomx8, -nomx4 do not use CC_MX{8,4} multiplexer cells in output netlist. + -luttree + use new LUT tree mapping approach (EXPERIMENTAL). + -dff run 'abc' with -dff option @@ -6067,7 +6088,11 @@ The following commands are executed by this synthesis command: techmap -map +/gatemate/mux_map.v map_luts: - abc -dress -lut 4 + abc -genlib +/gatemate/lut_tree_cells.genlib (with -luttree) + techmap -map +/gatemate/lut_tree_map.v (with -luttree) + gatemate_foldinv (with -luttree) + techmap -map +/gatemate/inv_map.v (with -luttree) + abc -dress -lut 4 (without -luttree) clean map_cells: @@ -7901,6 +7926,9 @@ Import options: -v, -vv Verbose log messages. (-vv is even more verbose than -v.) + -pp <filename> + Pretty print design after elaboration to specified file. + The following additional import options are useful for debugging the Verific bindings (for Yosys and/or Verific developers): @@ -7941,50 +7969,6 @@ Pretty print options: Save output for VHDL design units. - verific -app <application>.. - -Execute YosysHQ formal application on loaded Verilog files. - -Application options: - - -module <module> - Run formal application only on specified module. - - -blacklist <filename[:lineno]> - Do not run application on modules from files that match the filename - or filename and line number if provided in such format. - Parameter can also contain comma separated list of file locations. - - -blfile <file> - Do not run application on locations specified in file, they can - represent filename or filename and location in file. - -Applications: - - WARNING: Applications only available in commercial build. - - - verific -template <name> <top_module>.. - -Generate template for specified top module of loaded design. - -Template options: - - -out - Specifies output file for generated template, by default output is stdout - - -chparam name value - Generate template using this parameter value. Otherwise default parameter - values will be used for templat generate functionality. This option - can be specified multiple times to override multiple parameters. - String values must be passed in double quotes ("). - -Templates: - - WARNING: Templates only available in commercial build. - - - verific -cfg [<name> [<value>]] Get/set Verific runtime flags. diff --git a/techlibs/gatemate/gatemate_foldinv.cc b/techlibs/gatemate/gatemate_foldinv.cc index 20fbbf8a3..752f8aac0 100644 --- a/techlibs/gatemate/gatemate_foldinv.cc +++ b/techlibs/gatemate/gatemate_foldinv.cc @@ -34,26 +34,6 @@ struct LUTType { IdString output_param; }; -static const dict<IdString, LUTType> lut_types = { - {ID(CC_LUT2), {{ - {ID(I0), {0, ID(INIT)}}, - {ID(I1), {1, ID(INIT)}}, - }, ID(INIT)}}, - {ID(CC_L2T4), {{ - {ID(I0), {0, ID(INIT_L00)}}, - {ID(I1), {1, ID(INIT_L00)}}, - {ID(I2), {0, ID(INIT_L01)}}, - {ID(I3), {1, ID(INIT_L01)}}, - }, ID(INIT_L10)}}, - {ID(CC_L2T5), {{ - {ID(I0), {0, ID(INIT_L02)}}, - {ID(I1), {1, ID(INIT_L02)}}, - {ID(I2), {0, ID(INIT_L03)}}, - {ID(I3), {1, ID(INIT_L03)}}, - {ID(I4), {0, ID(INIT_L20)}}, - }, ID(INIT_L20)}}, -}; - struct FoldInvWorker { FoldInvWorker(Module *module) : module(module), sigmap(module) {}; Module *module; @@ -64,6 +44,27 @@ struct FoldInvWorker { // Mapping from inverter input to inverter dict<SigBit, Cell*> inverter_input; + const dict<IdString, LUTType> lut_types = { + {ID(CC_LUT2), {{ + {ID(I0), {0, ID(INIT)}}, + {ID(I1), {1, ID(INIT)}}, + }, ID(INIT)}}, + {ID(CC_L2T4), {{ + {ID(I0), {0, ID(INIT_L00)}}, + {ID(I1), {1, ID(INIT_L00)}}, + {ID(I2), {0, ID(INIT_L01)}}, + {ID(I3), {1, ID(INIT_L01)}}, + }, ID(INIT_L10)}}, + {ID(CC_L2T5), {{ + {ID(I0), {0, ID(INIT_L02)}}, + {ID(I1), {1, ID(INIT_L02)}}, + {ID(I2), {0, ID(INIT_L03)}}, + {ID(I3), {1, ID(INIT_L03)}}, + {ID(I4), {0, ID(INIT_L20)}}, + }, ID(INIT_L20)}}, + }; + + void find_inverted_bits() { for (auto cell : module->selected_cells()) { |