docs/getting_started_make_guide.md


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148

# More Detailed `make` Instructions

The full syntax of the `make` command is `<keyboard_folder>:<keymap>:<target>`, where:

* `<keyboard_folder>` is the path of the keyboard, for example `planck`
  * Use `all` to compile all keyboards
  * Specify the path to compile a revision, for example `planck/rev4` or `planck/rev3`
  * If the keyboard doesn't have any folders, it can be left out
  * To compile the default folder, you can leave it out
* `<keymap>` is the name of the keymap, for example `algernon`
  * Use `all` to compile all keymaps
* `<target>` will be explained in more detail below.

The `<target>` means the following
* If no target is given, then it's the same as `all` below
* `all` compiles as many keyboard/revision/keymap combinations as specified. For example, `make planck/rev4:default` will generate a single .hex, while `make planck/rev4:all` will generate a hex for every keymap available to the planck.
* `flash`, `dfu`, `teensy`, `avrdude`, `dfu-util`, or `bootloadHID` compile and upload the firmware to the keyboard. If the compilation fails, then nothing will be uploaded. The programmer to use depends on the keyboard. For most keyboards it's `dfu`, but for ChibiOS keyboards you should use `dfu-util`, and `teensy` for standard Teensys. To find out which command you should use for your keyboard, check the keyboard specific readme.
 * **Note**: some operating systems need root access for these commands to work, so in that case you need to run for example `sudo make planck/rev4:default:flash`.
* `clean`, cleans the build output folders to make sure that everything is built from scratch. Run this before normal compilation if you have some unexplainable problems.

You can also add extra options at the end of the make command line, after the target

