aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
blob: da5a7f57ed8f8c09b82757eecc711e3d6113bc10 (plain)
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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
2
/*
    ChibiOS/RT - Copyright (C) 2006,2007,2008,2009,2010,
                 2011,2012,2013 Giovanni Di Sirio.

    This file is part of ChibiOS/RT.

    ChibiOS/RT is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 3 of the License, or
    (at your option) any later version.

    ChibiOS/RT is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
*/

/**
 * @file    mmc_spi.h
 * @brief   MMC over SPI driver header.
 *
 * @addtogroup MMC_SPI
 * @{
 */

#ifndef _MMC_SPI_H_
#define _MMC_SPI_H_

#if HAL_USE_MMC_SPI || defined(__DOXYGEN__)

/*===========================================================================*/
/* Driver constants.                                                         */
/*===========================================================================*/

#define MMC_CMD0_RETRY              10
#define MMC_CMD1_RETRY              100
#define MMC_ACMD41_RETRY            100
#define MMC_WAIT_DATA               10000

/*===========================================================================*/
/* Driver pre-compile time settings.                                         */
/*===========================================================================*/

/**
 * @name    MMC_SPI configuration options
 * @{
 */
/**
 * @brief   Delays insertions.
 * @details If enabled this options inserts delays into the MMC waiting
 *          routines releasing some extra CPU time for the threads with
 *          lower priority, this may slow down the driver a bit however.
 *          This option is recommended also if the SPI driver does not
 *          use a DMA channel and heavily loads the CPU.
 */
#if !defined(MMC_NICE_WAITING) || defined(__DOXYGEN__)
#define MMC_NICE_WAITING            TRUE
#endif
/** @} */

/*===========================================================================*/
/* Derived constants and error checks.                                       */
/*===========================================================================*/

#if !HAL_USE_SPI || !SPI_USE_WAIT || !CH_USE_EVENTS
#error "MMC_SPI driver requires HAL_USE_SPI, SPI_USE_WAIT and CH_USE_EVENTS"
#endif

/*===========================================================================*/
/* Driver data structures and types.                                         */
/*===========================================================================*/

/**
 * @brief   MMC/SD over SPI driver configuration structure.
 */
typedef struct {
  /**
   * @brief SPI driver associated to this MMC driver.
   */
  SPIDriver             *spip;
  /**
   * @brief SPI low speed configuration used during initialization.
   */
  const SPIConfig       *lscfg;
  /**
   * @brief SPI high speed configuration used during transfers.
   */
  const SPIConfig       *hscfg;
} MMCConfig;

/**
 * @brief   @p MMCDriver specific methods.
 */
#define _mmc_driver_methods                                                 \
  _mmcsd_block_device_methods

/**
 * @extends MMCSDBlockDeviceVMT
 *
 * @brief   @p MMCDriver virtual methods table.
 */
struct MMCDriverVMT {
  _mmc_driver_methods
};

/**
 * @extends MMCSDBlockDevice
 *
 * @brief   Structure representing a MMC/SD over SPI driver.
 */
typedef struct {
  /**
   * @brief Virtual Methods Table.
   */
  const struct MMCDriverVMT *vmt;
  _mmcsd_block_device_data
  /**
   * @brief Current configuration data.
   */
  const MMCConfig       *config;
  /***
   * @brief Addresses use blocks instead of bytes.
   */
  bool_t                block_addresses;
} MMCDriver;

/*===========================================================================*/
/* Driver macros.                                                            */
/*===========================================================================*/

/**
 * @name    Macro Functions
 * @{
 */
/**
 * @brief   Returns the card insertion status.
 * @note    This macro wraps a low level function named
 *          @p sdc_lld_is_card_inserted(), this function must be
 *          provided by the application because it is not part of the
 *          SDC driver.
 *
 * @param[in] mmcp      pointer to the @p MMCDriver object
 * @return              The card state.
 * @retval FALSE        card not inserted.
 * @retval TRUE         card inserted.
 *
 * @api
 */
#define mmcIsCardInserted(mmcp) mmc_lld_is_card_inserted(mmcp)

/**
 * @brief   Returns the write protect status.
 *
 * @param[in] mmcp      pointer to the @p MMCDriver object
 * @return              The card state.
 * @retval FALSE        card not inserted.
 * @retval TRUE         card inserted.
 *
 * @api
 */
#define mmcIsWriteProtected(mmcp) mmc_lld_is_write_protected(mmcp)
/** @} */

/*===========================================================================*/
/* External declarations.                                                    */
/*===========================================================================*/

#ifdef __cplusplus
extern "C" {
#endif
  void mmcInit(void);
  void mmcObjectInit(MMCDriver *mmcp);
  void mmcStart(MMCDriver *mmcp, const MMCConfig *config);
  void mmcStop(MMCDriver *mmcp);
  bool_t mmcConnect(MMCDriver *mmcp);
  bool_t mmcDisconnect(MMCDriver *mmcp);
  bool_t mmcStartSequentialRead(MMCDriver *mmcp, uint32_t startblk);
  bool_t mmcSequentialRead(MMCDriver *mmcp, uint8_t *buffer);
  bool_t mmcStopSequentialRead(MMCDriver *mmcp);
  bool_t mmcStartSequentialWrite(MMCDriver *mmcp, uint32_t startblk);
  bool_t mmcSequentialWrite(MMCDriver *mmcp, const uint8_t *buffer);
  bool_t mmcStopSequentialWrite(MMCDriver *mmcp);
  bool_t mmcSync(MMCDriver *mmcp);
  bool_t mmcGetInfo(MMCDriver *mmcp, BlockDeviceInfo *bdip);
  bool_t mmcErase(MMCDriver *mmcp, uint32_t startblk, uint32_t endblk);
  bool_t mmc_lld_is_card_inserted(MMCDriver *mmcp);
  bool_t mmc_lld_is_write_protected(MMCDriver *mmcp);
#ifdef __cplusplus
}
#endif

#endif /* HAL_USE_MMC_SPI */

#endif /* _MMC_SPI_H_ */

