SatPass Struct Reference

Inheritance diagram for SatPass:

Collaboration diagram for SatPass:

Public Member Functions
	SatPass ()
virtual void	help ()
virtual void	execute (std::vector< std::string > args, RTLIL::Design *design)
pre_post_exec_state_t	pre_execute ()
void	post_execute (pre_post_exec_state_t state)
void	cmd_log_args (const std::vector< std::string > &args)
void	cmd_error (const std::vector< std::string > &args, size_t argidx, std::string msg)
void	extra_args (std::vector< std::string > args, size_t argidx, RTLIL::Design *design, bool select=true)
virtual void	run_register ()

Static Public Member Functions
static void	call (RTLIL::Design *design, std::string command)
static void	call (RTLIL::Design *design, std::vector< std::string > args)
static void	call_on_selection (RTLIL::Design *design, const RTLIL::Selection &selection, std::string command)
static void	call_on_selection (RTLIL::Design *design, const RTLIL::Selection &selection, std::vector< std::string > args)
static void	call_on_module (RTLIL::Design *design, RTLIL::Module *module, std::string command)
static void	call_on_module (RTLIL::Design *design, RTLIL::Module *module, std::vector< std::string > args)
static void	init_register ()
static void	done_register ()

Data Fields
std::string	pass_name
std::string	short_help
int	call_counter
int64_t	runtime_ns
Pass *	next_queued_pass

Detailed Description

Definition at line 808 of file sat.cc.

Constructor & Destructor Documentation

SatPass::SatPass ( )

inline

Definition at line 809 of file sat.cc.

: Pass("sat", "solve a SAT problem in the circuit") { }

Member Function Documentation

void Pass::call ( RTLIL::Design *  design, std::string  command  )

staticinherited

Definition at line 146 of file register.cc.

