Atticus Kuhn

Chore: prove that addition on BitStreams corresponds to Additon on BitVectors

10

There are currently two sorries in the file `BitStream.lean`. This proof removes one sorry, in the case of addition by proving that addition on BitVectors agrees with addition on BitStreams...

Idea: Possible way to shorten the code of the MLIR Parser

2

Here is an idea that could shorten the code for the lean-mlir parser substantially. The gist of this idea is to not do any typechecking ourselves, but to syntactically transform...

Chore: Add Documentation to Automata Tactic

3

Add documentation explaining the purpose and inner workings of the automata tactic. CC: @Superty because he was asking about how the automata tactic functions.

Bug: Why does GitHub workflow build Mathlib?

3

Take a look at the GitHub workflow logs, for example, https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867 Here is an excerpt of the output: ``` 9m 11s Run lake -R exe cache get # download cache...

See https://grosser.zulipchat.com/#narrow/stream/248449-Project---Lean4/topic/Overflow.20Flags.20in.20LLVM For more information,

lean-mlir does support the syntax ``` llvm.icmp.eq llvm.icmp.sgt llvm.icmp.ne ... ``` But it does not support the syntax ``` llvm.icmp "eq" ``` which is allowed by the llvm mlir standard....

[circt-opt] Add pass `--convert-core-to-fsm`

1

This PR adds a pass to `circt-opt` called `--convert-core-to-fsm`. This pass converts code written in RTL (`comb` + `seq`) and converts it to the `fsm` dialect. It recognises and extracts...

[circt-verilog] 'moore.case_eq' operand must be simple bit vector type, but got array

1

I ran `circt-verilog` on this file from OpenTitan: https://github.com/lowRISC/opentitan/blob/d8b5efd1427152b8387d6e03d9db413167e58475/hw/ip/lc_ctrl/rtl/lc_ctrl_fsm.sv I got this error: ```bash ak2518@autobot:/local/scratch/ak2518/opentitan$ /local/scratch/ak2518/circt/build/bin/circt-verilog --debug --parse-only /local/scratch/ak2518/opentitan/hw/ip/lc_ctrl/rtl/lc_ctrl_fsm.sv -yhw/ip/prim_generic/rtl -yhw/ip/prim/rtl -yhw/ip/lc_ctrl/rtl -yhw/ip/rom_ctrl/rtl -Ihw/ip/prim/rtl -yhw/ip/prim_generic/rtl -DYOSYS -DSYNTHESIS --mlir-print-ir-after-failure --verbose-pass-executions --mlir-pass-statistics...

[circt-verilog] `circt-verilog` produces non `comb`/`seq` dialects including `cf` and `llhd`

3

I am trying to convert this file found in OpenTitan from SystemVerilog to MLIR: https://github.com/lowRISC/opentitan/blob/d8b5efd1427152b8387d6e03d9db413167e58475/hw/top_englishbreakfast/ip_autogen/pwrmgr/rtl/pwrmgr_fsm.sv When I run `circt-verilog`, it produces unexpected dialects like `cf` and `llhd`. I don't expect...