* `make COLOR=false` - turns off color output
* `make SILENT=true` - turns off output besides errors/warnings
* `make VERBOSE=true` - outputs all of the gcc stuff (not interesting, unless you need to debug)
* `make EXTRAFLAGS=-E` - Preprocess the code without doing any compiling (useful if you are trying to debug #define commands)

The make command itself also has some additional options, type `make --help` for more information. The most useful is probably `-jx`, which specifies that you want to compile using more than one CPU, the `x` represents the number of CPUs that you want to use. Setting that can greatly reduce the compile times, especially if you are compiling many keyboards/keymaps. I usually set it to one less than the number of CPUs that I have, so that I have some left for doing other things while it's compiling. Note that not all operating systems and make versions supports that option.

Here are some examples commands

* `make all:all` builds everything (all keyboard folders, all keymaps). Running just `make` from the `root` will also run this.
* `make ergodox_infinity:algernon:clean` will clean the build output of the Ergodox Infinity keyboard.
* `make planck/rev4:default:flash COLOR=false` builds and uploads the keymap without color output.

## `rules.mk` Options

Set these variables to `no` to disable them, and `yes` to enable them.

`BOOTMAGIC_ENABLE`

This allows you to hold a key and the salt key (space by default) and have access to a various EEPROM settings that persist over power loss. It's advised you keep this disabled, as the settings are often changed by accident, and produce confusing results that makes it difficult to debug. It's one of the more common problems encountered in help sessions.

`MOUSEKEY_ENABLE`

This gives you control over cursor movements and clicks via keycodes/custom functions.

`EXTRAKEY_ENABLE`

This allows you to use the system and audio control key codes.

`CONSOLE_ENABLE`

This allows you to print messages that can be read using [`hid_listen`](https://www.pjrc.com/teensy/hid_listen.html).

By default, all debug (*dprint*) print (*print*, *xprintf*), and user print (*uprint*) messages will be enabled. This will eat up a significant portion of the flash and may make the keyboard .hex file too big to program.

To disable debug messages (*dprint*) and reduce the .hex file size, include `#define NO_DEBUG` in your `config.h` file.

To disable print messages (*print*, *xprintf*) and user print messages (*uprint*) and reduce the .hex file size, include `#define NO_PRINT` in your `config.h` file.

To disable print messages (*print*, *xprintf*) and **KEEP** user print messages (*uprint*), include `#define USER_PRINT` in your `config.h` file (do not also include `#define NO_PRINT` in this case).

To see the text, open `hid_listen` and enjoy looking at your printed messages.

**NOTE:** Do not include *uprint* messages in anything other than your keymap code. It must not be used within the QMK system framework. Otherwise, you will bloat other people's .hex files.

`COMMAND_ENABLE`

This enables magic commands, typically fired with the default magic key combo `LSHIFT+RSHIFT+KEY`. Magic commands include turning on debugging messages (`MAGIC+D`) or temporarily toggling NKRO (`MAGIC+N`).

`SLEEP_LED_ENABLE`

Enables your LED to breath while your computer is sleeping. Timer1 is being used here. This feature is largely unused and untested, and needs updating/abstracting.

`NKRO_ENABLE`

This allows the keyboard to tell the host OS that up to 248 keys are held down at once (default without NKRO is 6). NKRO is off by default, even if `NKRO_ENABLE` is set. NKRO can be forced by adding `#define FORCE_NKRO` to your config.h or by binding `MAGIC_TOGGLE_NKRO` to a key and then hitting the key.

`BACKLIGHT_ENABLE`

This enables the in-switch LED backlighting. You can specify the backlight pin by putting this in your `config.h`:

    #define BACKLIGHT_PIN B7

`MIDI_ENABLE`

This enables MIDI sending and receiving with your keyboard. To enter MIDI send mode, you can use the keycode `MI_ON`, and `MI_OFF` to turn it off. This is a largely untested feature, but more information can be found in the `quantum/quantum.c` file.

`UNICODE_ENABLE`

This allows you to send Unicode characters using `UC(<code point>)` in your keymap. Code points up to `0x7FFF` are supported. This covers characters for most modern languages, as well as symbols, but it doesn't cover emoji.

`UNICODEMAP_ENABLE`

This allows you to send Unicode characters using `X(<map index>)` in your keymap. You will need to maintain a mapping table in your keymap file. All possible code points (up to `0x10FFFF`) are supported.

`UCIS_ENABLE`

This allows you to send Unicode characters by inputting a mnemonic corresponding to the character you want to send. You will need to maintain a mapping table in your keymap file. All possible code points (up to `0x10FFFF`) are supported.

For further details, as well as limitations, see the [Unicode page](feature_unicode.md).

`BLUETOOTH_ENABLE`

This allows you to interface with a Bluefruit EZ-key to send keycodes wirelessly. It uses the D2 and D3 pins.

`AUDIO_ENABLE`

This allows you output audio on the C6 pin (needs abstracting). See the [audio page](feature_audio.md) for more information.

`FAUXCLICKY_ENABLE`

Uses buzzer to emulate clicky switches. A cheap imitation of the Cherry blue switches. By default, uses the C6 pin, same as `AUDIO_ENABLE`.

`VARIABLE_TRACE`

Use this to debug changes to variable values, see the [tracing variables](unit_testing.md#tracing-variables) section of the Unit Testing page for more information.

`API_SYSEX_ENABLE`

This enables using the Quantum SYSEX API to send strings (somewhere?)

`KEY_LOCK_ENABLE`

This enables [key lock](feature_key_lock.md).

`SPLIT_KEYBOARD`

This enables split keyboard support (dual MCU like the let's split and bakingpy's boards) and includes all necessary files located at quantum/split_common

`SPLIT_TRANSPORT`

As there is no standard split communication driver for ARM-based split keyboards yet, `SPLIT_TRANSPORT = custom` must be used for these. It will prevent the standard split keyboard communication code (which is AVR-specific) from being included, allowing a custom implementation to be used.

`CUSTOM_MATRIX`

Lets you replace the default matrix scanning routine with your own code. For further details, see the [Custom Matrix page](custom_matrix.md).

`DEBOUNCE_TYPE`

Lets you replace the default key debouncing routine with an alternative one. If `custom` you will need to provide your own implementation.

## Customizing Makefile Options on a Per-Keymap Basis

If your keymap directory has a file called `rules.mk` any options you set in that file will take precedence over other `rules.mk` options for your particular keyboard.

So let's say your keyboard's `rules.mk` has `BACKLIGHT_ENABLE = yes`. You want your particular keyboard to not have the backlight, so you make a file called `rules.mk` and specify `BACKLIGHT_ENABLE = no`.
#
# yosys -- Yosys Open SYnthesis Suite
#
# Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
#
# 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.
#

import sys, re, os, signal
import subprocess
if os.name == "posix":
    import resource
from copy import deepcopy
from select import select
from time import time
from queue import Queue, Empty
from threading import Thread


# This is needed so that the recursive SMT2 S-expression parser
# does not run out of stack frames when parsing large expressions
if os.name == "posix":
    smtio_reclimit = 64 * 1024
    if sys.getrecursionlimit() < smtio_reclimit:
        sys.setrecursionlimit(smtio_reclimit)

    current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK)
    if current_rlimit_stack[0] != resource.RLIM_INFINITY:
        smtio_stacksize = 128 * 1024 * 1024
        if os.uname().sysname == "Darwin":
            # MacOS has rather conservative stack limits
            smtio_stacksize = 16 * 1024 * 1024
        if current_rlimit_stack[1] != resource.RLIM_INFINITY:
            smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
        if current_rlimit_stack[0] < smtio_stacksize:
            try:
                resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
            except ValueError:
                # couldn't get more stack, just run with what we have
                pass


# currently running solvers (so we can kill them)
running_solvers = dict()
forced_shutdown = False
solvers_index = 0

def force_shutdown(signum, frame):
    global forced_shutdown
    if not forced_shutdown:
        forced_shutdown = True
        if signum is not None:
            print("<%s>" % signal.Signals(signum).name)
        for p in running_solvers.values():
            # os.killpg(os.getpgid(p.pid), signal.SIGTERM)
            os.kill(p.pid, signal.SIGTERM)
    sys.exit(1)

if os.name == "posix":
    signal.signal(signal.SIGHUP, force_shutdown)
signal.signal(signal.SIGINT, force_shutdown)
signal.signal(signal.SIGTERM, force_shutdown)

def except_hook(exctype, value, traceback):
    if not forced_shutdown:
        sys.__excepthook__(exctype, value, traceback)
    force_shutdown(None, None)

sys.excepthook = except_hook


hex_dict = {
    "0": "0000", "1": "0001", "2": "0010", "3": "0011",
    "4": "0100", "5": "0101", "6": "0110", "7": "0111",
    "8": "1000", "9": "1001", "A": "1010", "B": "1011",
    "C": "1100", "D": "1101", "E": "1110", "F": "1111",
    "a": "1010", "b": "1011", "c": "1100", "d": "1101",
    "e": "1110", "f": "1111"
}


class SmtModInfo:
    def __init__(self):
        self.inputs = set()
        self.outputs = set()
        self.registers = set()
        self.memories = dict()
        self.wires = set()
        self.wsize = dict()
        self.clocks = dict()
        self.cells = dict()
        self.asserts = dict()
        self.covers = dict()
        self.anyconsts = dict()
        self.anyseqs = dict()
        self.allconsts = dict()
        self.allseqs = dict()
        self.asize = dict()


class SmtIo:
    def __init__(self, opts=None):
        global solvers_index

        self.logic = None
        self.logic_qf = True
        self.logic_ax = True
        self.logic_uf = True
        self.logic_bv = True
        self.logic_dt = False
        self.forall = False
        self.produce_models = True
        self.smt2cache = [list()]
        self.p = None
        self.p_index = solvers_index
        solvers_index += 1

        if opts is not None:
            self.logic = opts.logic
            self.solver = opts.solver
            self.solver_opts = opts.solver_opts
            self.debug_print = opts.debug_print
            self.debug_file = opts.debug_file
            self.dummy_file = opts.dummy_file
            self.timeinfo = opts.timeinfo
            self.unroll = opts.unroll
            self.noincr = opts.noincr
            self.info_stmts = opts.info_stmts
            self.nocomments = opts.nocomments

        else:
            self.solver = "yices"
            self.solver_opts = list()
            self.debug_print = False
            self.debug_file = None
            self.dummy_file = None
            self.timeinfo = os.name != "nt"
            self.unroll = False
            self.noincr = False
            self.info_stmts = list()
            self.nocomments = False

        self.start_time = time()

        self.modinfo = dict()
        self.curmod = None
        self.topmod = None
        self.setup_done = False

    def __del__(self):
        if self.p is not None and not forced_shutdown:
            os.killpg(os.getpgid(self.p.pid), signal.SIGTERM)
            if running_solvers is not None:
                del running_solvers[self.p_index]

    def setup(self):
        assert not self.setup_done

        if self.forall:
            self.unroll = False

        if self.solver == "yices":
            if self.noincr:
                self.popen_vargs = ['yices-smt2'] + self.solver_opts
            else:
                self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts

        if self.solver == "z3":
            self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts

        if self.solver == "cvc4":
            if self.noincr:
                self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
            else:
                self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts

        if self.solver == "mathsat":
            self.popen_vargs = ['mathsat'] + self.solver_opts

        if self.solver == "boolector":
            if self.noincr:
                self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
            else:
                self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
            self.unroll = True

        if self.solver == "abc":
            if len(self.solver_opts) > 0:
                self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
            else:
                self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
            self.logic_ax = False
            self.unroll = True
            self.noincr = True

        if self.solver == "dummy":
            assert self.dummy_file is not None
            self.dummy_fd = open(self.dummy_file, "r")
        else:
            if self.dummy_file is not None:
                self.dummy_fd = open(self.dummy_file, "w")
            if not self.noincr:
                self.p_open()

        if self.unroll:
            assert not self.forall
            self.logic_uf = False
            self.unroll_idcnt = 0
            self.unroll_buffer = ""
            self.unroll_sorts = set()
            self.unroll_objs = set()
            self.unroll_decls = dict()
            self.unroll_cache = dict()
            self.unroll_stack = list()

        if self.logic is None:
            self.logic = ""
            if self.logic_qf: self.logic += "QF_"
            if self.logic_ax: self.logic += "A"
            if self.logic_uf: self.logic += "UF"
            if self.logic_bv: self.logic += "BV"
            if self.logic_dt: self.logic = "ALL"

        self.setup_done = True

        for stmt in self.info_stmts:
            self.write(stmt)

        if self.produce_models:
            self.write("(set-option :produce-models true)")

        self.write("(set-logic %s)" % self.logic)

    def timestamp(self):
        secs = int(time() - self.start_time)
        return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)

    def replace_in_stmt(self, stmt, pat, repl):
        if stmt == pat:
            return repl

        if isinstance(stmt, list):
            return [self.replace_in_stmt(s, pat, repl) for s in stmt]

        return stmt

    def unroll_stmt(self, stmt):
        if not isinstance(stmt, list):
            return stmt

        stmt = [self.unroll_stmt(s) for s in stmt]

        if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls:
            assert stmt[1] in self.unroll_objs

            key = tuple(stmt)
            if key not in self.unroll_cache:
                decl = deepcopy(self.unroll_decls[key[0]])

                self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
                decl[1] = self.unroll_cache[key]
                self.unroll_idcnt += 1

                if decl[0] == "declare-fun":
                    if isinstance(decl[3], list) or decl[3] not in self.unroll_sorts:
                        self.unroll_objs.add(decl[1])
                        decl[2] = list()
                    else:
                        self.unroll_objs.add(decl[1])
                        decl = list()

                elif decl[0] == "define-fun":
                    arg_index = 1
                    for arg_name, arg_sort in decl[2]:
                        decl[4] = self.replace_in_stmt(decl[4], arg_name, key[arg_index])
                        arg_index += 1
                    decl[2] = list()

                if len(decl) > 0:
                    decl = self.unroll_stmt(decl)
                    self.write(self.unparse(decl), unroll=False)

            return self.unroll_cache[key]

        return stmt

    def p_thread_main(self):
        while True:
            data = self.p.stdout.readline().decode("ascii")
            if data == "": break
            self.p_queue.put(data)
        self.p_queue.put("")
        self.p_running = False

    def p_open(self):
        assert self.p is None
        self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
        running_solvers[self.p_index] = self.p
        self.p_running = True
        self.p_next = None
        self.p_queue = Queue()
        self.p_thread = Thread(target=self.p_thread_main)
        self.p_thread.start()

    def p_write(self, data, flush):
        assert self.p is not None
        self.p.stdin.write(bytes(data, "ascii"))
        if flush: self.p.stdin.flush()

    def p_read(self):
        assert self.p is not None
        if self.p_next is not None:
            data = self.p_next
            self.p_next = None
            return data
        if not self.p_running:
            return ""
        return self.p_queue.get()

    def p_poll(self, timeout=0.1):
        assert self.p is not None
        assert self.p_running
        if self.p_next is not None:
            return False
        try:
            self.p_next = self.p_queue.get(True, timeout)
            return False
        except Empty:
            return True

    def p_close(self):
        assert self.p is not None
        self.p.stdin.close()
        self.p_thread.join()
        assert not self.p_running
        del running_solvers[self.p_index]
        self.p = None
        self.p_next = None
        self.p_queue = None
        self.p_thread = None

    def write(self, stmt, unroll=True):
        if stmt.startswith(";"):
            self.info(stmt)
            if not self.setup_done:
                self.info_stmts.append(stmt)
                return
        elif not self.setup_done:
            self.setup()

        stmt = stmt.strip()

        if self.nocomments or self.unroll:
            stmt = re.sub(r" *;.*", "", stmt)
            if stmt == "": return

        if unroll and self.unroll:
            stmt = self.unroll_buffer + stmt
            self.unroll_buffer = ""

            s = re.sub(r"\|[^|]*\|", "", stmt)
            if s.count("(") != s.count(")"):
                self.unroll_buffer = stmt + " "
                return

            s = self.parse(stmt)

            if self.debug_print:
                print("-> %s" % s)

            if len(s) == 3 and s[0] == "declare-sort" and s[2] == "0":
                self.unroll_sorts.add(s[1])
                return

            elif len(s) == 4 and s[0] == "declare-fun" and s[2] == [] and s[3] in self.unroll_sorts:
                self.unroll_objs.add(s[1])
                return

            elif len(s) >= 4 and s[0] == "declare-fun":
                for arg_sort in s[2]:
                    if arg_sort in self.unroll_sorts:
                        self.unroll_decls[s[1]] = s
                        return

            elif len(s) >= 4 and s[0] == "define-fun":
                for arg_name, arg_sort in s[2]:
                    if arg_sort in self.unroll_sorts:
                        self.unroll_decls[s[1]] = s
                        return

            stmt = self.unparse(self.unroll_stmt(s))

            if stmt == "(push 1)":
                self.unroll_stack.append((
                    deepcopy(self.unroll_sorts),
                    deepcopy(self.unroll_objs),
                    deepcopy(self.unroll_decls),
                    deepcopy(self.unroll_cache),
                ))

            if stmt == "(pop 1)":
                self.unroll_sorts, self.unroll_objs, self.unroll_decls, self.unroll_cache = self.unroll_stack.pop()

        if self.debug_print:
            print("> %s" % stmt)

        if self.debug_file:
            print(stmt, file=self.debug_file)
            self.debug_file.flush()

        if self.solver != "dummy":
            if self.noincr:
                if self.p is not None and not stmt.startswith("(get-"):
                    self.p_close()
                if stmt == "(push 1)":
                    self.smt2cache.append(list())
                elif stmt == "(pop 1)":
                    self.smt2cache.pop()
                else:
                    if self.p is not None:
                        self.p_write(stmt + "\n", True)
                    self.smt2cache[-1].append(stmt)
            else:
                self.p_write(stmt + "\n", True)

    def info(self, stmt):
        if not stmt.startswith("; yosys-smt2-"):
            return

        fields = stmt.split()

        if fields[1] == "yosys-smt2-nomem":
            if self.logic is None:
                self.logic_ax = False

        if fields[1] == "yosys-smt2-nobv":
            if self.logic is None:
                self.logic_bv = False

        if fields[1] == "yosys-smt2-stdt":
            if self.logic is None:
                self.logic_dt = True

        if fields[1] == "yosys-smt2-forall":
            if self.logic is None:
                self.logic_qf = False
            self.forall = True

        if fields[1] == "yosys-smt2-module":
            self.curmod = fields[2]
            self.modinfo[self.curmod] = SmtModInfo()

        if fields[1] == "yosys-smt2-cell":
            self.modinfo[self.curmod].cells[fields[3]] = fields[2]

        if fields[1] == "yosys-smt2-topmod":
            self.topmod = fields[2]

        if fields[1] == "yosys-smt2-input":
            self.modinfo[self.curmod].inputs.add(fields[2])
            self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])

        if fields[1] == "yosys-smt2-output":
            self.modinfo[self.curmod].outputs.add(fields[2])
            self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])

        if fields[1] == "yosys-smt2-register":
            self.modinfo[self.curmod].registers.add(fields[2])
            self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])

        if fields[1] == "yosys-smt2-memory":
            self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]), int(fields[6]), fields[7] == "async")

        if fields[1] == "yosys-smt2-wire":
            self.modinfo[self.curmod].wires.add(fields[2])
            self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])

        if fields[1] == "yosys-smt2-clock":
            for edge in fields[3:]:
                if fields[2] not in self.modinfo[self.curmod].clocks:
                    self.modinfo[self.curmod].clocks[fields[2]] = edge
                elif self.modinfo[self.curmod].clocks[fields[2]] != edge:
                    self.modinfo[self.curmod].clocks[fields[2]] = "event"

        if fields[1] == "yosys-smt2-assert":
            self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]

        if fields[1] == "yosys-smt2-cover":
            self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]

        if fields[1] == "yosys-smt2-anyconst":
            self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])

        if fields[1] == "yosys-smt2-anyseq":
            self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])

        if fields[1] == "yosys-smt2-allconst":
            self.modinfo[self.curmod].allconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])

        if fields[1] == "yosys-smt2-allseq":
            self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
            self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])

    def hiernets(self, top, regs_only=False):
        def hiernets_worker(nets, mod, cursor):
            for netname in sorted(self.modinfo[mod].wsize.keys()):
                if not regs_only or netname in self.modinfo[mod].registers:
                    nets.append(cursor + [netname])
            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                hiernets_worker(nets, celltype, cursor + [cellname])

        nets = list()
        hiernets_worker(nets, top, [])
        return nets

    def hieranyconsts(self, top):
        def worker(results, mod, cursor):
            for name, value in sorted(self.modinfo[mod].anyconsts.items()):
                width = self.modinfo[mod].asize[name]
                results.append((cursor, name, value[0], value[1], width))
            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                worker(results, celltype, cursor + [cellname])

        results = list()
        worker(results, top, [])
        return results

    def hieranyseqs(self, top):
        def worker(results, mod, cursor):
            for name, value in sorted(self.modinfo[mod].anyseqs.items()):
                width = self.modinfo[mod].asize[name]
                results.append((cursor, name, value[0], value[1], width))
            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                worker(results, celltype, cursor + [cellname])

        results = list()
        worker(results, top, [])
        return results

    def hierallconsts(self, top):
        def worker(results, mod, cursor):
            for name, value in sorted(self.modinfo[mod].allconsts.items()):
                width = self.modinfo[mod].asize[name]
                results.append((cursor, name, value[0], value[1], width))
            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                worker(results, celltype, cursor + [cellname])

        results = list()
        worker(results, top, [])
        return results

    def hierallseqs(self, top):
        def worker(results, mod, cursor):
            for name, value in sorted(self.modinfo[mod].allseqs.items()):
                width = self.modinfo[mod].asize[name]
                results.append((cursor, name, value[0], value[1], width))
            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                worker(results, celltype, cursor + [cellname])

        results = list()
        worker(results, top, [])
        return results

    def hiermems(self, top):
        def hiermems_worker(mems, mod, cursor):
            for memname in sorted(self.modinfo[mod].memories.keys()):
                mems.append(cursor + [memname])
            for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
                hiermems_worker(mems, celltype, cursor + [cellname])

        mems = list()
        hiermems_worker(mems, top, [])
        return mems

    def read(self):
        stmt = []
        count_brackets = 0

        while True:
            if self.solver == "dummy":
                line = self.dummy_fd.readline().strip()
            else:
                line = self.p_read().strip()
                if self.dummy_file is not None:
                    self.dummy_fd.write(line + "\n")

            count_brackets += line.count("(")
            count_brackets -= line.count(")")
            stmt.append(line)

            if self.debug_print:
                print("< %s" % line)
            if count_brackets == 0:
                break
            if self.solver != "dummy" and self.p.poll():
                print("%s Solver terminated unexpectedly: %s" % (self.timestamp(), "".join(stmt)), flush=True)
                sys.exit(1)

        stmt = "".join(stmt)
        if stmt.startswith("(error"):
            print("%s Solver Error: %s" % (self.timestamp(), stmt), flush=True)
            if self.solver != "dummy":
                self.p_close()
            sys.exit(1)

        return stmt

    def check_sat(self):
        if self.debug_print:
            print("> (check-sat)")
        if self.debug_file and not self.nocomments:
            print("; running check-sat..", file=self.debug_file)
            self.debug_file.flush()

        if self.solver != "dummy":
            if self.noincr:
                if self.p is not None:
                    self.p_close()
                self.p_open()
                for cache_ctx in self.smt2cache:
                    for cache_stmt in cache_ctx:
                        self.p_write(cache_stmt + "\n", False)

            self.p_write("(check-sat)\n", True)

            if self.timeinfo:
                i = 0
                s = "/-\|"

                count = 0
                num_bs = 0
                while self.p_poll():
                    count += 1

                    if count < 25:
                        continue

                    if count % 10 == 0 or count == 25:
                        secs = count // 10

                        if secs < 60:
                            m = "(%d seconds)" % secs
                        elif secs < 60*60:
                            m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
                        else:
                            m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)

                        print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
                        num_bs = len(m) + 3

                    else:
                        print("\b" + s[i], end="", file=sys.stderr)

                    sys.stderr.flush()
                    i = (i + 1) % len(s)

                if num_bs != 0:
                    print("\b \b" * num_bs, end="", file=sys.stderr)
                    sys.stderr.flush()

            else:
                count = 0
                while self.p_poll(60):
                    count += 1
                    msg = None

                    if count == 1:
                        msg = "1 minute"

                    elif count in [5, 10, 15, 30]:
                        msg = "%d minutes" % count

                    elif count == 60:
                        msg = "1 hour"

                    elif count % 60 == 0:
                        msg = "%d hours" % (count // 60)

                    if msg is not None:
                        print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)

        result = self.read()

        if self.debug_file:
            print("(set-info :status %s)" % result, file=self.debug_file)
            print("(check-sat)", file=self.debug_file)
            self.debug_file.flush()

        if result not in ["sat", "unsat"]:
            if result == "":
                print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
            else:
                print("%s Unexpected response from solver: %s" % (self.timestamp(), result), flush=True)
            if self.solver != "dummy":
                self.p_close()
            sys.exit(1)

        return result

    def parse(self, stmt):
        def worker(stmt):
            if stmt[0] == '(':
                expr = []
                cursor = 1
                while stmt[cursor] != ')':
                    el, le = worker(stmt[cursor:])
                    expr.append(el)
                    cursor += le
                return expr, cursor+1

            if stmt[0] == '|':
                expr = "|"
                cursor = 1
                while stmt[cursor] != '|':
                    expr += stmt[cursor]
                    cursor += 1
                expr += "|"
                return expr, cursor+1

            if stmt[0] in [" ", "\t", "\r", "\n"]:
                el, le = worker(stmt[1:])
                return el, le+1

            expr = ""
            cursor = 0
            while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
                expr += stmt[cursor]
                cursor += 1
            return expr, cursor
        return worker(stmt)[0]

    def unparse(self, stmt):
        if isinstance(stmt, list):
            return "(" + " ".join([self.unparse(s) for s in stmt]) + ")"
        return stmt

    def bv2hex(self, v):
        h = ""
        v = self.bv2bin(v)
        while len(v) > 0:
            d = 0
            if len(v) > 0 and v[-1] == "1": d += 1
            if len(v) > 1 and v[-2] == "1": d += 2
            if len(v) > 2 and v[-3] == "1": d += 4
            if len(v) > 3 and v[-4] == "1": d += 8
            h = hex(d)[2:] + h
            if len(v) < 4: break
            v = v[:-4]
        return h

    def bv2bin(self, v):
        if type(v) is list and len(v) == 3 and v[0] == "_" and v[1].startswith("bv"):
            x, n = int(v[1][2:]), int(v[2])
            return "".join("1" if (x & (1 << i)) else "0" for i in range(n-1, -1, -1))
        if v == "true": return "1"
        if v == "false": return "0"
        if v.startswith("#b"):
            return v[2:]
        if v.startswith("#x"):
            return "".join(hex_dict.get(x) for x in v[2:])
        assert False

    def bv2int(self, v):
        return int(self.bv2bin(v), 2)

    def get(self, expr):
        self.write("(get-value (%s))" % (expr))
        return self.parse(self.read())[0][1]

    def get_list(self, expr_list):
        if len(expr_list) == 0:
            return []
        self.write("(get-value (%s))" % " ".join(expr_list))
        return [n[1] for n in self.parse(self.read())]

    def get_path(self, mod, path):
        assert mod in self.modinfo
        path = path.replace("\\", "/").split(".")

        for i in range(len(path)-1):
            first = ".".join(path[0:i+1])
            second = ".".join(path[i+1:])

            if first in self.modinfo[mod].cells:
                nextmod = self.modinfo[mod].cells[first]
                return [first] + self.get_path(nextmod, second)

        return [".".join(path)]

    def net_expr(self, mod, base, path):
        if len(path) == 0:
            return base

        if len(path) == 1:
            assert mod in self.modinfo
            if path[0] == "":
                return base
            if path[0] in self.modinfo[mod].cells:
                return "(|%s_h %s| %s)" % (mod, path[0], base)
            if path[0] in self.modinfo[mod].wsize:
                return "(|%s_n %s| %s)" % (mod, path[0], base)
            if path[0] in self.modinfo[mod].memories:
                return "(|%s_m %s| %s)" % (mod, path[0], base)
            assert 0

        assert mod in self.modinfo
        assert path[0] in self.modinfo[mod].cells

        nextmod = self.modinfo[mod].cells[path[0]]
        nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
        return self.net_expr(nextmod, nextbase, path[1:])

    def net_width(self, mod, net_path):
        for i in range(len(net_path)-1):
            assert mod in self.modinfo
            assert net_path[i] in self.modinfo[mod].cells
            mod = self.modinfo[mod].cells[net_path[i]]

        assert mod in self.modinfo
        assert net_path[-1] in self.modinfo[mod].wsize
        return self.modinfo[mod].wsize[net_path[-1]]

    def net_clock(self, mod, net_path):
        for i in range(len(net_path)-1):
            assert mod in self.modinfo
            assert net_path[i] in self.modinfo[mod].cells
            mod = self.modinfo[mod].cells[net_path[i]]

        assert mod in self.modinfo
        if net_path[-1] not in self.modinfo[mod].clocks:
            return None
        return self.modinfo[mod].clocks[net_path[-1]]

    def net_exists(self, mod, net_path):
        for i in range(len(net_path)-1):
            if mod not in self.modinfo: return False
            if net_path[i] not in self.modinfo[mod].cells: return False
            mod = self.modinfo[mod].cells[net_path[i]]

        if mod not in self.modinfo: return False
        if net_path[-1] not in self.modinfo[mod].wsize: return False
        return True

    def mem_exists(self, mod, mem_path):
        for i in range(len(mem_path)-1):
            if mod not in self.modinfo: return False
            if mem_path[i] not in self.modinfo[mod].cells: return False
            mod = self.modinfo[mod].cells[mem_path[i]]

        if mod not in self.modinfo: return False
        if mem_path[-1] not in self.modinfo[mod].memories: return False
        return True

    def mem_expr(self, mod, base, path, port=None, infomode=False):
        if len(path) == 1:
            assert mod in self.modinfo
            assert path[0] in self.modinfo[mod].memories
            if infomode:
                return self.modinfo[mod].memories[path[0]]
            return "(|%s_m%s %s| %s)" % (mod, "" if port is None else ":%s" % port, path[0], base)

        assert mod in self.modinfo
        assert path[0] in self.modinfo[mod].cells

        nextmod = self.modinfo[mod].cells[path[0]]
        nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
        return self.mem_expr(nextmod, nextbase, path[1:], port=port, infomode=infomode)

    def mem_info(self, mod, path):
        return self.mem_expr(mod, "", path, infomode=True)

    def get_net(self, mod_name, net_path, state_name):
        return self.get(self.net_expr(mod_name, state_name, net_path))

    def get_net_list(self, mod_name, net_path_list, state_name):
        return self.get_list([self.net_expr(mod_name, state_name, n) for n in net_path_list])

    def get_net_hex(self, mod_name, net_path, state_name):
        return self.bv2hex(self.get_net(mod_name, net_path, state_name))

    def get_net_hex_list(self, mod_name, net_path_list, state_name):
        return [self.bv2hex(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]

    def get_net_bin(self, mod_name, net_path, state_name):
        return self.bv2bin(self.get_net(mod_name, net_path, state_name))

    def get_net_bin_list(self, mod_name, net_path_list, state_name):
        return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]

    def wait(self):
        if self.p is not None:
            self.p.wait()
            self.p_close()