{
    std::vector<std::string> args;

    std::string cmd_buf = command;
    std::string tok = next_token(cmd_buf, " \t\r\n");

    if (tok.empty() || tok[0] == '#')
        return;

    if (tok[0] == '!') {
        cmd_buf = command.substr(command.find('!') + 1);
        while (!cmd_buf.empty() && (cmd_buf.back() == ' ' || cmd_buf.back() == '\t' ||
                cmd_buf.back() == '\r' || cmd_buf.back() == '\n'))
            cmd_buf.resize(cmd_buf.size()-1);
        log_header("Shell command: %s\n", cmd_buf.c_str());
        int retCode = run_command(cmd_buf);
        if (retCode != 0)
            log_cmd_error("Shell command returned error code %d.\n", retCode);
        return;
    }

    while (!tok.empty()) {
        if (tok == "#")
            break;
        if (tok.back() == ';') {
            int num_semikolon = 0;
            while (!tok.empty() && tok.back() == ';')
                tok.resize(tok.size()-1), num_semikolon++;
            if (!tok.empty())
                args.push_back(tok);
            call(design, args);
            args.clear();
            if (num_semikolon == 2)
                call(design, "clean");
            if (num_semikolon == 3)
                call(design, "clean -purge");
        } else
            args.push_back(tok);
        tok = next_token(cmd_buf, " \t\r\n");
    }

    call(design, args);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Pass::call ( RTLIL::Design *  design, std::vector< std::string >  args  )

staticinherited

Definition at line 191 of file register.cc.

{
    if (args.size() == 0 || args[0][0] == '#')
        return;

    if (echo_mode) {
        log("%s", create_prompt(design, 0));
        for (size_t i = 0; i < args.size(); i++)
            log("%s%s", i ? " " : "", args[i].c_str());
        log("\n");
    }

    if (pass_register.count(args[0]) == 0)
        log_cmd_error("No such command: %s (type 'help' for a command overview)\n", args[0].c_str());

    size_t orig_sel_stack_pos = design->selection_stack.size();
    auto state = pass_register[args[0]]->pre_execute();
    pass_register[args[0]]->execute(args, design);
    pass_register[args[0]]->post_execute(state);
    while (design->selection_stack.size() > orig_sel_stack_pos)
        design->selection_stack.pop_back();

    design->check();
}

Here is the call graph for this function:

void Pass::call_on_module ( RTLIL::Design *  design, RTLIL::Module *  module, std::string  command  )

staticinherited

Definition at line 240 of file register.cc.

{
    std::string backup_selected_active_module = design->selected_active_module;
    design->selected_active_module = module->name.str();
    design->selection_stack.push_back(RTLIL::Selection(false));
    design->selection_stack.back().select(module);

    Pass::call(design, command);

    design->selection_stack.pop_back();
    design->selected_active_module = backup_selected_active_module;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Pass::call_on_module ( RTLIL::Design *  design, RTLIL::Module *  module, std::vector< std::string >  args  )

staticinherited

Definition at line 253 of file register.cc.

{
    std::string backup_selected_active_module = design->selected_active_module;
    design->selected_active_module = module->name.str();
    design->selection_stack.push_back(RTLIL::Selection(false));
    design->selection_stack.back().select(module);

    Pass::call(design, args);

    design->selection_stack.pop_back();
    design->selected_active_module = backup_selected_active_module;
}

Here is the call graph for this function:

void Pass::call_on_selection ( RTLIL::Design *  design, const RTLIL::Selection &  selection, std::string  command  )

staticinherited

Definition at line 216 of file register.cc.

{
    std::string backup_selected_active_module = design->selected_active_module;
    design->selected_active_module.clear();
    design->selection_stack.push_back(selection);

    Pass::call(design, command);

    design->selection_stack.pop_back();
    design->selected_active_module = backup_selected_active_module;
}

Here is the call graph for this function:

void Pass::call_on_selection ( RTLIL::Design *  design, const RTLIL::Selection &  selection, std::vector< std::string >  args  )

staticinherited

Definition at line 228 of file register.cc.

{
    std::string backup_selected_active_module = design->selected_active_module;
    design->selected_active_module.clear();
    design->selection_stack.push_back(selection);

    Pass::call(design, args);

    design->selection_stack.pop_back();
    design->selected_active_module = backup_selected_active_module;
}

Here is the call graph for this function:

void Pass::cmd_error ( const std::vector< std::string > &  args, size_t  argidx, std::string  msg  )

inherited

Definition at line 110 of file register.cc.

{
    std::string command_text;
    int error_pos = 0;

    for (size_t i = 0; i < args.size(); i++) {
        if (i < argidx)
            error_pos += args[i].size() + 1;
        command_text = command_text + (command_text.empty() ? "" : " ") + args[i];
    }

    log("\nSyntax error in command `%s':\n", command_text.c_str());
    help();

    log_cmd_error("Command syntax error: %s\n> %s\n> %*s^\n",
            msg.c_str(), command_text.c_str(), error_pos, "");
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Pass::cmd_log_args ( const std::vector< std::string > &  args )

inherited

Definition at line 100 of file register.cc.

{
    if (args.size() <= 1)
        return;
    log("Full command line:");
    for (size_t i = 0; i < args.size(); i++)
        log(" %s", args[i].c_str());
    log("\n");
}

Here is the call graph for this function:

void Pass::done_register ( )

staticinherited

Definition at line 62 of file register.cc.

{
    frontend_register.clear();
    pass_register.clear();
    backend_register.clear();
    log_assert(first_queued_pass == NULL);
}

Here is the caller graph for this function:

virtual void SatPass::execute ( std::vector< std::string >  args, RTLIL::Design *  design  )

inlinevirtual

Implements Pass.

Definition at line 944 of file sat.cc.

    {
        std::vector<std::pair<std::string, std::string>> sets, sets_init, prove, prove_x;
        std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
        std::map<int, std::vector<std::string>> unsets_at, sets_def_at, sets_any_undef_at, sets_all_undef_at;
        std::vector<std::string> shows, sets_def, sets_any_undef, sets_all_undef;
        int loopcount = 0, seq_len = 0, maxsteps = 0, initsteps = 0, timeout = 0, prove_skip = 0;
        bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
        bool ignore_div_by_zero = false, set_init_undef = false, set_init_zero = false, max_undef = false;
        bool tempinduct = false, prove_asserts = false, show_inputs = false, show_outputs = false;
        bool ignore_unknown_cells = false, falsify = false, tempinduct_def = false, set_init_def = false;
        std::string vcd_file_name, cnf_file_name;

        log_header("Executing SAT pass (solving SAT problems in the circuit).\n");

        size_t argidx;
        for (argidx = 1; argidx < args.size(); argidx++) {
            if (args[argidx] == "-all") {
                loopcount = -1;
                continue;
            }
            if (args[argidx] == "-verify") {
                fail_on_timeout = true;
                verify = true;
                continue;
            }
            if (args[argidx] == "-verify-no-timeout") {
                verify = true;
                continue;
            }
            if (args[argidx] == "-falsify") {
                fail_on_timeout = true;
                falsify = true;
                continue;
            }
            if (args[argidx] == "-falsify-no-timeout") {
                falsify = true;
                continue;
            }
            if (args[argidx] == "-timeout" && argidx+1 < args.size()) {
                timeout = atoi(args[++argidx].c_str());
                continue;
            }
            if (args[argidx] == "-max" && argidx+1 < args.size()) {
                loopcount = atoi(args[++argidx].c_str());
                continue;
            }
            if (args[argidx] == "-maxsteps" && argidx+1 < args.size()) {
                maxsteps = atoi(args[++argidx].c_str());
                continue;
            }
            if (args[argidx] == "-initsteps" && argidx+1 < args.size()) {
                initsteps = atoi(args[++argidx].c_str());
                continue;
            }
            if (args[argidx] == "-ignore_div_by_zero") {
                ignore_div_by_zero = true;
                continue;
            }
            if (args[argidx] == "-enable_undef") {
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-max_undef") {
                enable_undef = true;
                max_undef = true;
                continue;
            }
            if (args[argidx] == "-set-def-inputs") {
                enable_undef = true;
                set_def_inputs = true;
                continue;
            }
            if (args[argidx] == "-set" && argidx+2 < args.size()) {
                std::string lhs = args[++argidx];
                std::string rhs = args[++argidx];
                sets.push_back(std::pair<std::string, std::string>(lhs, rhs));
                continue;
            }
            if (args[argidx] == "-set-def" && argidx+1 < args.size()) {
                sets_def.push_back(args[++argidx]);
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-set-any-undef" && argidx+1 < args.size()) {
                sets_any_undef.push_back(args[++argidx]);
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-set-all-undef" && argidx+1 < args.size()) {
                sets_all_undef.push_back(args[++argidx]);
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-tempinduct") {
                tempinduct = true;
                continue;
            }
            if (args[argidx] == "-tempinduct-def") {
                tempinduct = true;
                tempinduct_def = true;
                continue;
            }
            if (args[argidx] == "-prove" && argidx+2 < args.size()) {
                std::string lhs = args[++argidx];
                std::string rhs = args[++argidx];
                prove.push_back(std::pair<std::string, std::string>(lhs, rhs));
                continue;
            }
            if (args[argidx] == "-prove-x" && argidx+2 < args.size()) {
                std::string lhs = args[++argidx];
                std::string rhs = args[++argidx];
                prove_x.push_back(std::pair<std::string, std::string>(lhs, rhs));
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-prove-asserts") {
                prove_asserts = true;
                continue;
            }
            if (args[argidx] == "-prove-skip" && argidx+1 < args.size()) {
                prove_skip = atoi(args[++argidx].c_str());
                continue;
            }
            if (args[argidx] == "-seq" && argidx+1 < args.size()) {
                seq_len = atoi(args[++argidx].c_str());
                continue;
            }
            if (args[argidx] == "-set-at" && argidx+3 < args.size()) {
                int timestep = atoi(args[++argidx].c_str());
                std::string lhs = args[++argidx];
                std::string rhs = args[++argidx];
                sets_at[timestep].push_back(std::pair<std::string, std::string>(lhs, rhs));
                continue;
            }
            if (args[argidx] == "-unset-at" && argidx+2 < args.size()) {
                int timestep = atoi(args[++argidx].c_str());
                unsets_at[timestep].push_back(args[++argidx]);
                continue;
            }
            if (args[argidx] == "-set-def-at" && argidx+2 < args.size()) {
                int timestep = atoi(args[++argidx].c_str());
                sets_def_at[timestep].push_back(args[++argidx]);
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-set-any-undef-at" && argidx+2 < args.size()) {
                int timestep = atoi(args[++argidx].c_str());
                sets_any_undef_at[timestep].push_back(args[++argidx]);
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-set-all-undef-at" && argidx+2 < args.size()) {
                int timestep = atoi(args[++argidx].c_str());
                sets_all_undef_at[timestep].push_back(args[++argidx]);
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-set-init" && argidx+2 < args.size()) {
                std::string lhs = args[++argidx];
                std::string rhs = args[++argidx];
                sets_init.push_back(std::pair<std::string, std::string>(lhs, rhs));
                continue;
            }
            if (args[argidx] == "-set-init-undef") {
                set_init_undef = true;
                enable_undef = true;
                continue;
            }
            if (args[argidx] == "-set-init-def") {
                set_init_def = true;
                continue;
            }
            if (args[argidx] == "-set-init-zero") {
                set_init_zero = true;
                continue;
            }
            if (args[argidx] == "-show" && argidx+1 < args.size()) {
                shows.push_back(args[++argidx]);
                continue;
            }
            if (args[argidx] == "-show-inputs") {
                show_inputs = true;
                continue;
            }
            if (args[argidx] == "-show-outputs") {
                show_outputs = true;
                continue;
            }
            if (args[argidx] == "-ignore_unknown_cells") {
                ignore_unknown_cells = true;
                continue;
            }
            if (args[argidx] == "-dump_vcd" && argidx+1 < args.size()) {
                vcd_file_name = args[++argidx];
                continue;
            }
            if (args[argidx] == "-dump_cnf" && argidx+1 < args.size()) {
                cnf_file_name = args[++argidx];
                continue;
            }
            break;
        }
        extra_args(args, argidx, design);

        RTLIL::Module *module = NULL;
        for (auto &mod_it : design->modules_)
            if (design->selected(mod_it.second)) {
                if (module)
                    log_cmd_error("Only one module must be selected for the SAT pass! (selected: %s and %s)\n",
                            RTLIL::id2cstr(module->name), RTLIL::id2cstr(mod_it.first));
                module = mod_it.second;
            }
        if (module == NULL) 
            log_cmd_error("Can't perform SAT on an empty selection!\n");

        if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
            log_cmd_error("Got -tempinduct but nothing to prove!\n");

        if (prove_skip && tempinduct)
            log_cmd_error("Options -prove-skip and -tempinduct don't work with each other.\n");

        if (prove_skip >= seq_len && prove_skip > 0)
            log_cmd_error("The value of -prove-skip must be smaller than the one of -seq.\n");

        if (set_init_undef + set_init_zero + set_init_def > 1)
            log_cmd_error("The options -set-init-undef, -set-init-def, and -set-init-zero are exclusive!\n");

        if (set_def_inputs) {
            for (auto &it : module->wires_)
                if (it.second->port_input)
                    sets_def.push_back(it.second->name.str());
        }

        if (show_inputs) {
            for (auto &it : module->wires_)
                if (it.second->port_input)
                    shows.push_back(it.second->name.str());
        }

        if (show_outputs) {
            for (auto &it : module->wires_)
                if (it.second->port_output)
                    shows.push_back(it.second->name.str());
        }

        if (tempinduct)
        {
            if (loopcount > 0 || max_undef)
                log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");

            SatHelper basecase(design, module, enable_undef);
            SatHelper inductstep(design, module, enable_undef);

            basecase.sets = sets;
            basecase.prove = prove;
            basecase.prove_x = prove_x;
            basecase.prove_asserts = prove_asserts;
            basecase.sets_at = sets_at;
            basecase.unsets_at = unsets_at;
            basecase.shows = shows;
            basecase.timeout = timeout;
            basecase.sets_def = sets_def;
            basecase.sets_any_undef = sets_any_undef;
            basecase.sets_all_undef = sets_all_undef;
            basecase.sets_def_at = sets_def_at;
            basecase.sets_any_undef_at = sets_any_undef_at;
            basecase.sets_all_undef_at = sets_all_undef_at;
            basecase.sets_init = sets_init;
            basecase.set_init_def = set_init_def;
            basecase.set_init_undef = set_init_undef;
            basecase.set_init_zero = set_init_zero;
            basecase.satgen.ignore_div_by_zero = ignore_div_by_zero;
            basecase.ignore_unknown_cells = ignore_unknown_cells;

            for (int timestep = 1; timestep <= seq_len; timestep++)
                basecase.setup(timestep);
            basecase.setup_init();

            inductstep.sets = sets;
            inductstep.prove = prove;
            inductstep.prove_x = prove_x;
            inductstep.prove_asserts = prove_asserts;
            inductstep.shows = shows;
            inductstep.timeout = timeout;
            inductstep.sets_def = sets_def;
            inductstep.sets_any_undef = sets_any_undef;
            inductstep.sets_all_undef = sets_all_undef;
            inductstep.satgen.ignore_div_by_zero = ignore_div_by_zero;
            inductstep.ignore_unknown_cells = ignore_unknown_cells;

            inductstep.setup(1);
            inductstep.ez.assume(inductstep.setup_proof(1));

            if (tempinduct_def) {
                std::vector<int> undef_state = inductstep.satgen.importUndefSigSpec(inductstep.satgen.initial_state.export_all(), 1);
                inductstep.ez.assume(inductstep.ez.NOT(inductstep.ez.expression(ezSAT::OpOr, undef_state)));
            }

            for (int inductlen = 1; inductlen <= maxsteps || maxsteps == 0; inductlen++)
            {
                log("\n** Trying induction with length %d **\n", inductlen);

                // phase 1: proving base case

                basecase.setup(seq_len + inductlen);
                int property = basecase.setup_proof(seq_len + inductlen);
                basecase.generate_model();

                if (inductlen > 1)
                    basecase.force_unique_state(seq_len + 1, seq_len + inductlen);

                log("\n[base case] Solving problem with %d variables and %d clauses..\n",
                        basecase.ez.numCnfVariables(), basecase.ez.numCnfClauses());

                if (basecase.solve(basecase.ez.NOT(property))) {
                    log("SAT temporal induction proof finished - model found for base case: FAIL!\n");
                    print_proof_failed();
                    basecase.print_model();
                    if(!vcd_file_name.empty())
                        basecase.dump_model_to_vcd(vcd_file_name);
                    goto tip_failed;
                }

                if (basecase.gotTimeout)
                    goto timeout;

                log("Base case for induction length %d proven.\n", inductlen);
                basecase.ez.assume(property);

                // phase 2: proving induction step

                inductstep.setup(inductlen + 1);
                property = inductstep.setup_proof(inductlen + 1);
                inductstep.generate_model();

                if (inductlen > 1)
                    inductstep.force_unique_state(1, inductlen + 1);

                if (inductlen < initsteps)
                {
                    log("\n[induction step] Skipping problem with %d variables and %d clauses (below initsteps).\n",
                            inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());
                    inductstep.ez.assume(property);
                }
                else
                {
                    if (!cnf_file_name.empty())
                    {
                        FILE *f = fopen(cnf_file_name.c_str(), "w");
                        if (!f)
                            log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));

                        log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
                        cnf_file_name.clear();

                        inductstep.ez.printDIMACS(f, false);
                        fclose(f);
                    }

                    log("\n[induction step] Solving problem with %d variables and %d clauses..\n",
                            inductstep.ez.numCnfVariables(), inductstep.ez.numCnfClauses());

                    if (!inductstep.solve(inductstep.ez.NOT(property))) {
                        if (inductstep.gotTimeout)
                            goto timeout;
                        log("Induction step proven: SUCCESS!\n");
                        print_qed();
                        goto tip_success;
                    }

                    log("Induction step failed. Incrementing induction length.\n");
                    inductstep.ez.assume(property);
                    inductstep.print_model();
                }
            }

            log("\nReached maximum number of time steps -> proof failed.\n");
            if(!vcd_file_name.empty())
                inductstep.dump_model_to_vcd(vcd_file_name);
            print_proof_failed();

        tip_failed:
            if (verify) {
                log("\n");
                log_error("Called with -verify and proof did fail!\n");
            }

            if (0)
        tip_success:
            if (falsify) {
                log("\n");
                log_error("Called with -falsify and proof did succeed!\n");
            }
        }
        else
        {
            if (maxsteps > 0)
                log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");

            SatHelper sathelper(design, module, enable_undef);

            sathelper.sets = sets;
            sathelper.prove = prove;
            sathelper.prove_x = prove_x;
            sathelper.prove_asserts = prove_asserts;
            sathelper.sets_at = sets_at;
            sathelper.unsets_at = unsets_at;
            sathelper.shows = shows;
            sathelper.timeout = timeout;
            sathelper.sets_def = sets_def;
            sathelper.sets_any_undef = sets_any_undef;
            sathelper.sets_all_undef = sets_all_undef;
            sathelper.sets_def_at = sets_def_at;
            sathelper.sets_any_undef_at = sets_any_undef_at;
            sathelper.sets_all_undef_at = sets_all_undef_at;
            sathelper.sets_init = sets_init;
            sathelper.set_init_def = set_init_def;
            sathelper.set_init_undef = set_init_undef;
            sathelper.set_init_zero = set_init_zero;
            sathelper.satgen.ignore_div_by_zero = ignore_div_by_zero;
            sathelper.ignore_unknown_cells = ignore_unknown_cells;

            if (seq_len == 0) {
                sathelper.setup();
                if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
                    sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
            } else {
                std::vector<int> prove_bits;
                for (int timestep = 1; timestep <= seq_len; timestep++) {
                    sathelper.setup(timestep);
                    if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
                        if (timestep > prove_skip)
                            prove_bits.push_back(sathelper.setup_proof(timestep));
                }
                if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
                    sathelper.ez.assume(sathelper.ez.NOT(sathelper.ez.expression(ezSAT::OpAnd, prove_bits)));
                sathelper.setup_init();
            }
            sathelper.generate_model();

            if (!cnf_file_name.empty())
            {
                FILE *f = fopen(cnf_file_name.c_str(), "w");
                if (!f)
                    log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));

                log("Dumping CNF to file `%s'.\n", cnf_file_name.c_str());
                cnf_file_name.clear();

                sathelper.ez.printDIMACS(f, false);
                fclose(f);
            }

            int rerun_counter = 0;

        rerun_solver:
            log("\nSolving problem with %d variables and %d clauses..\n",
                    sathelper.ez.numCnfVariables(), sathelper.ez.numCnfClauses());

            if (sathelper.solve())
            {
                if (max_undef) {
                    log("SAT model found. maximizing number of undefs.\n");
                    sathelper.maximize_undefs();
                }

                if (!prove.size() && !prove_x.size() && !prove_asserts) {
                    log("SAT solving finished - model found:\n");
                } else {
                    log("SAT proof finished - model found: FAIL!\n");
                    print_proof_failed();
                }

                sathelper.print_model();

                if(!vcd_file_name.empty())
                    sathelper.dump_model_to_vcd(vcd_file_name);

                if (loopcount != 0) {
                    loopcount--, rerun_counter++;
                    sathelper.invalidate_model(max_undef);
                    goto rerun_solver;
                }

                if (!prove.size() && !prove_x.size() && !prove_asserts) {
                    if (falsify) {
                        log("\n");
                        log_error("Called with -falsify and found a model!\n");
                    }
                } else {
                    if (verify) {
                        log("\n");
                        log_error("Called with -verify and proof did fail!\n");
                    }
                }
            }
            else
            {
                if (sathelper.gotTimeout)
                    goto timeout;
                if (rerun_counter)
                    log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
                else if (!prove.size() && !prove_x.size() && !prove_asserts) {
                    log("SAT solving finished - no model found.\n");
                    if (verify) {
                        log("\n");
                        log_error("Called with -verify and found no model!\n");
                    }
                } else {
                    log("SAT proof finished - no model found: SUCCESS!\n");
                    print_qed();
                    if (falsify) {
                        log("\n");
                        log_error("Called with -falsify and proof did succeed!\n");
                    }
                }
            }

            if (!prove.size() && !prove_x.size() && !prove_asserts) {
                if (falsify && rerun_counter) {
                    log("\n");
                    log_error("Called with -falsify and found a model!\n");
                }
            } else {
                if (verify && rerun_counter) {
                    log("\n");
                    log_error("Called with -verify and proof did fail!\n");
                }
            }
        }

        if (0) {
    timeout:
            log("Interrupted SAT solver: TIMEOUT!\n");
            print_timeout();
            if (fail_on_timeout)
                log_error("Called with -verify and proof did time out!\n");
        }
    }

