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

[LLHDToLLVM] Refactor conversion patterns of each dialect to separate files

Happy to work on this!

[circt-mc] Introduce `circt-mc` (supersedes #4647)

Also I remember in an ODM a while ago it was mentioned that `circt-mc` was ambiguous in case the `mc` was read to stand for 'machine code', alternative names welcome

[circt-mc] Introduce `circt-mc` (supersedes #4647)

Thanks for all the feedback @fabianschuiki - it seems pretty clear that the Circuit infrastructure needs trimming. Think I mentioned this to you before, but that seems like a lot...

[circt-mc] Introduce `circt-mc` (supersedes #4647)

Probably makes sense to close this now that we have a plan to replace this with a new version based on the SMT dialect stuff that @maerhart is currently upstreaming,...

[SMT] Added support for :pattern attribute

Sorry @luisacicolini, looks like rebasing with the correct LLVM commit made GitHub think I was the author of the commits on the branch!

`comb` dialect: `typeSum` and `hList` seem suspicuous

> happy to eliminate `typeSum` given what [@TaoBi22](https://github.com/TaoBi22) said - I stuck with the `comb` doc which did not mention this afaict. will also give the `comb.concat` signature a try...

RFC: [AIG] Add an AIG dialect and circt-synth

Super exciting :smile:

[Verif] Lowering from `verif.formal` to `verif.bmc`

I'll take a look into this at some point, no promises on timescale though!

[SMT] How to go from Verilog to smtlib2 like with Yosys?

Hey @flaviens! Yeah, I *think* I know what the problem is here but @maerhart might be able to confirm. Currently the SMTLIB infrastructure we have is just focused on our...

export to smtlib

Hi @Ckaf! We don't really have a path from Verilog to a generically usable SMTLIB output currently - the reason for this is that our flow from hardware to SMTLIB...