verilog/rtl/unit_test/cover/model/design_smt2.log

 /----------------------------------------------------------------------------\
 |                                                                            |
 |  yosys -- Yosys Open SYnthesis Suite                                       |
 |                                                                            |
 |  Copyright (C) 2012 - 2020  Claire Xenia Wolf <claire@yosyshq.com>         |
 |                                                                            |
 |  Permission to use, copy, modify, and/or distribute this software for any  |
 |  purpose with or without fee is hereby granted, provided that the above    |
 |  copyright notice and this permission notice appear in all copies.         |
 |                                                                            |
 |  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES  |
 |  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF          |
 |  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR   |
 |  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES    |
 |  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN     |
 |  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF   |
 |  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.            |
 |                                                                            |
 \----------------------------------------------------------------------------/

 Yosys 0.15+11 (git sha1 cbece4af0, clang 10.0.0-4ubuntu1 -fPIC -Os)


-- Executing script file `design_smt2.ys' --

1. Executing RTLIL frontend.
Input filename: design.il

2. Executing MEMORY_NORDFF pass (extracting $dff cells from memories).

3. Executing ASYNC2SYNC pass.

4. Executing OPT_CLEAN pass (remove unused cells and wires).
Finding unused cells or wires in module \hyperram..

5. Executing SETUNDEF pass (replace undef values with defined constants).

6. Executing OPT pass (performing simple optimizations).

6.1. Executing OPT_EXPR pass (perform const folding).
Optimizing module hyperram.

6.2. Executing OPT_MERGE pass (detect identical cells).
Finding identical cells in module `\hyperram'.
Removed a total of 0 cells.

6.3. Executing OPT_DFF pass (perform DFF optimizations).
Adding SRST signal on $procdff$416 ($dff) from module hyperram (D = \ck_bar, Q = \ck, rval = 1'0).
Adding EN signal on $procdff$414 ($dff) from module hyperram (D = \next_control_state, Q = \control_state).
Adding EN signal on $procdff$413 ($dff) from module hyperram (D = $2\next_done_counter[7:0], Q = \done_counter).
Adding SRST signal on $auto$ff.cc:262:slice$451 ($dffe) from module hyperram (D = $add$hyperram.v:225$40_Y, Q = \done_counter, rval = 8'00000000).
Adding EN signal on $procdff$412 ($dff) from module hyperram (D = $2\next_wait_counter[7:0], Q = \wait_counter).
Adding SRST signal on $auto$ff.cc:262:slice$453 ($dffe) from module hyperram (D = $add$hyperram.v:152$30_Y, Q = \wait_counter, rval = 8'00000000).
Adding EN signal on $procdff$408 ($dff) from module hyperram (D = $add$hyperram.v:273$49_Y, Q = \write_count).
Adding EN signal on $procdff$407 ($dff) from module hyperram (D = $add$hyperram.v:270$47_Y, Q = \read_count).

6.4. Executing OPT_CLEAN pass (remove unused cells and wires).
Finding unused cells or wires in module \hyperram..
Removed 7 unused cells and 7 unused wires.
<suppressed ~10 debug messages>

6.5. Rerunning OPT passes. (Removed registers in this run.)

6.6. Executing OPT_EXPR pass (perform const folding).
Optimizing module hyperram.
<suppressed ~1 debug messages>

6.7. Executing OPT_MERGE pass (detect identical cells).
Finding identical cells in module `\hyperram'.
Removed a total of 0 cells.

6.8. Executing OPT_DFF pass (perform DFF optimizations).

6.9. Executing OPT_CLEAN pass (remove unused cells and wires).
Finding unused cells or wires in module \hyperram..

6.10. Finished fast OPT passes.

7. Executing CHECK pass (checking for obvious problems).
Checking module hyperram...
Found and reported 0 problems.

8. Executing HIERARCHY pass (managing design hierarchy).

8.1. Analyzing design hierarchy..
Top module:  \hyperram

8.2. Analyzing design hierarchy..
Top module:  \hyperram
Removed 0 unused modules.
Module hyperram directly or indirectly contains formal properties -> setting "keep" attribute.

9. Executing DFFUNMAP pass (unmap clock enable and synchronous reset from FFs).

10. Printing statistics.

=== hyperram ===

   Number of wires:                100
   Number of wire bits:            563
   Number of public wires:          34
   Number of public wire bits:     383
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                 94
     $add                            5
     $anyseq                         4
     $cover                          9
     $dff                           19
     $eq                            22
     $logic_and                      1
     $logic_not                      3
     $logic_or                       1
     $mux                           18
     $ne                             4
     $pmux                           3
     $reduce_and                     1
     $reduce_bool                    1
     $reduce_or                      3

11. Executing SMT2 backend.

11.1. Executing BMUXMAP pass.

11.2. Executing DEMUXMAP pass.
Creating SMT-LIBv2 representation of module hyperram.

End of script. Logfile hash: e86ecf84c9, CPU: user 0.03s system 0.01s, MEM: 11.30 MB peak
Yosys 0.15+11 (git sha1 cbece4af0, clang 10.0.0-4ubuntu1 -fPIC -Os)
Time spent: 27% 3x opt_clean (0 sec), 14% 2x opt_expr (0 sec), ...