Here is the call graph for this function:

void Pass::extra_args ( std::vector< std::string >  args, size_t  argidx, RTLIL::Design *  design, bool  select = true  )

inherited

Definition at line 128 of file register.cc.

{
    for (; argidx < args.size(); argidx++)
    {
        std::string arg = args[argidx];

        if (arg.substr(0, 1) == "-")
            cmd_error(args, argidx, "Unknown option or option in arguments.");

        if (!select)
            cmd_error(args, argidx, "Extra argument.");

        handle_extra_select_args(this, args, argidx, args.size(), design);
        break;
    }
    // cmd_log_args(args);
}

Here is the call graph for this function:

virtual void SatPass::help ( )

inlinevirtual

Reimplemented from Pass.

Definition at line 810 of file sat.cc.

    {
        //   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
        log("\n");
        log("    sat [options] [selection]\n");
        log("\n");
        log("This command solves a SAT problem defined over the currently selected circuit\n");
        log("and additional constraints passed as parameters.\n");
        log("\n");
        log("    -all\n");
        log("        show all solutions to the problem (this can grow exponentially, use\n");
        log("        -max <N> instead to get <N> solutions)\n");
        log("\n");
        log("    -max <N>\n");
        log("        like -all, but limit number of solutions to <N>\n");
        log("\n");
        log("    -enable_undef\n");
        log("        enable modeling of undef value (aka 'x-bits')\n");
        log("        this option is implied by -set-def, -set-undef et. cetera\n");
        log("\n");
        log("    -max_undef\n");
        log("        maximize the number of undef bits in solutions, giving a better\n");
        log("        picture of which input bits are actually vital to the solution.\n");
        log("\n");
        log("    -set <signal> <value>\n");
        log("        set the specified signal to the specified value.\n");
        log("\n");
        log("    -set-def <signal>\n");
        log("        add a constraint that all bits of the given signal must be defined\n");
        log("\n");
        log("    -set-any-undef <signal>\n");
        log("        add a constraint that at least one bit of the given signal is undefined\n");
        log("\n");
        log("    -set-all-undef <signal>\n");
        log("        add a constraint that all bits of the given signal are undefined\n");
        log("\n");
        log("    -set-def-inputs\n");
        log("        add -set-def constraints for all module inputs\n");
        log("\n");
        log("    -show <signal>\n");
        log("        show the model for the specified signal. if no -show option is\n");
        log("        passed then a set of signals to be shown is automatically selected.\n");
        log("\n");
        log("    -show-inputs, -show-outputs\n");
        log("        add all module input (output) ports to the list of shown signals\n");
        log("\n");
        log("    -ignore_div_by_zero\n");
        log("        ignore all solutions that involve a division by zero\n");
        log("\n");
        log("    -ignore_unknown_cells\n");
        log("        ignore all cells that can not be matched to a SAT model\n");
        log("\n");
        log("The following options can be used to set up a sequential problem:\n");
        log("\n");
        log("    -seq <N>\n");
        log("        set up a sequential problem with <N> time steps. The steps will\n");
        log("        be numbered from 1 to N.\n");
        log("\n");
        log("    -set-at <N> <signal> <value>\n");
        log("    -unset-at <N> <signal>\n");
        log("        set or unset the specified signal to the specified value in the\n");
        log("        given timestep. this has priority over a -set for the same signal.\n");
        log("\n");
        log("    -set-def-at <N> <signal>\n");
        log("    -set-any-undef-at <N> <signal>\n");
        log("    -set-all-undef-at <N> <signal>\n");
        log("        add undef constraints in the given timestep.\n");
        log("\n");
        log("    -set-init <signal> <value>\n");
        log("        set the initial value for the register driving the signal to the value\n");
        log("\n");
        log("    -set-init-undef\n");
        log("        set all initial states (not set using -set-init) to undef\n");
        log("\n");
        log("    -set-init-def\n");
        log("        do not force a value for the initial state but do not allow undef\n");
        log("\n");
        log("    -set-init-zero\n");
        log("        set all initial states (not set using -set-init) to zero\n");
        log("\n");
        log("    -dump_vcd <vcd-file-name>\n");
        log("        dump SAT model (counter example in proof) to VCD file\n");
        log("\n");
        log("    -dump_cnf <cnf-file-name>\n");
        log("        dump CNF of SAT problem (in DIMACS format). in temporal induction\n");
        log("        proofs this is the CNF of the first induction step.\n");
        log("\n");
        log("The following additional options can be used to set up a proof. If also -seq\n");
        log("is passed, a temporal induction proof is performed.\n");
        log("\n");
        log("    -tempinduct\n");
        log("        Perform a temporal induction proof. In a temporalinduction proof it is\n");
        log("        proven that the condition holds forever after the number of time steps\n");
        log("        specified using -seq.\n");
        log("\n");
        log("    -tempinduct-def\n");
        log("        Perform a temporal induction proof. Assume an initial state with all\n");
        log("        registers set to defined values for the induction step.\n");
        log("\n");
        log("    -prove <signal> <value>\n");
        log("        Attempt to proof that <signal> is always <value>.\n");
        log("\n");
        log("    -prove-x <signal> <value>\n");
        log("        Like -prove, but an undef (x) bit in the lhs matches any value on\n");
        log("        the right hand side. Useful for equivialence checking.\n");
        log("\n");
        log("    -prove-asserts\n");
        log("        Prove that all asserts in the design hold.\n");
        log("\n");
        log("    -prove-skip <N>\n");
        log("        Do not enforce the prove-condition for the first <N> time steps.\n");
        log("\n");
        log("    -maxsteps <N>\n");
        log("        Set a maximum length for the induction.\n");
        log("\n");
        log("    -initsteps <N>\n");
        log("        Set initial length for the induction.\n");
        log("\n");
        log("    -timeout <N>\n");
        log("        Maximum number of seconds a single SAT instance may take.\n");
        log("\n");
        log("    -verify\n");
        log("        Return an error and stop the synthesis script if the proof fails.\n");
        log("\n");
        log("    -verify-no-timeout\n");
        log("        Like -verify but do not return an error for timeouts.\n");
        log("\n");
        log("    -falsify\n");
        log("        Return an error and stop the synthesis script if the proof succeeds.\n");
        log("\n");
        log("    -falsify-no-timeout\n");
        log("        Like -falsify but do not return an error for timeouts.\n");
        log("\n");
    }