/** @} */
/a> 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599
#!/usr/bin/env python3
#
# 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 os, sys, getopt, re
##yosys-sys-path##
from smtio import SmtIo, SmtOpts, MkVcd
from collections import defaultdict

got_topt = False
skip_steps = 0
step_size = 1
num_steps = 20
append_steps = 0
vcdfile = None
cexfile = None
aimfile = None
aiwfile = None
aigheader = True
btorwitfile = None
vlogtbfile = None
vlogtbtop = None
inconstr = list()
outconstr = None
gentrace = False
covermode = False
tempind = False
dumpall = False
assume_skipped = None
final_only = False
topmod = None
noinfo = False
presat = False
smtcinit = False
smtctop = None
noinit = False
binarymode = False
so = SmtOpts()


def usage():
    print(os.path.basename(sys.argv[0]) + """ [options] <yosys_smt2_output>

    -t <num_steps>
    -t <skip_steps>:<num_steps>
    -t <skip_steps>:<step_size>:<num_steps>
        default: skip_steps=0, step_size=1, num_steps=20

    -g
        generate an arbitrary trace that satisfies
        all assertions and assumptions.

    -i
        instead of BMC run temporal induction

    -c
        instead of regular BMC run cover analysis

    -m <module_name>
        name of the top module

    --smtc <constr_filename>
        read constraints file

    --cex <cex_filename>
        read cex file as written by ABC's "write_cex -n"

    --aig <prefix>
        read AIGER map file (as written by Yosys' "write_aiger -map")
        and AIGER witness file. The file names are <prefix>.aim for
        the map file and <prefix>.aiw for the witness file.

    --aig <aim_filename>:<aiw_filename>
        like above, but for map files and witness files that do not
        share a filename prefix (or use different file extensions).

    --aig-noheader
        the AIGER witness file does not include the status and
        properties lines.

    --btorwit <btor_witness_filename>
        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
        this will also help to "warm up" the solver, potentially
        yielding a speedup.

    --final-only
        only check final constraints, assume base case

    --assume-skipped <start_step>
        assume asserts in skipped steps in BMC.
        no assumptions are created for skipped steps
        before <start_step>.

    --dump-vcd <vcd_filename>
        write trace to this VCD file
        (hint: use 'write_smt2 -wires' for maximum
        coverage of signals in generated VCD file)

    --dump-vlogtb <verilog_filename>
        write trace as Verilog test bench

    --vlogtb-top <hierarchical_name>
        use the given entity as top module for the generated
        Verilog test bench. The <hierarchical_name> is relative
        to the design top module without the top module name.

    --dump-smtc <constr_filename>
        write trace as constraints file

    --smtc-init
        write just the last state as initial constraint to smtc file

    --smtc-top <old>[:<new>]
        replace <old> with <new> in constraints dumped to smtc
        file and only dump object below <old> 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 replaces in all dump
        filenames with the step number.

    --append <num_steps>
        add <num_steps> 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
""" + so.helpmsg())
    sys.exit(1)


try:
    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
             "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
             "smtc-init", "smtc-top=", "noinit", "binary"])
except:
    usage()

for o, a in opts:
    if o == "-t":
        got_topt = True
        a = a.split(":")
        if len(a) == 1:
            num_steps = int(a[0])
        elif len(a) == 2:
            skip_steps = int(a[0])
            num_steps = int(a[1])
        elif len(a) == 3:
            skip_steps = int(a[0])
            step_size = int(a[1])
            num_steps = int(a[2])
        else:
            assert False
    elif o == "--assume-skipped":
        assume_skipped = int(a)
    elif o == "--final-only":
        final_only = True
    elif o == "--smtc":
        inconstr.append(a)
    elif o == "--cex":
        cexfile = a
    elif o == "--aig":
        if ":" in a:
            aimfile, aiwfile = a.split(":")
        else:
            aimfile = a + ".aim"
            aiwfile = a + ".aiw"
    elif o == "--aig-noheader":
        aigheader = False
    elif o == "--btorwit":
        btorwitfile = a
    elif o == "--dump-vcd":
        vcdfile = a
    elif o == "--dump-vlogtb":
        vlogtbfile = a
    elif o == "--vlogtb-top":
        vlogtbtop = a
    elif o == "--dump-smtc":
        outconstr = a
    elif o == "--smtc-init":
        smtcinit = True
    elif o == "--smtc-top":
        smtctop = a.split(":")
        if len(smtctop) == 1:
            smtctop.append("")
        assert len(smtctop) == 2
        smtctop = tuple(smtctop)
    elif o == "--dump-all":
        dumpall = True
    elif o == "--presat":
        presat = True
    elif o == "--noinfo":
        noinfo = True
    elif o == "--noinit":
        noinit = True
    elif o == "--append":
        append_steps = int(a)
    elif o == "-i":
        tempind = True
    elif o == "-g":
        gentrace = True
    elif o == "-c":
        covermode = True
    elif o == "-m":
        topmod = a
    elif o == "--binary":
        binarymode = True
    elif so.handle(o, a):
        pass
    else:
        usage()

if len(args) != 1:
    usage()

if sum([tempind, gentrace, covermode]) > 1:
    usage()

constr_final_start = None
constr_asserts = defaultdict(list)
constr_assumes = defaultdict(list)
constr_write = list()

