Skip to content

Commit 0d63696

Browse files
cliffordwolfcliffordwolf
committed
Merge branch 'forall'
2 parents 2521ed3 + b13e6bd commit 0d63696

File tree

17 files changed

+424
-98
lines changed

17 files changed

+424
-98
lines changed

‎README.md

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -387,15 +387,20 @@ Non-standard or SystemVerilog features for formal verification
387387
- The system task ``$initstate`` evaluates to 1 in the initial state and
388388
to 0 otherwise.
389389

390-
- The system task ``$anyconst`` evaluates to any constant value. This is
390+
- The system function ``$anyconst`` evaluates to any constant value. This is
391391
equivalent to declaring a reg as ``rand const``, but also works outside
392392
of checkers. (Yosys also supports ``rand const`` outside checkers.)
393393

394-
- The system task ``$anyseq`` evaluates to any value, possibly a different
394+
- The system function ``$anyseq`` evaluates to any value, possibly a different
395395
value in each cycle. This is equivalent to declaring a reg as ``rand``,
396396
but also works outside of checkers. (Yosys also supports ``rand``
397397
variables outside checkers.)
398398

399+
- The system functions ``$allconst`` and ``$allseq`` are used to construct formal
400+
exist-forall problems. Assertions are only violated if the trace vialoates
401+
the assertion for all ``$allconst/$allseq`` values and assumptions only hold
402+
if the trace satisfies the assumtion for all ``$allconst/$allseq`` values.
403+
399404
- The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
400405
supported in any clocked block.
401406

‎backends/smt2/smt2.cc

Lines changed: 72 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -32,16 +32,17 @@ struct Smt2Worker
3232
CellTypes ct;
3333
SigMap sigmap;
3434
RTLIL::Module *module;
35-
bool bvmode, memmode, wiresmode, verbose, statebv, statedt;
35+
bool bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode;
3636
dict<IdString, int> &mod_stbv_width;
37-
int idcounter, statebv_width;
37+
int idcounter = 0, statebv_width = 0;
3838

3939
std::vector<std::string> decls, trans, hier, dtmembers;
4040
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
4141
std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
4242
pool<Cell*> recursive_cells, registers;
4343

4444
pool<SigBit> clock_posedge, clock_negedge;
45+
vector<string> ex_state_eq, ex_input_eq;
4546

4647
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
4748
std::map<Cell*, int> memarrays;
@@ -106,10 +107,10 @@ struct Smt2Worker
106107
decls.push_back(decl_str + "\n");
107108
}
108109

109-
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt,
110+
Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, bool forallmode,
110111
dict<IdString, int> &mod_stbv_width, dict<IdString, dict<IdString, pair<bool, bool>>> &mod_clk_cache) :
111112
ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
112-
verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
113+
verbose(verbose), statebv(statebv), statedt(statedt), forallmode(forallmode), mod_stbv_width(mod_stbv_width)
113114
{
114115
pool<SigBit> noclock;
115116

@@ -507,14 +508,16 @@ struct Smt2Worker
507508
return;
508509
}
509510

510-
if (cell->type.in("$anyconst", "$anyseq"))
511+
if (cell->type.in("$anyconst", "$anyseq", "$allconst", "$allseq"))
511512
{
512513
registers.insert(cell);
513514
string infostr = cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell);
514515
if (cell->attributes.count("\\reg"))
515516
infostr += " " + cell->attributes.at("\\reg").decode_string();
516-
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, infostr.c_str()));
517+
decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort("\\Y")), infostr.c_str()));
517518
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")));
519+
if (cell->type == "$anyseq")
520+
ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
518521
register_bv(cell->getPort("\\Y"), idcounter++);
519522
recursive_cells.erase(cell);
520523
return;
@@ -787,14 +790,24 @@ struct Smt2Worker
787790
if (bvmode && GetSize(sig) > 1) {
788791
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
789792
get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
793+
if (wire->port_input)
794+
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
795+
get_id(module), get_id(wire), get_id(module), get_id(wire)));
790796
} else {
791797
for (int i = 0; i < GetSize(sig); i++)
792-
if (GetSize(sig) > 1)
798+
if (GetSize(sig) > 1) {
793799
decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
794800
get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
795-
else
801+
if (wire->port_input)
802+
ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
803+
get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
804+
} else {
796805
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
797806
get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
807+
if (wire->port_input)
808+
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
809+
get_id(module), get_id(wire), get_id(module), get_id(wire)));
810+
}
798811
}
799812
}
800813
}
@@ -919,20 +932,24 @@ struct Smt2Worker
919932
std::string expr_d = get_bool(cell->getPort("\\D"));
920933
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
921934
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
935+
ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort("\\Q")).c_str(), get_bool(cell->getPort("\\Q"), "other_state").c_str()));
922936
}
923937