Here is the call graph for this function:

void Pass::init_register ( )

staticinherited

Definition at line 54 of file register.cc.

{
    while (first_queued_pass) {
        first_queued_pass->run_register();
        first_queued_pass = first_queued_pass->next_queued_pass;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Pass::post_execute ( Pass::pre_post_exec_state_t  state )

inherited

Definition at line 84 of file register.cc.

{
    int64_t time_ns = PerformanceTimer::query() - state.begin_ns;
    runtime_ns += time_ns;
    current_pass = state.parent_pass;
    if (current_pass)
        current_pass->runtime_ns -= time_ns;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Pass::pre_post_exec_state_t Pass::pre_execute ( )

inherited

Definition at line 74 of file register.cc.

{
    pre_post_exec_state_t state;
    call_counter++;
    state.begin_ns = PerformanceTimer::query();
    state.parent_pass = current_pass;
    current_pass = this;
    return state;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Pass::run_register ( )

virtualinherited

Reimplemented in Backend, and Frontend.

Definition at line 48 of file register.cc.

{
    log_assert(pass_register.count(pass_name) == 0);
    pass_register[pass_name] = this;
}

Here is the caller graph for this function:

Field Documentation

int Pass::call_counter

inherited

Definition at line 36 of file register.h.

Pass* Pass::next_queued_pass

inherited

Definition at line 60 of file register.h.

std::string Pass::pass_name

inherited

Definition at line 29 of file register.h.

int64_t Pass::runtime_ns

inherited

Definition at line 37 of file register.h.

std::string Pass::short_help

inherited

Definition at line 29 of file register.h.

---

The documentation for this struct was generated from the following file:

• sat.cc