for fn in inconstr:
    current_states = None
    current_line = 0

    with open(fn, "r") as f:
        for line in f:
            current_line += 1

            if line.startswith("#"):
                continue

            tokens = line.split()

            if len(tokens) == 0:
                continue

            if tokens[0] == "initial":
                current_states = set()
                if not tempind:
                    current_states.add(0)
                continue

            if tokens[0] == "final":
                constr_final = True
                if len(tokens) == 1:
                    current_states = set(["final-%d" % i for i in range(0, num_steps+1)])
                    constr_final_start = 0
                elif len(tokens) == 2:
                    arg = abs(int(tokens[1]))
                    current_states = set(["final-%d" % i for i in range(arg, num_steps+1)])
                    constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg)
                else:
                    assert False
                continue

            if tokens[0] == "state":
                current_states = set()
                if not tempind:
                    for token in tokens[1:]:
                        tok = token.split(":")
                        if len(tok) == 1:
                            current_states.add(int(token))
                        elif len(tok) == 2:
                            lower = int(tok[0])
                            if tok[1] == "*":
                                upper = num_steps
                            else:
                                upper = int(tok[1])
                            for i in range(lower, upper+1):
                                current_states.add(i)
                        else:
                            assert False
                continue

            if tokens[0] == "always":
                if len(tokens) == 1:
                    current_states = set(range(0, num_steps+1))
                elif len(tokens) == 2:
                    arg = abs(int(tokens[1]))
                    current_states = set(range(arg, num_steps+1))
                else:
                    assert False
                continue

            if tokens[0] == "assert":
                assert current_states is not None

                for state in current_states:
                    constr_asserts[state].append(("%s:%d" % (fn, current_line), " ".join(tokens[1:])))

                continue

            if tokens[0] == "assume":
                assert current_states is not None

                for state in current_states:
                    constr_assumes[state].append(("%s:%d" % (fn, current_line), " ".join(tokens[1:])))

                continue

            if tokens[0] == "write":
                constr_write.append(" ".join(tokens[1:]))
                continue

            if tokens[0] == "logic":
                so.logic = " ".join(tokens[1:])
                continue

            assert False


def get_constr_expr(db, state, final=False, getvalues=False):
    if final:
        if ("final-%d" % state) not in db:
            return ([], [], []) if getvalues else "true"
    else:
        if state not in db:
            return ([], [], []) if getvalues else "true"

    netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')

    def replace_netref(match):
        state_sel = match.group(2)

        if state_sel == "":
            st = state
        elif state_sel[0] == "-":
            st = state + int(state_sel[:-1])
        else:
            st = int(state_sel[:-1])

        expr = smt.net_expr(topmod, "s%d" % st, smt.get_path(topmod, match.group(3)))

        return match.group(1) + expr

    expr_list = list()
    for loc, expr in db[("final-%d" % state) if final else state]:
        actual_expr = netref_regex.sub(replace_netref, expr)
        if getvalues:
            expr_list.append((loc, expr, actual_expr))
        else:
            expr_list.append(actual_expr)

    if getvalues:
        loc_list, expr_list, acual_expr_list = zip(*expr_list)
        value_list = smt.get_list(acual_expr_list)
        return loc_list, expr_list, value_list

    if len(expr_list) == 0:
        return "true"

    if len(expr_list) == 1:
        return expr_list[0]

    return "(and %s)" % " ".join(expr_list)


smt = SmtIo(opts=so)

if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None:
    smt.produce_models = False

def print_msg(msg):
    print("%s %s" % (smt.timestamp(), msg))
    sys.stdout.flush()

print_msg("Solver: %s" % (so.solver))

with open(args[0], "r") as f:
    for line in f:
        smt.write(line)

for line in constr_write:
    smt.write(line)

if topmod is None:
    topmod = smt.topmod

assert topmod is not None
assert topmod in smt.modinfo

if cexfile is not None:
    if not got_topt:
        assume_skipped = 0
        skip_steps = 0
        num_steps = 0

    with open(cexfile, "r") as f:
        cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
        for entry in f.read().split():
            match = cex_regex.match(entry)
            assert match

            name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5)

            if extra_name != "":
                continue

            if name not in smt.modinfo[topmod].inputs:
                continue

            if bit is None:
                bit = 0
            else:
                bit = int(bit[1:-1])

            step = int(step[1:])
            val = int(val)

            if smt.modinfo[topmod].wsize[name] == 1:
                assert bit == 0
                smtexpr = "(= [%s] %s)" % (name, "true" if val else "false")
            else:
                smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bit, bit, name, val)

            # print("cex@%d: %s" % (step, smtexpr))
            constr_assumes[step].append((cexfile, smtexpr))

            if not got_topt:
                skip_steps = max(skip_steps, step)
                num_steps = max(num_steps, step+1)

if aimfile is not None:
    input_map = dict()
    init_map = dict()
    latch_map = dict()

    if not got_topt:
        assume_skipped = 0
        skip_steps = 0
        num_steps = 0

    with open(aimfile, "r") as f:
        for entry in f.read().splitlines():
            entry = entry.split()

            if entry[0] == "input":
                input_map[int(entry[1])] = (entry[3], int(entry[2]))
                continue

            if entry[0] == "init":
                init_map[int(entry[1])] = (entry[3], int(entry[2]))
                continue

            if entry[0] in ["latch", "invlatch"]:
                latch_map[int(entry[1])] = (entry[3], int(entry[2]), entry[0] == "invlatch")
                continue

            if entry[0] in ["output", "wire"]:
                continue

            assert False

    with open(aiwfile, "r") as f:
        got_state = False
        got_ffinit = False
        step = 0

        if not aigheader:
            got_state = True

        for entry in f.read().splitlines():
            if len(entry) == 0 or entry[0] in "bcjfu.":
                continue

            if not got_state:
                got_state = True
                assert entry == "1"
                continue

            if not got_ffinit:
                got_ffinit = True
                if len(init_map) == 0:
                    for i in range(len(entry)):
                        if entry[i] == "x":
                            continue

                        if i in latch_map:
                            value = int(entry[i])
                            name = latch_map[i][0]
                            bitidx = latch_map[i][1]
                            invert = latch_map[i][2]

                            if invert:
                                value = 1 - value

                            path = smt.get_path(topmod, name)
                            width = smt.net_width(topmod, path)

                            if width == 1:
                                assert bitidx == 0
                                smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
                            else:
                                smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)

                            constr_assumes[0].append((cexfile, smtexpr))
                continue

            for i in range(len(entry)):
                if entry[i] == "x":
                    continue

                if (step == 0) and (i in init_map):
                    value = int(entry[i])
                    name = init_map[i][0]
                    bitidx = init_map[i][1]

                    path = smt.get_path(topmod, name)

                    if not smt.net_exists(topmod, path):
                        match = re.match(r"(.*)\[(\d+)\]$", path[-1])
                        if match:
                            path[-1] = match.group(1)
                            addr = int(match.group(2))

                        if not match or not smt.mem_exists(topmod, path):
                            print_msg("Ignoring init value for unknown net: %s" % (name))
                            continue

                        meminfo = smt.mem_info(topmod, path)
                        smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0]))
                        width = meminfo[1]

                    else:
                        smtexpr = "[%s]" % name
                        width = smt.net_width(topmod, path)

                    if width == 1:
                        assert bitidx == 0
                        smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false")
                    else:
                        smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value)

                    constr_assumes[0].append((cexfile, smtexpr))

                if i in input_map:
                    value = int(entry[i])
                    name = input_map[i][0]
                    bitidx = input_map[i][1]

                    path = smt.get_path(topmod, name)
                    width = smt.net_width(topmod, path)

                    if width == 1:
                        assert bitidx == 0
                        smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
                    else:
                        smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)

                    constr_assumes[step].append((cexfile, smtexpr))

            if not got_topt:
                skip_steps = max(skip_steps, step)
                num_steps = max(num_steps, step+1)
            step += 1

