diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-02-26 11:58:44 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-02-26 11:58:44 +0100 |
| commit | 675dd5347ad7bafdfa95f97b60996595a32f2c7d (patch) | |
| tree | 7704de79f2b65895f296185028626e79a3a12f71 /README.md | |
| parent | fba499b8666ef33bc5b11ce2df7b8b18a5aeaa75 (diff) | |
| download | yosys-675dd5347ad7bafdfa95f97b60996595a32f2c7d.tar.gz yosys-675dd5347ad7bafdfa95f97b60996595a32f2c7d.tar.bz2 yosys-675dd5347ad7bafdfa95f97b60996595a32f2c7d.zip | |
Small fixes and improvements in $allconst/$allseq handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -396,10 +396,11 @@ Non-standard or SystemVerilog features for formal verification but also works outside of checkers. (Yosys also supports ``rand`` variables outside checkers.) -- The system functions ``$allconst`` and ``$allseq`` are used to construct formal - exist-forall problems. Assertions are only violated if the trace vialoates - the assertion for all ``$allconst/$allseq`` values and assumptions only hold - if the trace satisfies the assumtion for all ``$allconst/$allseq`` values. +- The system functions ``$allconst`` and ``$allseq`` can be used to construct + formal exist-forall problems. Assumptions only hold if the trace satisfies + the assumtion for all ``$allconst/$allseq`` values. For assertions and cover + statements it is sufficient if just one ``$allconst/$allseq`` value triggers + the property (similar to ``$anyconst/$anyseq``). - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are supported in any clocked block. |