924938
if (cell->type.in("$ff", "$dff"))
925939
{
926940
std::string expr_d = get_bv(cell->getPort("\\D"));
927941
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
928942
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
943+
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Q")).c_str(), get_bv(cell->getPort("\\Q"), "other_state").c_str()));
929944
}
930945

931-
if (cell->type == "$anyconst")
946+
if (cell->type.in("$anyconst", "$allconst"))
932947
{
933948
std::string expr_d = get_bv(cell->getPort("\\Y"));
934949
std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
935950
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
951+
if (cell->type == "$anyconst")
952+
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Y")).c_str(), get_bv(cell->getPort("\\Y"), "other_state").c_str()));
936953
}
937954

938955
if (cell->type == "$mem")
@@ -1044,6 +1061,7 @@ struct Smt2Worker
10441061
std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
10451062
std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
10461063
trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
1064+
ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
10471065

10481066
if (async_read)
10491067
hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
@@ -1086,6 +1104,37 @@ struct Smt2Worker
10861104
hier.push_back(stringf(" (|%s_h| (|%s_h %s| state))\n", get_id(c->type), get_id(module), get_id(c->name)));
10871105
trans.push_back(stringf(" (|%s_t| (|%s_h %s| state) (|%s_h %s| next_state))\n",
10881106
get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
1107+
ex_state_eq.push_back(stringf("(|%s_ex_state_eq| (|%s_h %s| state) (|%s_h %s| other_state))\n",
1108+
get_id(c->type), get_id(module), get_id(c->name), get_id(module), get_id(c->name)));
1109+
}
1110+
1111+
if (forallmode)
1112+
{
1113+
string expr = ex_state_eq.empty() ? "true" : "(and";
1114+
if (!ex_state_eq.empty()) {
1115+
if (GetSize(ex_state_eq) == 1) {
1116+
expr = "\n " + ex_state_eq.front() + "\n";
1117+
} else {
1118+
for (auto &str : ex_state_eq)
1119+
expr += stringf("\n %s", str.c_str());
1120+
expr += "\n)";
1121+
}
1122+
}
1123+
decls.push_back(stringf("(define-fun |%s_ex_state_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
1124+
get_id(module), get_id(module), get_id(module), expr.c_str()));
1125+
1126+
expr = ex_input_eq.empty() ? "true" : "(and";
1127+
if (!ex_input_eq.empty()) {
1128+
if (GetSize(ex_input_eq) == 1) {
1129+
expr = "\n " + ex_input_eq.front() + "\n";
1130+
} else {
1131+
for (auto &str : ex_input_eq)
1132+
expr += stringf("\n %s", str.c_str());
1133+
expr += "\n)";
1134+
}
1135+
}
1136+
decls.push_back(stringf("(define-fun |%s_ex_input_eq| ((state |%s_s|) (other_state |%s_s|)) Bool %s)\n",
1137+
get_id(module), get_id(module), get_id(module), expr.c_str()));
10891138
}
10901139

10911140
string assert_expr = assert_list.empty() ? "true" : "(and";
@@ -1336,6 +1385,7 @@ struct Smt2Backend : public Backend {
13361385
{
13371386
std::ifstream template_f;
13381387
bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
1388+
bool forallmode = false;
13391389

13401390
log_header(design, "Executing SMT2 backend.\n");
13411391

@@ -1443,14 +1493,26 @@ struct Smt2Backend : public Backend {
14431493
Module *topmod = design->top_module();
14441494
std::string topmod_id;
14451495

1496+
for (auto module : sorted_modules)
1497+
for (auto cell : module->cells())
1498+
if (cell->type.in("$allconst", "$allseq"))
1499+
goto found_forall;
1500+
if (0) {
1501+
found_forall:
1502+
forallmode = true;
1503+
*f << stringf("; yosys-smt2-forall\n");
1504+
if (!statebv && !statedt)
1505+
log_error("Forall-exists problems are only supported in -stbv or -stdt mode.\n");
1506+
}
1507+
14461508
for (auto module : sorted_modules)
14471509
{
14481510
if (module->get_bool_attribute("\\blackbox") || module->has_memories_warn() || module->has_processes_warn())
14491511
continue;
14501512

14511513
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
14521514

1453-
Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width, mod_clk_cache);
1515+
Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, forallmode, mod_stbv_width, mod_clk_cache);
14541516
worker.run();
14551517
worker.write(*f);
14561518

0 commit comments

Comments
 (0)