if btorwitfile is not None:
    with open(btorwitfile, "r") as f:
        step = None
        suffix = None
        altsuffix = None
        header_okay = False

        for line in f:
            line = line.strip()

            if line == "sat":
                header_okay = True
                continue

            if not header_okay:
                continue

            if line == "" or line[0] == "b" or line[0] == "j":
                continue

            if line == ".":
                break

            if line[0] == '#' or line[0] == '@':
                step = int(line[1:])
                suffix = line
                altsuffix = suffix
                if suffix[0] == "@":
                    altsuffix = "#" + suffix[1:]
                else:
                    altsuffix = "@" + suffix[1:]
                continue

            line = line.split()

            if len(line) == 0:
                continue

            if line[-1].endswith(suffix):
                line[-1] = line[-1][0:len(line[-1]) - len(suffix)]

            if line[-1].endswith(altsuffix):
                line[-1] = line[-1][0:len(line[-1]) - len(altsuffix)]

            if line[-1][0] == "$":
                continue

            # BV assignments
            if len(line) == 3 and line[1][0] != "[":
                value = line[1]
                name = line[2]

                path = smt.get_path(topmod, name)

                if not smt.net_exists(topmod, path):
                    continue

                width = smt.net_width(topmod, path)

                if width == 1:
                    assert value in ["0", "1"]
                    value = "true" if value == "1" else "false"
                else:
                    value = "#b" + value

                smtexpr = "(= [%s] %s)" % (name, value)
                constr_assumes[step].append((btorwitfile, smtexpr))

            # Array assignments
            if len(line) == 4 and line[1][0] == "[":
                index = line[1]
                value = line[2]
                name = line[3]

                path = smt.get_path(topmod, name)

                if not smt.mem_exists(topmod, path):
                    continue

                meminfo = smt.mem_info(topmod, path)

                if meminfo[1] == 1:
                    assert value in ["0", "1"]
                    value = "true" if value == "1" else "false"
                else:
                    value = "#b" + value

                assert index[0] == "["
                assert index[-1] == "]"
                index = "#b" + index[1:-1]

                smtexpr = "(= (select [%s] %s) %s)" % (name, index, value)
                constr_assumes[step].append((btorwitfile, smtexpr))

        skip_steps = step
        num_steps = step+1

def write_vcd_trace(steps_start, steps_stop, index):
    filename = vcdfile.replace("%", index)
    print_msg("Writing trace to VCD file: %s" % (filename))

    with open(filename, "w") as vcd_file:
        vcd = MkVcd(vcd_file)
        path_list = list()

        for netpath in sorted(smt.hiernets(topmod)):
            hidden_net = False
            for n in netpath:
                if n.startswith("$"):
                    hidden_net = True
            if not hidden_net:
                edge = smt.net_clock(topmod, netpath)
                if edge is None:
                    vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
                else:
                    vcd.add_clock([topmod] + netpath, edge)
                path_list.append(netpath)

        mem_trace_data = dict()
        for mempath in sorted(smt.hiermems(topmod)):
            abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)

            expr_id = list()
            expr_list = list()
            for i in range(steps_start, steps_stop):
                for j in range(rports):
                    expr_id.append(('R', i-steps_start, j, 'A'))
                    expr_id.append(('R', i-steps_start, j, 'D'))
                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
                for j in range(wports):
                    expr_id.append(('W', i-steps_start, j, 'A'))
                    expr_id.append(('W', i-steps_start, j, 'D'))
                    expr_id.append(('W', i-steps_start, j, 'M'))
                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
                    expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))

            rdata = list()
            wdata = list()
            addrs = set()

            for eid, edat in zip(expr_id, smt.get_list(expr_list)):
                t, i, j, f = eid

                if t == 'R':
                    c = rdata
                elif t == 'W':
                    c = wdata
                else:
                    assert False

                while len(c) <= i:
                    c.append(list())
                c = c[i]

                while len(c) <= j:
                    c.append(dict())
                c = c[j]

                c[f] = smt.bv2bin(edat)

                if f == 'A':
                    addrs.add(c[f])

            for addr in addrs:
                tdata = list()
                data = ["x"] * width
                gotread = False

                if len(wdata) == 0 and len(rdata) != 0:
                    wdata = [[]] * len(rdata)

                assert len(rdata) == len(wdata)

                for i in range(len(wdata)):
                    if not gotread:
                        for j_data in rdata[i]:
                            if j_data["A"] == addr:
                                data = list(j_data["D"])
                                gotread = True
                                break

                        if gotread:
                            buf = data[:]
                            for i in reversed(range(len(tdata))):
                                for k in range(width):
                                    if tdata[i][k] == "x":
                                        tdata[i][k] = buf[k]
                                    else:
                                        buf[k] = tdata[i][k]

                    if not asyncwr:
                        tdata.append(data[:])

                    for j_data in wdata[i]:
                        if j_data["A"] != addr:
                            continue

                        D = j_data["D"]
                        M = j_data["M"]

                        for k in range(width):
                            if M[k] == "1":
                                data[k] = D[k]

                    if asyncwr:
                        tdata.append(data[:])

                assert len(tdata) == len(rdata)

                netpath = mempath[:]
                netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int(addr, 2))
                vcd.add_net([topmod] + netpath, width)

                for i in range(steps_start, steps_stop):
                    if i not in mem_trace_data:
                        mem_trace_data[i] = list()
                    mem_trace_data[i].append((netpath, "".join(tdata[i-steps_start])))

        for i in range(steps_start, steps_stop):
            vcd.set_time(i)
            value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
            for path, value in zip(path_list, value_list):
                vcd.set_net([topmod] + path, value)
            if i in mem_trace_data:
                for path, value in mem_trace_data[i]:
                    vcd.set_net([topmod] + path, value)

        vcd.set_time(steps_stop)

