<cr1901_modern>
Last time multiclock came up, I recall wq didn't want explicit $global_clock support in nmigen. Which would mean having to write out assumptions that eventually every clock domain eventually ticks
<cr1901_modern>
(otherwise, the SMT solver will just provide a CEX where none of the clocks ever tick)
<cr1901_modern>
until the last proof step*
<awygle>
i think writing explicit assumptions to tick the clocks is not unreasonable, but i wouldn't mind a clock domain for $global_clock either. it seems like a natural default_clk for the formal platform.
<cr1901_modern>
I don't remember wq's reasoning, and I'm pretty sure the logs where we discussed it in privmsg (predates #nmigen) are on another computer.
<awygle>
i also think that "cex where no clocks tick" is not universally applicable
<awygle>
depends on your properties
<awygle>
and solver maybe
<awygle>
since the inductive portion of a k-induction proof will be able to assume violating values
<awygle>
that's probably what you meant
<awygle>
i have been enjoying pdr not requiring me to fuck around with such things
<cr1901_modern>
1. I want to say "holding all the clocks at a single value until the final proof step is equivalent of turning your n-step k induction into a 1-step k-induction". But this only _feels_ correct.
<cr1901_modern>
2. All the CEXes I had when first learning multiclock were of the above form. So I assume it's common :P.
<awygle>
lol yes, fair
<awygle>
but that may be at least in part because ~all learning resources for yosys formal teach only k-induction
<cr1901_modern>
I haven't done much formal since Aug 2018. And well, last year around this time was effectively a reset on everything for me. So I'm def not up to date.
<awygle>
mhm
<whitequark>
awygle: is that latency necessary?
<whitequark>
I came to the same conclusion but I don't understand why is it fundamentally needed
<whitequark>
it feels like working around something irrelevant
<awygle>
i think it's because the read port isn't transparent
<awygle>
but when i tried to make it transparent i got a weird error about a constant
<awygle>
and then i got pulled away
<awygle>
i have the impression that there's weirdness with memory read ports in yosys anyway
<awygle>
but i couldn't tell you exactly why
<awygle>
just am ambient impression
<whitequark>
awygle: ohh
<whitequark>
damn it, ok
<whitequark>
yes, transparent read ports can't have a read enable
<whitequark>
this is currently just hardcoded on the nmigen side, which is one of the single ugliest parts of nmigen
<whitequark>
but until someone fixes yosys we can't realistically use such ports anyway
<whitequark>
so i'd say increase the latency and leave a comment in there linking to the yosys issue
<whitequark>
the weirdness is basically just the memory_bram pass being an awful little pile of ad-hoc logic that never quite works well
<whitequark>
it needs a rewrite but this rewrite is so monumental that no one i know, including me, is up to the task of doing it
<awygle>
arright this is pissing me off, i'm gonna tap out for tonight
<awygle>
there are two "read_clk" signals in this VCD and one is twice as fast as the other
<awygle>
that's troubling at best
<awygle>
also this counterexample trace happily violates the CDC invariant of the grey code which i'm _almost_ sure is a formal testbench issue and not real
<awygle>
i'll figure out what's happening another time