Verilator

1
// -*- mode: C++; c-file-style: "cc-mode" -*-
2
//*************************************************************************
3
//
4
// Code available from: https://verilator.org
5
//
6
// Copyright 2024 by Wilson Snyder.  This program is free software; you can
7
// redistribute it and/or modify it under the terms of either the GNU Lesser
8
// General Public License Version 3 or the Perl Artistic License Version 2.0.
9
// SPDX-License-Identifier: LGPL-3.0-only OR Artistic-2.0
10
//
11
//=========================================================================
12
///
13
/// \file
14
/// \brief Verilated randomization implementation code
15
///
16
/// This file must be compiled and linked against all Verilated objects
17
/// that use randomization features.
18
///
19
/// See the internals documentation docs/internals.rst for details.
20
///
21
//=========================================================================
22

23
#include "verilated_random.h"
24

25
#include <iostream>
26
#include <sstream>
27
#include <streambuf>
28

29
#define _VL_SOLVER_HASH_LEN 1
30
#define _VL_SOLVER_HASH_LEN_TOTAL 4
31

32
// clang-format off
33
#if defined(__unix__) || defined(__unix) || (defined(__APPLE__) && defined(__MACH__))
34
# define _VL_SOLVER_PIPE  // Allow pipe SMT solving.  Needs fork()
35
#endif
36

37
#ifdef _VL_SOLVER_PIPE
38
# include <sys/wait.h>
39
# include <fcntl.h>
40
#endif
41

42
#if defined(_WIN32) || defined(__MINGW32__)
43
# include <io.h>  // open, read, write, close
44
#endif
45
// clang-format on
46