def char_ok_in_verilog(c,i):
    if ('A' <= c <= 'Z'): return True
    if ('a' <= c <= 'z'): return True
    if ('0' <= c <= '9' and i>0): return True
    if (c == '_'): return True
    if (c == '$'): return True
    return False

def escape_identifier(identifier):
    if type(identifier) is list: 
        return map(escape_identifier, identifier)
    if "." in identifier:
        return ".".join(escape_identifier(identifier.split(".")))
    if (all(char_ok_in_verilog(identifier[i],i) for i in range(0, len(identifier)))):
        return identifier
    return "\\"+identifier+" "



def write_vlogtb_trace(steps_start, steps_stop, index):
    filename = vlogtbfile.replace("%", index)
    print_msg("Writing trace to Verilog testbench: %s" % (filename))

    vlogtb_topmod = topmod
    vlogtb_state = "s@@step_idx@@"

    if vlogtbtop is not None:
        for item in vlogtbtop.split("."):
            if item in smt.modinfo[vlogtb_topmod].cells:
                vlogtb_state = "(|%s_h %s| %s)" % (vlogtb_topmod, item, vlogtb_state)
                vlogtb_topmod = smt.modinfo[vlogtb_topmod].cells[item]
            else:
                print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop, item, vlogtb_topmod))
                break

    with open(filename, "w") as f:
        print("`ifndef VERILATOR", file=f)
        print("module testbench;", file=f)
        print("  reg [4095:0] vcdfile;", file=f)
        print("  reg clock;", file=f)
        print("`else", file=f)
        print("module testbench(input clock, output reg genclock);", file=f)
        print("  initial genclock = 1;", file=f)
        print("`endif", file=f)

        print("  reg genclock = 1;", file=f)
        print("  reg [31:0] cycle = 0;", file=f)

        primary_inputs = list()
        clock_inputs = set()

        for name in smt.modinfo[vlogtb_topmod].inputs:
            if name in ["clk", "clock", "CLK", "CLOCK"]:
                clock_inputs.add(name)
            width = smt.modinfo[vlogtb_topmod].wsize[name]
            primary_inputs.append((name, width))

        for name, width in primary_inputs:
            if name in clock_inputs:
                print("  wire [%d:0] %s = clock;" % (width-1, escape_identifier("PI_"+name)), file=f)
            else:
                print("  reg [%d:0] %s;" % (width-1, escape_identifier("PI_"+name)), file=f)

        print("  %s UUT (" % escape_identifier(vlogtb_topmod), file=f)
        print(",\n".join("    .%s(%s)" % (escape_identifier(name), escape_identifier("PI_"+name)) for name, _ in primary_inputs), file=f)
        print("  );", file=f)

        print("`ifndef VERILATOR", file=f)
        print("  initial begin", file=f)
        print("    if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f)
        print("      $dumpfile(vcdfile);", file=f)
        print("      $dumpvars(0, testbench);", file=f)
        print("    end", file=f)
        print("    #5 clock = 0;", file=f)
        print("    while (genclock) begin", file=f)
        print("      #5 clock = 0;", file=f)
        print("      #5 clock = 1;", file=f)
        print("    end", file=f)
        print("  end", file=f)
        print("`endif", file=f)

        print("  initial begin", file=f)

        regs = sorted(smt.hiernets(vlogtb_topmod, regs_only=True))
        regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps_start)))

        print("`ifndef VERILATOR", file=f)
        print("    #1;", file=f)
        print("`endif", file=f)
        for reg, val in zip(regs, regvals):
            hidden_net = False
            for n in reg:
                if n.startswith("$"):
                    hidden_net = True
            print("    %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(escape_identifier(reg)), len(val), val), file=f)

        anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod))
        for info in anyconsts:
            if info[3] is not None:
                modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0])
                value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
                print("    UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);

        mems = sorted(smt.hiermems(vlogtb_topmod))
        for mempath in mems:
            abits, width, rports, wports, asyncwr = smt.mem_info(vlogtb_topmod, mempath)

            addr_expr_list = list()
            data_expr_list = list()
            for i in range(steps_start, steps_stop):
                for j in range(rports):
                    addr_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
                    data_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))

            addr_list = smt.get_list(addr_expr_list)
            data_list = smt.get_list(data_expr_list)

            addr_data = dict()
            for addr, data in zip(addr_list, data_list):
                addr = smt.bv2bin(addr)
                data = smt.bv2bin(data)
                if addr not in addr_data:
                    addr_data[addr] = data

            for addr, data in addr_data.items():
                print("    UUT.%s[%d'b%s] = %d'b%s;" % (".".join(escape_identifier(mempath)), len(addr), addr, len(data), data), file=f)

        print("", file=f)
        anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))

        for i in range(steps_start, steps_stop):
            pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
            pi_values = smt.get_net_bin_list(vlogtb_topmod, pi_names, vlogtb_state.replace("@@step_idx@@", str(i)))

            print("    // state %d" % i, file=f)

            if i > 0:
                print("    if (cycle == %d) begin" % (i-1), file=f)

            for name, val in zip(pi_names, pi_values):
                if i > 0:
                    print("      %s <= %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f)
                else:
                    print("    %s = %d'b%s;" % (escape_identifier("PI_"+".".join(name)), len(val), val), file=f)

            for info in anyseqs:
                if info[3] is not None:
                    modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0])
                    value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
                    if i > 0:
                        print("      UUT.%s <= %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);
                    else:
                        print("    UUT.%s = %d'b%s;" % (".".join(escape_identifier(info[0] + [info[3]])), len(value), value), file=f);

            if i > 0:
                print("    end", file=f)
                print("", file=f)

            if i == 0:
                print("  end", file=f)
                print("  always @(posedge clock) begin", file=f)

        print("    genclock <= cycle < %d;" % (steps_stop-1), file=f)
        print("    cycle <= cycle + 1;", file=f)
        print("  end", file=f)

        print("endmodule", file=f)


def write_constr_trace(steps_start, steps_stop, index):
    filename = outconstr.replace("%", index)
    print_msg("Writing trace to constraints file: %s" % (filename))

    constr_topmod = topmod
    constr_state = "s@@step_idx@@"
    constr_prefix = ""

    if smtctop is not None:
        for item in smtctop[0].split("."):
            assert item in smt.modinfo[constr_topmod].cells
            constr_state = "(|%s_h %s| %s)" % (constr_topmod, item, constr_state)
            constr_topmod = smt.modinfo[constr_topmod].cells[item]
        if smtctop[1] != "":
            constr_prefix = smtctop[1] + "."

    if smtcinit:
        steps_start = steps_stop - 1

    with open(filename, "w") as f:
        primary_inputs = list()

        for name in smt.modinfo[constr_topmod].inputs:
            width = smt.modinfo[constr_topmod].wsize[name]
            primary_inputs.append((name, width))

        if steps_start == 0 or smtcinit:
            print("initial", file=f)
        else:
            print("state %d" % steps_start, file=f)

        regnames = sorted(smt.hiernets(constr_topmod, regs_only=True))
        regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start)))

        for name, val in zip(regnames, regvals):
            print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)

        mems = sorted(smt.hiermems(constr_topmod))
        for mempath in mems:
            abits, width, rports, wports, asyncwr = smt.mem_info(constr_topmod, mempath)

            addr_expr_list = list()
            data_expr_list = list()
            for i in range(steps_start, steps_stop):
                for j in range(rports):
                    addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
                    data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))

            addr_list = smt.get_list(addr_expr_list)
            data_list = smt.get_list(data_expr_list)

            addr_data = dict()
            for addr, data in zip(addr_list, data_list):
                if addr not in addr_data:
                    addr_data[addr] = data

            for addr, data in addr_data.items():
                print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f)

        for k in range(steps_start, steps_stop):
            if not smtcinit:
                print("", file=f)
                print("state %d" % k, file=f)

            pi_names = [[name] for name, _ in sorted(primary_inputs)]
            pi_values = smt.get_net_list(constr_topmod, pi_names, constr_state.replace("@@step_idx@@", str(k)))

            for name, val in zip(pi_names, pi_values):
                print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)


