mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 13:29:12 +00:00
Code Activity

verificsva: check -L value is small enough for code to work

Browse source
This commit is contained in:
N. Engelhardt 2025-07-09 15:58:35 +02:00
parent 7566af4a4b
commit e47f5369fd
2 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

3
frontends/verific/verific.cc
View file

@ -4124,6 +4124,9 @@ struct VerificPass : public Pass {
if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
cmd_error(args, argidx, "unknown option");
if ((unsigned long)verific_sva_fsm_limit >= sizeof(1ull)*8)
log_cmd_error("-L %d: limit too large; maximum allowed value is %zu.\n", verific_sva_fsm_limit, sizeof(1ull)*8-1);
std::set<std::string> top_mod_names;
if (mode_all)

8
frontends/verific/verificsva.cc
View file

@ -479,14 +479,14 @@ struct SvaFsm
GetSize(dnode.ctrl), verific_sva_fsm_limit);
}
for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
for (unsigned long long i = 0; i < (1ull << GetSize(dnode.ctrl)); i++)
{
Const ctrl_val(i, GetSize(dnode.ctrl));
pool<SigBit> ctrl_bits;
for (int i = 0; i < GetSize(dnode.ctrl); i++)
if (ctrl_val[i] == State::S1)
ctrl_bits.insert(dnode.ctrl[i]);
for (int j = 0; j < GetSize(dnode.ctrl); j++)
if (ctrl_val[j] == State::S1)
ctrl_bits.insert(dnode.ctrl[j]);
vector<int> new_state;
bool accept = false, cond = false;