NikLeberg comments

Results 33 comments of


                                            NikLeberg

formal: add yosys+ghdl backend

> What is missing while CI? Oh, I haven't noticed that the action for pr https://github.com/SpinalHDL/docker/pull/11 did fail and you had to revert. I'll loot into it. > Does it...

formal: add yosys+ghdl backend

Why is `pastValid()` implemented with `initial()` instead of `init()` ? See [`formal/package.scala#L20`](https://github.com/SpinalHDL/SpinalHDL/blob/42b22b3eea7db0d9570ba3d17c2828673c47dd3a/core/src/main/scala/spinal/core/formal/package.scala#L20) ```scala def pastValid() : Bool = signalCache(ClockDomain.current -> "formal.pastValid")(RegNext(True) initial(False) setWeakName("formal_with_past")) ``` This fails in VHDL, where the...

formal: add yosys+ghdl backend

In both cases (using `init` or `initial`), the following verilog is emitted: ```verilog initial begin formal_with_past = 1'b0; end always @(posedge clk) begin formal_with_past

formal: add yosys+ghdl backend

I added commit #[94f07b1](https://github.com/SpinalHDL/SpinalHDL/pull/1429/commits/94f07b166a76ad7d0ddcea888449ac5de40b7f31) that implements the discussed change from `initial` to `init` for the formal `pastValid`. Maybe @Dolu1990 can help us out and explain if we would break something...

formal: add yosys+ghdl backend

About CI.. I don't think your pr #1455 did what you think it did? It is now using the `latest` tag that was last pushed/released to one year ago.

formal: add yosys+ghdl backend

Ah, so I have to change the image tag that is used in the action yaml? Can do... that commit shall never enter dev though. I can also test under...

formal: add yosys+ghdl backend

Hi @Readon I think implementation wise this is done. I'm passing all tests locally with latest upstream GHDL version #[3b05281](https://github.com/ghdl/ghdl/commit/3b05281987f194478fea538a843411c775931a09). This latest GHDL version is required as there was a...