47
class Process final : private std::streambuf, public std::iostream {
48
    static constexpr int BUFFER_SIZE = 4096;
49
    const char* const* m_cmd = nullptr;  // fork() process argv
50
#ifdef _VL_SOLVER_PIPE
51
    pid_t m_pid = 0;  // fork() process id
52
#else
53
    int m_pid = 0;  // fork() process id - always zero as disabled
54
#endif
55
    bool m_pidExited = true;  // If subprocess has exited and can be opened
56
    int m_pidStatus = 0;  // fork() process exit status, valid if m_pidExited
57
    int m_writeFd = -1;  // File descriptor TO subprocess
58
    int m_readFd = -1;  // File descriptor FROM subprocess
59
    char m_readBuf[BUFFER_SIZE];
60
    char m_writeBuf[BUFFER_SIZE];
61

62
public:
63
    typedef std::streambuf::traits_type traits_type;
64

65
protected:
66
    int overflow(int c = traits_type::eof()) override {
67
        char c2 = static_cast<char>(c);
68
        if (pbase() == pptr()) return 0;
69
        size_t size = pptr() - pbase();
70
        ssize_t n = ::write(m_writeFd, pbase(), size);
71
        if (n == -1) perror("write");
72
        if (n <= 0) {
73
            wait_report();
74
            return traits_type::eof();
75
        }
76
        if (n == size)
77
            setp(m_writeBuf, m_writeBuf + sizeof(m_writeBuf));
78
        else
79
            setp(m_writeBuf + n, m_writeBuf + sizeof(m_writeBuf));
80
        if (c != traits_type::eof()) sputc(c2);
81
        return 0;
82
    }
83
    int underflow() override {
84
        sync();
85
        ssize_t n = ::read(m_readFd, m_readBuf, sizeof(m_readBuf));
86
        if (n == -1) perror("read");
87
        if (n <= 0) {
88
            wait_report();
89
            return traits_type::eof();
90
        }
91
        setg(m_readBuf, m_readBuf, m_readBuf + n);
92
        return traits_type::to_int_type(m_readBuf[0]);
93
    }
94
    int sync() override {
95
        overflow();
96
        return 0;
97
    }
98

99
public:
100
    explicit Process(const char* const* const cmd = nullptr)
101
        : std::streambuf{}
102
        , std::iostream{this}
103
        , m_cmd{cmd} {
104
        open(cmd);
105
    }
106

107
    void wait_report() {
108
        if (m_pidExited) return;
109
#ifdef _VL_SOLVER_PIPE
110
        if (waitpid(m_pid, &m_pidStatus, 0) != m_pid) return;
111
        if (m_pidStatus) {
112
            std::stringstream msg;
113
            msg << "Subprocess command `" << m_cmd[0];
114
            for (const char* const* arg = m_cmd + 1; *arg; arg++) msg << ' ' << *arg;
115
            msg << "' failed: ";
116
            if (WIFSIGNALED(m_pidStatus))
117
                msg << strsignal(WTERMSIG(m_pidStatus))
118
                    << (WCOREDUMP(m_pidStatus) ? " (core dumped)" : "");
119
            else if (WIFEXITED(m_pidStatus))
120
                msg << "exit status " << WEXITSTATUS(m_pidStatus);
121
            const std::string str = msg.str();
122
            VL_WARN_MT("", 0, "Process", str.c_str());
123
        }
124
#endif
125
        m_pidExited = true;
126
        m_pid = 0;
127
        closeFds();
128
    }
129

130
    void closeFds() {
131
        if (m_writeFd != -1) {
132
            close(m_writeFd);
133
            m_writeFd = -1;
134
        }
135
        if (m_readFd != -1) {
136
            close(m_readFd);
137
            m_readFd = -1;
138
        }
139
    }
140

141
    bool open(const char* const* const cmd) {
142
        setp(std::begin(m_writeBuf), std::end(m_writeBuf));
143
        setg(m_readBuf, m_readBuf, m_readBuf);
144
#ifdef _VL_SOLVER_PIPE
145
        if (!cmd || !cmd[0]) return false;
146
        m_cmd = cmd;
147
        int fd_stdin[2];  // Can't use std::array
148
        int fd_stdout[2];  // Can't use std::array
149
        constexpr int P_RD = 0;
150
        constexpr int P_WR = 1;
151

152
        if (pipe(fd_stdin) != 0) {
153
            perror("Process::open: pipe");
154
            return false;
155
        }
156
        if (pipe(fd_stdout) != 0) {
157
            perror("Process::open: pipe");
158
            close(fd_stdin[P_RD]);
159
            close(fd_stdin[P_WR]);
160
            return false;
161
        }
162

163
        if (fd_stdin[P_RD] <= 2 || fd_stdin[P_WR] <= 2 || fd_stdout[P_RD] <= 2
164
            || fd_stdout[P_WR] <= 2) {
165
            // We'd have to rearrange all of the FD usages in this case.
166
            // Too unlikely; verilator isn't a daemon.
167
            fprintf(stderr, "stdin/stdout closed before pipe opened\n");
168
            close(fd_stdin[P_RD]);
169
            close(fd_stdin[P_WR]);
170
            close(fd_stdout[P_RD]);
171
            close(fd_stdout[P_WR]);
172
            return false;
173
        }
174

175
        const pid_t pid = fork();
176
        if (pid < 0) {
177
            perror("Process::open: fork");
178
            close(fd_stdin[P_RD]);
179
            close(fd_stdin[P_WR]);
180
            close(fd_stdout[P_RD]);
181
            close(fd_stdout[P_WR]);
182
            return false;
183
        }
184
        if (pid == 0) {
185
            // Child
186
            close(fd_stdin[P_WR]);
187
            dup2(fd_stdin[P_RD], STDIN_FILENO);
188
            close(fd_stdout[P_RD]);
189
            dup2(fd_stdout[P_WR], STDOUT_FILENO);
190
            execvp(cmd[0], const_cast<char* const*>(cmd));
191
            std::stringstream msg;
192
            msg << "Process::open: execvp(" << cmd[0] << ")";
193
            const std::string str = msg.str();
194
            perror(str.c_str());
195
            _exit(127);
196
        }
197
        // Parent
198
        m_pid = pid;
199
        m_pidExited = false;
200
        m_pidStatus = 0;
201
        m_readFd = fd_stdout[P_RD];
202
        m_writeFd = fd_stdin[P_WR];
203

204
        close(fd_stdin[P_RD]);
205
        close(fd_stdout[P_WR]);
206

207
        return true;
208
#else
209
        return false;
210
#endif
211
    }
212
};
213