class SmtOpts:
    def __init__(self):
        self.shortopts = "s:S:v"
        self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
        self.solver = "yices"
        self.solver_opts = list()
        self.debug_print = False
        self.debug_file = None
        self.dummy_file = None
        self.unroll = False
        self.noincr = False
        self.timeinfo = os.name != "nt"
        self.logic = None
        self.info_stmts = list()
        self.nocomments = False

    def handle(self, o, a):
        if o == "-s":
            self.solver = a
        elif o == "-S":
            self.solver_opts.append(a)
        elif o == "-v":
            self.debug_print = True
        elif o == "--unroll":
            self.unroll = True
        elif o == "--noincr":
            self.noincr = True
        elif o == "--noprogress":
            self.timeinfo = False
        elif o == "--dump-smt2":
            self.debug_file = open(a, "w")
        elif o == "--logic":
            self.logic = a
        elif o == "--dummy":
            self.dummy_file = a
        elif o == "--info":
            self.info_stmts.append(a)
        elif o == "--nocomments":
            self.nocomments = True
        else:
            return False
        return True

    def helpmsg(self):
        return """
    -s <solver>
        set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
        default: yices

    -S <opt>
        pass <opt> as command line argument to the solver

    --logic <smt2_logic>
        use the specified SMT2 logic (e.g. QF_AUFBV)

    --dummy <filename>
        if solver is "dummy", read solver output from that file
        otherwise: write solver output to that file

    -v
        enable debug output

    --unroll
        unroll uninterpreted functions

    --noincr
        don't use incremental solving, instead restart solver for
        each (check-sat). This also avoids (push) and (pop).

    --noprogress
        disable timer display during solving
        (this option is set implicitly on Windows)

    --dump-smt2 <filename>
        write smt2 statements to file

    --info <smt2-info-stmt>
        include the specified smt2 info statement in the smt2 output

    --nocomments
        strip all comments from the generated smt2 code
"""


