ghdl-yosys-plugin

ghdl-yosys-plugin copied to clipboard

I've done some tests with liveness proofs using PSL properties like:

assert always (rose(a) -> eventually! b);

I noticed that such constructs are processed by GHDL (and Yosys), but Symbiyosys crashes with a Python assertion. Aside from the non-handled assertion in SymbiYosys, there seems to be no support for Yosys' $live cells. These are needed for liveness proofs. There is a function in the yosys kernel (kernel/rtlil.h) to create such cells, but the ghdl-yosys-plugin doesn't use it.

RTLIL::Cell* addLive   (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, const RTLIL::SigSpec &sig_en, const std::string &src = "");

If ghdl-yosys-plugin want to support liveness properties correctly for formal verification, such a $live cell has to be created for PSL properties when liveness properties are used. AFAIK using non-negated strong operators usually results in a liveness property. The only strong PSL operator which GHDL synthesis currently supports is the eventually! operator.

Notice that we had a similar issue some time ago in ghdl: ghdl/ghdl#1345 I assume that the non working liveness proof in that issue is caused by GHDL which doesn't create the $live cells needed for these kind of proofs.

Last time I looked at it, it seemed to me that $live semantic doesn't really match the semantic of PSL. Is it supported only by boolector ?

AFAIK liveness proofs are supported by superprove (suprove) and aiger-bmc (aigbmc). I've tested it with superprove.

I assume we would have to support like Yosys does it for the SVA unbounded s_eventually operator.

Maybe we write $assert and $live cells for such properties. I think that Yosys selects the cell types which are supported in the which mode. I've noticed that Yosys hands over only the appropriate cells when starting the solver. in mode live normal $assertcells are ignored, they aren't included in the aiger file which these solvers use.

I've looked into the yosys logs. When using mode live following transformations are done:

chformal -assume -early
chformal -assert2assume
chformal -cover -remove

In mode bmc these are done:

chformal -assume -early
chformal -live -fair -cover -remove