T. Meissner

Good work. But I'm not sure if it is good to hard-code git as source code management system.

I get the same error for gentype, but also for the genmultilib patch. For example: pushd gcc-4.6-2012.03 && \ patch -N -p0 < ../patches/gcc-multilib-bash.patch && \ popd ; ~/Temp/jsnyder-arm-eabi-toolchain-4c24572/gcc-4.6-2012.03 ~/Temp/jsnyder-arm-eabi-toolchain-4c24572...

Wow. I also use Modelsim / Questa at work and didn't know, that you can click on a timestamp in the transcript window to set the cursor in the wave...

@JimLewis Ah, okay. You mean then you have 2 timestamps in one line, and Modelsim / Questa only recognizes the firestone, which isn't the time at of the event. I...

Okay. I will create a PR when I've made the necessary additions to the docs.

@efykse Sure that the ram array isn't optimized away? I don't know exactly if an assertion count as something similar like an output, but without the assert the ram would...

@efykse Yes, that could be the case with the reset. For formal, you don't want a dedicated BRAM, as you can't really verify it's content anymore. However, even when I...

AFAIK liveness proofs are supported by superprove (`suprove`) and aiger-bmc (`aigbmc`). I've tested it with superprove. I assume we would have to support like Yosys does it for the SVA...

Yeah, you're probably right. `d0 = true` would be valid, or simply `d0`. This is an artifact of my tries to implement support of parameters of type `bit`, I assume....

For me, the reproducer is not so beautiful coding style, we would never allow this code in our company ;) Especially this: ```vhdl if rising_edge(clk) and ce = '1' then...