Assume/Assert Cell Support #18
Conversation
Codecov Report
@@ Coverage Diff @@
## master #18 +/- ##
==========================================
- Coverage 81.31% 80.48% -0.83%
==========================================
Files 19 19
Lines 2884 2942 +58
Branches 625 632 +7
==========================================
+ Hits 2345 2368 +23
- Misses 497 530 +33
- Partials 42 44 +2
Continue to review full report at Codecov.
|
nmigen/back/pysim.py
Outdated
| raise NotImplementedError("Asserts not yet implemented for Simulator backend.") # :nocov: | ||
|
|
||
| def on_Assume(self, stmt): | ||
| raise NotImplementedError("Assumes not yet implemented for Simulator backend.") # :nocov: |
There was a problem hiding this comment.
Assumes should be ignored during simulation.
nmigen/hdl/xfrm.py
Outdated
|
|
||
| def on_Assume(self, stmt): | ||
| # Preserve _en, as the compiler state thinks _en is driven. | ||
| return Assume(self.on_value(stmt.test), _en=stmt_en) |
nmigen/hdl/xfrm.py
Outdated
| @@ -164,6 +176,14 @@ def on_value(self, value): | |||
| def on_Assign(self, stmt): | |||
| return Assign(self.on_value(stmt.lhs), self.on_value(stmt.rhs)) | |||
|
|
|||
| def on_Assert(self, stmt): | |||
| # Preserve _en, as the compiler state thinks _en is driven. | |||
There was a problem hiding this comment.
This comment is incorrect; _en is in fact driven. Besides, preserving parts of statements during transforms doesn't really need additional comments.
nmigen/hdl/xfrm.py
Outdated
| @@ -328,6 +354,12 @@ def groups(self): | |||
| def on_Assign(self, stmt): | |||
| self.unify(*stmt._lhs_signals()) | |||
|
|
|||
| def on_Assert(self, stmt): | |||
| self.unify(*stmt._lhs_signals()) | |||
There was a problem hiding this comment.
You can probably just do on_Assert = on_Assign.
| @@ -352,6 +384,16 @@ def on_Assign(self, stmt): | |||
| if any_lhs_signal in self.signals: | |||
| return stmt | |||
|
|
|||
| def on_Assert(self, stmt): | |||
cr1901
force-pushed
the
formal
branch
4 times, most recently
from
3bdf7b8
to
1dfa82d
Compare
| self.test = Value.wrap(test) | ||
| if _en is None: | ||
| self._en = Signal(1, reset_less=True, | ||
| name="assume${}$en".format(src(self.test.src_loc))) |
There was a problem hiding this comment.
This produces utterly gigantic IL statements like connect \A \assert$/home/whitequark/Projects/Boneless-CPU/boneless/gateware/formal.py:25$check. I think it's sufficient to call them something like $assume$en`
|
Merged. |
Scope
This PR adds the beginning of formal verification support to
nmigen. With this PR, a user can now write statements of the following form:The first statement in particular will create
Asserts/Assumes analogous toyosys's "properties":A
yosyspropertyis syntactic sugar for:The third statement is analogous to a SystemVerilog immediate
assert/assume.The generated RTLIL can then be fed to
yosys, which outputs ansmtv2file. Usingyosys-smtbmcorsymbiyosys, one can now run a basic formal verification flow usingnmigen!Limitations
initial assume/assertnot yet supported (easy to add initial support, but I don't know what the semantics should be if they are used within anIf/Else/Switchcontext.propertyis for concurrent asserts, and AFAIKyosysdoes not support these).