How to set two signals are not the equal in SAT Pass

[hanm2019]

How to set two signals are not the equal in SAT Pass
I know the -set a a1 is to set the signal a equal to a1, however, how do I add a constraint that a is not equal to a1?

[georgerennie]

I believe there is currently no way to do this using the SAT pass, as the parser that passes the set expressions is only able to return SigSpecs, so things like signals, concatenations/extractions of signals and constants, but not more complex expressions on signals.
The SAT pass mainly gets used for internal testing as far as I'm aware, what is your use case for these constraints? There may be a better solution than adding support for this to the SAT pass.

[hanm2019]

Hi, I try to update the SAT pass

    for (auto &s: nsets_at[timestep]) {
        RTLIL::SigSpec lhs, rhs;

        if (!RTLIL::SigSpec::parse_sel(lhs, design, module, s.first))
            log_cmd_error("Failed to parse lhs set expression `%s'.\n", s.first.c_str());
        if (!RTLIL::SigSpec::parse_rhs(lhs, rhs, module, s.second))
            log_cmd_error("Failed to parse rhs set expression `%s'.\n", s.second.c_str());
        show_signal_pool.add(sigmap(lhs));
        show_signal_pool.add(sigmap(rhs));

        if (lhs.size() != rhs.size())
            log_cmd_error("Set expression with different lhs and rhs sizes: %s (%s, %d bits) vs. %s (%s, %d bits)\n",
                          s.first.c_str(), log_signal(lhs), lhs.size(), s.second.c_str(), log_signal(rhs), rhs.size());

        log("Import set-constraint for this timestep: %s != %s\n", log_signal(lhs), log_signal(rhs));
        check_undef_enabled(lhs);
        check_undef_enabled(rhs);
        ez->assume(ez->NOT(satgen.signals_eq(lhs, rhs, timestep)));
    }

It works for me