def write_trace(steps_start, steps_stop, index):
    if vcdfile is not None:
        write_vcd_trace(steps_start, steps_stop, index)

    if vlogtbfile is not None:
        write_vlogtb_trace(steps_start, steps_stop, index)

    if outconstr is not None:
        write_constr_trace(steps_start, steps_stop, index)


def print_failed_asserts_worker(mod, state, path, extrainfo):
    assert mod in smt.modinfo
    found_failed_assert = False

    if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
        return

    for cellname, celltype in smt.modinfo[mod].cells.items():
        if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
            found_failed_assert = True

    for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
        if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
            print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
            found_failed_assert = True

    return found_failed_assert


def print_failed_asserts(state, final=False, extrainfo=""):
    if noinfo: return
    loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
    found_failed_assert = False

    for loc, expr, value in zip(loc_list, expr_list, value_list):
        if smt.bv2int(value) == 0:
            print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
            found_failed_assert = True

    if not final:
        if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
            found_failed_assert = True

    return found_failed_assert


def print_anyconsts_worker(mod, state, path):
    assert mod in smt.modinfo

    for cellname, celltype in smt.modinfo[mod].cells.items():
        print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)

    for fun, info in smt.modinfo[mod].anyconsts.items():
        if info[1] is None:
            if not binarymode:
                print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
            else:
                print_msg("Value for anyconst in %s (%s): %s" % (path, info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))
        else:
            if not binarymode:
                print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
            else:
                print_msg("Value for anyconst %s.%s (%s): %s" % (path, info[1], info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))


def print_anyconsts(state):
    if noinfo: return
    print_anyconsts_worker(topmod, "s%d" % state, topmod)


def get_cover_list(mod, base):
    assert mod in smt.modinfo

    cover_expr = list()
    cover_desc = list()

    for expr, desc in smt.modinfo[mod].covers.items():
        cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
        cover_desc.append(desc)

    for cell, submod in smt.modinfo[mod].cells.items():
        e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
        cover_expr += e
        cover_desc += d

    return cover_expr, cover_desc

states = list()
asserts_antecedent_cache = [list()]
asserts_consequent_cache = [list()]
asserts_cache_dirty = False

def smt_state(step):
    smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
    states.append("s%d" % step)

def smt_assert(expr):
    if expr == "true":
        return

    smt.write("(assert %s)" % expr)

def smt_assert_antecedent(expr):
    if expr == "true":
        return

    smt.write("(assert %s)" % expr)

    global asserts_cache_dirty
    asserts_cache_dirty = True
    asserts_antecedent_cache[-1].append(expr)

def smt_assert_consequent(expr):
    if expr == "true":
        return

    smt.write("(assert %s)" % expr)

    global asserts_cache_dirty
    asserts_cache_dirty = True
    asserts_consequent_cache[-1].append(expr)

