Catherine
Catherine
Can you upload your IL so I can directly try with that?
I think the command I suggested works correctly; it's more that the annotation doesn't seem to help. Try adding `attribute \gclk 32'1` before `wire width 1 input 2 \clk` in...
Yeah, I can reproduce that. It's really confusing! Are you sure it passes *correctly* when you go through Verilog?
Ok so this is something about Verilog. This is incredibly stupid, but works: ``` [tasks] cover bmc [options] bmc: mode bmc cover: mode cover depth 10 multiclock on [engines] smtbmc...
> Yikes. There are a lot of intermediate wires in the cover trace now... but I guess I'll take it? Oof! To be clear this isn't actually a solution I...
Okay, I figured it out. The `gclk` attribute causes the Yosys AST frontend to change the netlist such that `$dff` cells connected to that clock become `$ff` cells. Try this:...
Oh yeah sorry, let me figure out why.
@RobertBaruch Ok well that took longer than expected... ``` [tasks] cover bmc [options] bmc: mode bmc cover: mode cover depth 10 multiclock on [engines] smtbmc z3 [script] read_verilog
Indeed, and a remarkably gross one. Basically what you want is to do `s/posedge \clk/global/` in the input RTLIL file (try it, that would work...) The `(*gclk*)` attribute, `$global_clock` and...
@RobertBaruch Per discussion with @cr1901, the tentative nMigen platform level solution would be to avoid exposing the global clock at all, but instead add an assumption that at least one...