214
static Process& getSolver() {
215
    static Process s_solver;
216
    static bool s_done = false;
217
    if (s_done) return s_solver;
218
    s_done = true;
219

220
    static std::vector<const char*> s_argv;
221
    static std::string s_program = Verilated::threadContextp()->solverProgram();
222
    s_argv.emplace_back(&s_program[0]);
223
    for (char* arg = &s_program[0]; *arg; arg++) {
224
        if (*arg == ' ') {
225
            *arg = '\0';
226
            s_argv.emplace_back(arg + 1);
227
        }
228
    }
229
    s_argv.emplace_back(nullptr);
230

231
    const char* const* const cmd = &s_argv[0];
232
    s_solver.open(cmd);
233
    s_solver << "(set-logic QF_BV)\n";
234
    s_solver << "(check-sat)\n";
235
    s_solver << "(reset)\n";
236
    std::string s;
237
    getline(s_solver, s);
238
    if (s == "sat") return s_solver;
239

240
    std::stringstream msg;
241
    msg << "Unable to communicate with SAT solver, please check its installation or specify a "
242
           "different one in VERILATOR_SOLVER environment variable.\n";
243
    msg << " ... Tried: $";
244
    for (const char* const* arg = cmd; *arg; arg++) msg << ' ' << *arg;
245
    msg << '\n';
246
    const std::string str = msg.str();
247
    VL_WARN_MT("", 0, "randomize", str.c_str());
248

249
    while (getline(s_solver, s)) {}
250
    return s_solver;
251
}
252

253
//======================================================================
254
// VlRandomizer:: Methods
255

256
void VlRandomVar::emit(std::ostream& s) const { s << m_name; }
257
void VlRandomConst::emit(std::ostream& s) const {
258
    s << "#b";
259
    for (int i = 0; i < m_width; i++) s << (VL_BITISSET_Q(m_val, m_width - i - 1) ? '1' : '0');
260
}
261
void VlRandomBinOp::emit(std::ostream& s) const {
262
    s << '(' << m_op << ' ';
263
    m_lhs->emit(s);
264
    s << ' ';
265
    m_rhs->emit(s);
266
    s << ')';
267
}
268
void VlRandomExtract::emit(std::ostream& s) const {
269
    s << "((_ extract " << m_idx << ' ' << m_idx << ") ";
270
    m_expr->emit(s);
271
    s << ')';
272
}
273
bool VlRandomVar::set(std::string&& val) const {
274
    VlWide<VL_WQ_WORDS_E> qowp;
275
    VL_SET_WQ(qowp, 0ULL);
276
    WDataOutP owp = qowp;
277
    int obits = width();
278
    if (obits > VL_QUADSIZE) owp = reinterpret_cast<WDataOutP>(datap());
279
    int i;
280
    for (i = 0; val[i] && val[i] != '#'; i++) {}
281
    if (val[i++] != '#') return false;
282
    switch (val[i++]) {
283
    case 'b': _vl_vsss_based(owp, obits, 1, &val[i], 0, val.size() - i); break;
284
    case 'o': _vl_vsss_based(owp, obits, 3, &val[i], 0, val.size() - i); break;
285
    case 'h':  // FALLTHRU
286
    case 'x': _vl_vsss_based(owp, obits, 4, &val[i], 0, val.size() - i); break;
287
    default:
288
        VL_WARN_MT(__FILE__, __LINE__, "randomize",
289
                   "Internal: Unable to parse solver's randomized number");
290
        return false;
291
    }
292
    if (obits <= VL_BYTESIZE) {
293
        CData* const p = static_cast<CData*>(datap());
294
        *p = VL_CLEAN_II(obits, obits, owp[0]);
295
    } else if (obits <= VL_SHORTSIZE) {
296
        SData* const p = static_cast<SData*>(datap());
297
        *p = VL_CLEAN_II(obits, obits, owp[0]);
298
    } else if (obits <= VL_IDATASIZE) {
299
        IData* const p = static_cast<IData*>(datap());
300
        *p = VL_CLEAN_II(obits, obits, owp[0]);
301
    } else if (obits <= VL_QUADSIZE) {
302
        QData* const p = static_cast<QData*>(datap());
303
        *p = VL_CLEAN_QQ(obits, obits, VL_SET_QW(owp));
304
    } else {
305
        _vl_clean_inplace_w(obits, owp);
306
    }
307
    return true;
308
}
309

310
std::shared_ptr<const VlRandomExpr> VlRandomizer::randomConstraint(VlRNG& rngr, int bits) {
311
    unsigned long long hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1);
312
    std::shared_ptr<const VlRandomExpr> concat = nullptr;
313
    std::vector<std::shared_ptr<const VlRandomExpr>> varbits;
