Hongce Zhang comments

Results 8 comments of


                                            Hongce Zhang

chocolatey package and include paths

Any news on this issue in 2021?

Update Refinement Handling in Verilog Verification Target Generation

Honestly speaking, I'm having issues with compiling it on Windows. The core issue is in the dependent repo: https://github.com/zhanghongce/vexpparser, where I have no way to have the compiler on windows...

Update Refinement Handling in Verilog Verification Target Generation

> Hi Hongce, > > Can you grant me access to the repo for pr, I'd like to make a few changes to the script to see if that works....

watcher stack overflow

Hi Yuheng, I suspect that this has something to do with the CoSA installation. wonder how CoSA was installed. Are you using the docker image?

watcher stack overflow

Thanks for the info. However, I'm afraid that this is out of our scope. As you see it is something deep in the lingeling SAT solver which is subsequently used...

Parsing multiple files

In my case, after adding the change below: https://github.com/zhanghongce/verilog-vcd-parser/commit/10b408cc419be2df01fadf879fd46fbea2f0a813 it seems to work. But I'm not sure if this is the right fix.

SMT target and SystemVerilog target?

It seems that `-sv` option is for System Verilog target. But I encounter another error: ``` Internal error: Unreachable code (at "src/sail_sv_backend/jib_sv.ml" line 207): model/riscv_types.sail:408.21-42: 408 | " with xlen="...

GTKWave does not support signal names with a colon `:`

Many thanks for your suggestion! I don't see other special characters that Jasper generates.