Bea Healy

icon location Cambridge, UK icon location PhD Student at the University of Cambridge (Previously at University of Manchester and University of Edinburgh)

Results 15 comments of Bea Healy

export to smtlib

Hey @Ckaf! I've pushed a couple of PRs this week that mean we now have a flow for converting combinational modules to usable SMTLIB. If you add the `for-smtlib-export` to...

export to smtlib

> Hello [@TaoBi22](https://github.com/TaoBi22)! That's great! I am currently researching open tools for formal verification of hardware circuits, and I am interested in what the current limitations are for supporting circuits...

export to smtlib

> Okay, I was able to compile the project. The issue was with the flag `-DLLVM_ENABLE_LLD=ON`, and I think I can even fix it if I get around to it....

export to smtlib

Ah yeah, I took a look at the Yosys flow and I think that emitting the transition functions as they do should definitely be possible. We don't have any proper...

[ImportVerilog] moore.conversion generated instead of moore.int_to_string

The generated Moore IR is: ``` module { moore.module @top() { %0 = moore.constant_string "Test" : i32 %1 = moore.conversion %0 : !moore.i32 -> !moore.string %a = moore.variable %1 :...