314
    for (const auto& var : m_vars) {
315
        for (int i = 0; i < var.second->width(); i++)
316
            varbits.emplace_back(std::make_shared<const VlRandomExtract>(var.second, i));
317
    }
318
    for (int i = 0; i < bits; i++) {
319
        std::shared_ptr<const VlRandomExpr> bit = nullptr;
320
        for (unsigned j = 0; j * 2 < varbits.size(); j++) {
321
            unsigned idx = j + VL_RANDOM_RNG_I(rngr) % (varbits.size() - j);
322
            auto sel = varbits[idx];
323
            std::swap(varbits[idx], varbits[j]);
324
            bit = bit == nullptr ? sel : std::make_shared<const VlRandomBinOp>("bvxor", bit, sel);
325
        }
326
        concat = concat == nullptr ? bit
327
                                   : std::make_shared<const VlRandomBinOp>("concat", concat, bit);
328
    }
329
    return std::make_shared<const VlRandomBinOp>(
330
        "=", concat, std::make_shared<const VlRandomConst>(hash, bits));
331
}
332

333
bool VlRandomizer::next(VlRNG& rngr) {
334
    if (m_vars.empty()) return true;
335
    std::iostream& f = getSolver();
336
    if (!f) return false;
337

338
    f << "(set-option :produce-models true)\n";
339
    f << "(set-logic QF_BV)\n";
340
    for (const auto& var : m_vars) {
341
        f << "(declare-fun " << var.second->name() << " () (_ BitVec " << var.second->width()
342
          << "))\n";
343
    }
344
    for (const std::string& constraint : m_constraints) { f << "(assert " << constraint << ")\n"; }
345
    f << "(check-sat)\n";
346

347
    bool sat = parseSolution(f);
348
    if (!sat) {
349
        f << "(reset)\n";
350
        return false;
351
    }
352

353
    for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; i++) {
354
        f << "(assert ";
355
        randomConstraint(rngr, _VL_SOLVER_HASH_LEN)->emit(f);
356
        f << ")\n";
357
        f << "\n(check-sat)\n";
358
        sat = parseSolution(f);
359
    }
360

361
    f << "(reset)\n";
362
    return true;
363
}
364

365
bool VlRandomizer::parseSolution(std::iostream& f) {
366
    std::string sat;
367
    do { std::getline(f, sat); } while (sat == "");
368

369
    if (sat == "unsat") return false;
370
    if (sat != "sat") {
371
        std::stringstream msg;
372
        msg << "Internal: Solver error: " << sat;
373
        const std::string str = msg.str();
374
        VL_WARN_MT(__FILE__, __LINE__, "randomize", str.c_str());
375
        return false;
376
    }
377

378
    f << "(get-value (";
379
    for (const auto& var : m_vars) f << var.second->name() << ' ';
380
    f << "))\n";
381

382
    // Quasi-parse S-expression of the form ((x #xVALUE) (y #bVALUE) (z #xVALUE))
383
    char c;
384
    f >> c;
385
    if (c != '(') {
386
        VL_WARN_MT(__FILE__, __LINE__, "randomize",
387
                   "Internal: Unable to parse solver's response: invalid S-expression");
388
        return false;
389
    }
390

391
    while (true) {
392
        f >> c;
393
        if (c == ')') break;
394
        if (c != '(') {
395
            VL_WARN_MT(__FILE__, __LINE__, "randomize",
396
                       "Internal: Unable to parse solver's response: invalid S-expression");
397
            return false;
398
        }
399

400
        std::string name, value;
401
        f >> name;
402
        std::getline(f, value, ')');
403

404
        auto it = m_vars.find(name);
405
        if (it == m_vars.end()) continue;
406

407
        it->second->set(std::move(value));
408
    }
409

410
    return true;
411
}
412

413
void VlRandomizer::hard(std::string&& constraint) {
414
    m_constraints.emplace_back(std::move(constraint));
415
}
416

417
#ifdef VL_DEBUG
418
void VlRandomizer::dump() const {
419
    for (const auto& var : m_vars) {
420
        VL_PRINTF("Variable (%d): %s\n", var.second->width(), var.second->name());
421
    }
422
    for (const std::string& c : m_constraints) VL_PRINTF("Constraint: %s\n", c.c_str());
423
}
424
#endif
425