def smt_forall_assert():
    if not smt.forall:
        return

    global asserts_cache_dirty
    asserts_cache_dirty = False

    assert (len(smt.modinfo[topmod].maximize) + len(smt.modinfo[topmod].minimize) <= 1)

    def make_assert_expr(asserts_cache):
        expr = list()
        for lst in asserts_cache:
            expr += lst

        assert len(expr) != 0

        if len(expr) == 1:
            expr = expr[0]
        else:
            expr = "(and %s)" % (" ".join(expr))
        return expr

    antecedent_expr = make_assert_expr(asserts_antecedent_cache)
    consequent_expr = make_assert_expr(asserts_consequent_cache)

    states_db = set(states)
    used_states_db = set()
    new_antecedent_expr = list()
    new_consequent_expr = list()
    assert_expr = list()

    def make_new_expr(new_expr, expr):
        cursor = 0
        while cursor < len(expr):
            l = 1
            if expr[cursor] in '|"':
                while cursor+l+1 < len(expr) and expr[cursor] != expr[cursor+l]:
                    l += 1
                l += 1
            elif expr[cursor] not in '() ':
                while cursor+l < len(expr) and expr[cursor+l] not in '|"() ':
                    l += 1

            word = expr[cursor:cursor+l]
            if word in states_db:
                used_states_db.add(word)
                word += "_"

            new_expr.append(word)
            cursor += l

    make_new_expr(new_antecedent_expr, antecedent_expr)
    make_new_expr(new_consequent_expr, consequent_expr)

    new_antecedent_expr = ["".join(new_antecedent_expr)]
    new_consequent_expr = ["".join(new_consequent_expr)]

    if states[0] in used_states_db:
        new_antecedent_expr.append("(|%s_ex_state_eq| %s %s_)" % (topmod, states[0], states[0]))
    for s in states:
        if s in used_states_db:
            new_antecedent_expr.append("(|%s_ex_input_eq| %s %s_)" % (topmod, s, s))

    if len(new_antecedent_expr) == 0:
        new_antecedent_expr = "true"
    elif len(new_antecedent_expr) == 1:
        new_antecedent_expr = new_antecedent_expr[0]
    else:
        new_antecedent_expr = "(and %s)" % (" ".join(new_antecedent_expr))

    if len(new_consequent_expr) == 0:
        new_consequent_expr = "true"
    elif len(new_consequent_expr) == 1:
        new_consequent_expr = new_consequent_expr[0]
    else:
        new_consequent_expr = "(and %s)" % (" ".join(new_consequent_expr))

    assert_expr.append("(assert (forall (")
    first_state = True
    for s in states:
        if s in used_states_db:
            assert_expr.append("%s(%s_ |%s_s|)" % ("" if first_state else " ", s, topmod))
            first_state = False
    assert_expr.append(") (=> %s %s)))" % (new_antecedent_expr, new_consequent_expr))

    smt.write("".join(assert_expr))

    if len(smt.modinfo[topmod].maximize) > 0:
        for s in states:
            if s in used_states_db:
                smt.write("(maximize (|%s| %s))\n" % (smt.modinfo[topmod].maximize.copy().pop(), s))
                break

    if len(smt.modinfo[topmod].minimize) > 0:
        for s in states:
            if s in used_states_db:
                smt.write("(minimize (|%s| %s))\n" % (smt.modinfo[topmod].minimize.copy().pop(), s))
                break

def smt_push():
    global asserts_cache_dirty
    asserts_cache_dirty = True
    asserts_antecedent_cache.append(list())
    asserts_consequent_cache.append(list())
    smt.write("(push 1)")

def smt_pop():
    global asserts_cache_dirty
    asserts_cache_dirty = True
    asserts_antecedent_cache.pop()
    asserts_consequent_cache.pop()
    smt.write("(pop 1)")

def smt_check_sat(expected=["sat", "unsat"]):
    if asserts_cache_dirty:
        smt_forall_assert()
    return smt.check_sat(expected=expected)

if tempind:
    retstatus = "FAILED"
    skip_counter = step_size
    for step in range(num_steps, -1, -1):
        if smt.forall:
            print_msg("Temporal induction not supported for exists-forall problems.")
            break

        smt_state(step)
        smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
        smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
        smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
        smt_assert_consequent(get_constr_expr(constr_assumes, step))

        if step == num_steps:
            smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod, step, get_constr_expr(constr_asserts, step)))

        else:
            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step, step+1))
            smt_assert("(|%s_a| s%d)" % (topmod, step))
            smt_assert(get_constr_expr(constr_asserts, step))

        if step > num_steps-skip_steps:
            print_msg("Skipping induction in step %d.." % (step))
            continue

        skip_counter += 1
        if skip_counter < step_size:
            print_msg("Skipping induction in step %d.." % (step))
            continue

        skip_counter = 0
        print_msg("Trying induction in step %d.." % (step))

        if smt_check_sat() == "sat":
            if step == 0:
                print_msg("Temporal induction failed!")
                print_anyconsts(num_steps)
                print_failed_asserts(num_steps)
                write_trace(step, num_steps+1, '%')

            elif dumpall:
                print_anyconsts(num_steps)
                print_failed_asserts(num_steps)
                write_trace(step, num_steps+1, "%d" % step)

        else:
            print_msg("Temporal induction successful.")
            retstatus = "PASSED"
            break

