sees Past as a pritimive that samples a signal’s value in its own domain.That is, Past’s control set is determined locally at the point of use. I see Past as a primitive that samples an expression’s value in a given domain.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()
#Multiclock domain verification#
"""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? Also: always use always_ff or always_comb, never use always.It seems I can write something like m.d.comb += Assert(Past(signal) = 0). This must also be added to your property. The reset can be synchronous or asynchronous as you choose. That is, both x and temp should have resets local to their individual clock domains. The flipflops created should have resets.
#Multiclock domain update#
If the above doesn't work, or if it seems like a waste to start parallel assertions checking the same thing, the following code might work.Įdit2: Put x inside property and changed two final lines in property to update x to correct values. Thus you cannot check the value made by some other instance of this assertion. I removed the out = x ^ x check from line #3 because x is local to the property. Thus t will be updated to the new value on every posedge of clkA and you will have n assertions checking the same thing(which isn't a problem). A possible fix might be to declare the variable t outside the property scope. I must admit that I am hazy on the scoping of values local to a property, but check if this is causing you troubles. Lastly, what happens if clkA is much faster than clkB? Several assertions will start in parallel and disagree on the actual value of t on the first posedge of clkB. In that case the following would be more correct, although the previous code might still work. The way I read this the assertion should start on every clkA, and then a sequence will always follow. Line #2 is not e prerequisite for line #3, and the same can be said for line #3 and line #4. In my experience a non-overlapping implication will cause the assertion to sample not on the next clkB, but skip one clkB and then sample on clkB.įurthermore I don't quite understand why you are using implications all the way through your assertion. That is, with a overlapping implication in the clock handover.
0 kommentar(er)