class MkVcd:
    def __init__(self, f):
        self.f = f
        self.t = -1
        self.nets = dict()
        self.clocks = dict()

    def add_net(self, path, width):
        path = tuple(path)
        assert self.t == -1
        key = "n%d" % len(self.nets)
        self.nets[path] = (key, width)

    def add_clock(self, path, edge):
        path = tuple(path)
        assert self.t == -1
        key = "n%d" % len(self.nets)
        self.nets[path] = (key, 1)
        self.clocks[path] = (key, edge)

    def set_net(self, path, bits):
        path = tuple(path)
        assert self.t >= 0
        assert path in self.nets
        if path not in self.clocks:
            print("b%s %s" % (bits, self.nets[path][0]), file=self.f)

    def escape_name(self, name):
        name = re.sub(r"\[([0-9a-zA-Z_]*[a-zA-Z_][0-9a-zA-Z_]*)\]", r"<\1>", name)
        if re.match("[\[\]]", name) and name[0] != "\\":
            name = "\\" + name
        return name

    def set_time(self, t):
        assert t >= self.t
        if t != self.t:
            if self.t == -1:
                print("$version Generated by Yosys-SMTBMC $end", file=self.f)
                print("$timescale 1ns $end", file=self.f)
                print("$var integer 32 t smt_step $end", file=self.f)
                print("$var event 1 ! smt_clock $end", file=self.f)

                scope = []
                for path in sorted(self.nets):
                    key, width = self.nets[path]

                    uipath = list(path)
                    if "." in uipath[-1]:
                        uipath = uipath[0:-1] + uipath[-1].split(".")
                    for i in range(len(uipath)):
                        uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i])

                    while uipath[:len(scope)] != scope:
                        print("$upscope $end", file=self.f)
                        scope = scope[:-1]

                    while uipath[:-1] != scope:
                        scopename = uipath[len(scope)]
                        if scopename.startswith("$"):
                            scopename = "\\" + scopename
                        print("$scope module %s $end" % scopename, file=self.f)
                        scope.append(uipath[len(scope)])

                    if path in self.clocks and self.clocks[path][1] == "event":
                        print("$var event 1 %s %s $end" % (key, uipath[-1]), file=self.f)
                    else:
                        print("$var wire %d %s %s $end" % (width, key, uipath[-1]), file=self.f)

                for i in range(len(scope)):
                    print("$upscope $end", file=self.f)

                print("$enddefinitions $end", file=self.f)

            self.t = t
            assert self.t >= 0

            if self.t > 0:
                print("#%d" % (10 * self.t - 5), file=self.f)
                for path in sorted(self.clocks.keys()):
                    if self.clocks[path][1] == "posedge":
                        print("b0 %s" % self.nets[path][0], file=self.f)
                    elif self.clocks[path][1] == "negedge":
                        print("b1 %s" % self.nets[path][0], file=self.f)

            print("#%d" % (10 * self.t), file=self.f)
            print("1!", file=self.f)
            print("b%s t" % format(self.t, "032b"), file=self.f)

            for path in sorted(self.clocks.keys()):
                if self.clocks[path][1] == "negedge":
                    print("b0 %s" % self.nets[path][0], file=self.f)
                else:
                    print("b1 %s" % self.nets[path][0], file=self.f)