I believe that a global analysis that affects behavior is not a good fit for any part for the core language. Summarizing IRC discussion with I believe that a specification sub-language that is built around a local transformation (syntactic sugar for sampling an expression’s value in a given domain) as a good fit for the core language. Is that because I’ve violated the assumption that there is only one clock in the system and therefore yosys does unspecified behavior? However, now the cover trace looks distinctly odd:ĭata_out did change on the negative edge of ‘le’… but it also changed when le was stable. In that case, do I have to effectively make my own version of Past for the internal clock of the example module?īMC succeeds when multiclock is off, which also kind of makes sense to me, if signals are not allowed to change except on the positive edge of the global clock. In this case I probably shouldn’t be using Past, because really what I want to assert is that data_out is equal to what data_in was, when le was last high. This fails BMC when multiclock is on, which kind of makes sense to me, if Past is relative to the last cycle of the global clock. # With this off, it passes, but cover looks odd. M.d.comb += Assert(example.data_out = Past(example.data_in)) M.d.comb += Cover((example.data_out = 0xAAAAAAAA) & (example.le = 0) M.submodules.example = example = Example()
"""Formal verification for the example.""" M.d.internal_clk += self.data_out.eq(self.data_in) Internal_clk = ClockDomain("internal_clk", clk_edge="neg", local=True) # python example.py generate -t il > toplevel.ilĭef elaborate(self, _: Platform) -> Module: # other clock in the system - has a negative edge. # independent signal - assumed to be asynchrnous with any # Simple example that clocks data in into data out when the First, example.py: from nmigen import Signal, Module, Elaboratable, ClockDomain, Muxįrom nmigen.asserts import Assert, Fell, Past, Coverįrom nmigen.cli import main_parser, main_runner If multiclock is off in the sby file, what exactly is Past? It seems I can write something like m.d.comb += Assert(Past(signal) = 0).