elif covermode:
    cover_expr, cover_desc = get_cover_list(topmod, "state")
    cover_mask = "1" * len(cover_desc)

    if len(cover_expr) > 1:
        cover_expr = "(concat %s)" % " ".join(cover_expr)
    elif len(cover_expr) == 1:
        cover_expr = cover_expr[0]
    else:
        cover_expr = "#b0"

    coveridx = 0
    smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))

    step = 0
    retstatus = "FAILED"
    found_failed_assert = False

    assert step_size == 1

    while step < num_steps:
        smt_state(step)
        smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
        smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
        smt_assert_consequent(get_constr_expr(constr_assumes, step))

        if step == 0:
            if noinit:
                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
            else:
                smt_assert_antecedent("(|%s_i| s0)" % (topmod))
                smt_assert_antecedent("(|%s_is| s0)" % (topmod))

        else:
            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
            smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))

        while "1" in cover_mask:
            print_msg("Checking cover reachability in step %d.." % (step))
            smt_push()
            smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc)))

            if smt_check_sat() == "unsat":
                smt_pop()
                break

            if append_steps > 0:
                for i in range(step+1, step+1+append_steps):
                    print_msg("Appending additional step %d." % i)
                    smt_state(i)
                    smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
                    smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
                    smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
                    smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
                    smt_assert_consequent(get_constr_expr(constr_assumes, i))
                print_msg("Re-solving with appended steps..")
                if smt_check_sat() == "unsat":
                    print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
                    found_failed_assert = True
                    retstatus = "FAILED"
                    break

            reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
            assert len(reached_covers) == len(cover_desc)

            new_cover_mask = []

            for i in range(len(reached_covers)):
                if reached_covers[i] == "0":
                    new_cover_mask.append(cover_mask[i])
                    continue

                print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
                new_cover_mask.append("0")

            cover_mask = "".join(new_cover_mask)

            for i in range(step+1+append_steps):
                if print_failed_asserts(i, extrainfo=" (step %d)" % i):
                    found_failed_assert = True

            write_trace(0, step+1+append_steps, "%d" % coveridx)

            if found_failed_assert:
                break

            coveridx += 1
            smt_pop()
            smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))

        if found_failed_assert:
            break

        if "1" not in cover_mask:
            retstatus = "PASSED"
            break

        step += 1

    if "1" in cover_mask:
        for i in range(len(cover_mask)):
            if cover_mask[i] == "1":
                print_msg("Unreached cover statement at %s." % cover_desc[i])

else:  # not tempind, covermode
    step = 0
    retstatus = "PASSED"
    while step < num_steps:
        smt_state(step)
        smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
        smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
        smt_assert_consequent(get_constr_expr(constr_assumes, step))

        if step == 0:
            if noinit:
                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
            else:
                smt_assert_antecedent("(|%s_i| s0)" % (topmod))
                smt_assert_antecedent("(|%s_is| s0)" % (topmod))

        else:
            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
            smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))

        if step < skip_steps:
            if assume_skipped is not None and step >= assume_skipped:
                print_msg("Skipping step %d (and assuming pass).." % (step))
                smt_assert("(|%s_a| s%d)" % (topmod, step))
                smt_assert(get_constr_expr(constr_asserts, step))
            else:
                print_msg("Skipping step %d.." % (step))
            step += 1
            continue

        last_check_step = step
        for i in range(1, step_size):
            if step+i < num_steps:
                smt_state(step+i)
                smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i))
                smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i))
                smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i))
                smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i))
                smt_assert_consequent(get_constr_expr(constr_assumes, step+i))
                last_check_step = step+i

        if not gentrace:
            if presat:
                if last_check_step == step:
                    print_msg("Checking assumptions in step %d.." % (step))
                else:
                    print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))

                if smt_check_sat() == "unsat":
                    print("%s Assumptions are unsatisfiable!" % smt.timestamp())
                    retstatus = "PREUNSAT"
                    break

            if not final_only:
                if last_check_step == step:
                    print_msg("Checking assertions in step %d.." % (step))
                else:
                    print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
                smt_push()

                smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
                        [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))

                if smt_check_sat() == "sat":
                    print("%s BMC failed!" % smt.timestamp())
                    if append_steps > 0:
                        for i in range(last_check_step+1, last_check_step+1+append_steps):
                            print_msg("Appending additional step %d." % i)
                            smt_state(i)
                            smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
                            smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
                            smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
                            smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
                            smt_assert_consequent(get_constr_expr(constr_assumes, i))
                        print_msg("Re-solving with appended steps..")
                        if smt_check_sat() == "unsat":
                            print("%s Cannot append steps without violating assumptions!" % smt.timestamp())
                            retstatus = "FAILED"
                            break
                    print_anyconsts(step)
                    for i in range(step, last_check_step+1):
                        print_failed_asserts(i)
                    write_trace(0, last_check_step+1+append_steps, '%')
                    retstatus = "FAILED"
                    break

                smt_pop()

            if (constr_final_start is not None) or (last_check_step+1 != num_steps):
                for i in range(step, last_check_step+1):
                    smt_assert("(|%s_a| s%d)" % (topmod, i))
                    smt_assert(get_constr_expr(constr_asserts, i))

            if constr_final_start is not None:
                for i in range(step, last_check_step+1):
                    if i < constr_final_start:
                        continue

                    print_msg("Checking final constraints in step %d.." % (i))
                    smt_push()

                    smt_assert_consequent(get_constr_expr(constr_assumes, i, final=True))
                    smt_assert("(not %s)" % get_constr_expr(constr_asserts, i, final=True))

                    if smt_check_sat() == "sat":
                        print("%s BMC failed!" % smt.timestamp())
                        print_anyconsts(i)
                        print_failed_asserts(i, final=True)
                        write_trace(0, i+1, '%')
                        retstatus = "FAILED"
                        break

                    smt_pop()
                if retstatus == "FAILED" or retstatus == "PREUNSAT":
                    break

        else:  # gentrace
            for i in range(step, last_check_step+1):
                smt_assert("(|%s_a| s%d)" % (topmod, i))
                smt_assert(get_constr_expr(constr_asserts, i))

            print_msg("Solving for step %d.." % (last_check_step))
            status = smt_check_sat()
            if status != "sat":
                print("%s No solution found! (%s)" % (smt.timestamp(), status))
                retstatus = "FAILED"
                break

            elif dumpall:
                print_anyconsts(0)
                write_trace(0, last_check_step+1, "%d" % step)

        step += step_size

    if gentrace and retstatus == "PASSED":
        print_anyconsts(0)
        write_trace(0, num_steps, '%')


smt.write("(exit)")
smt.wait()

print_msg("Status: %s" % retstatus)
sys.exit(0 if retstatus == "PASSED" else 1)