Boris Novoselov

stack ``` Version 2.9.3 aarch64 Compiled with: - Cabal-3.6.3.0 ```

``` resolver: url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/6.yaml ```

Hello, I have also encountered this issue. I am attempting to generate SMT from a simple design and am receiving an empty file. Has there been any progress?

I think I specified the checksum correctly, what could be the problem?

Hello @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 with...

P.S. I noticed this while compiling the project. ``` FAILED: [code=1] tools/circt/lib/Transforms/CMakeFiles/obj.CIRCTTransforms.dir/FlattenMemRefs.cpp.o /usr/bin/c++ -DCIRCT_INCLUDE_TESTS -DGTEST_HAS_RTTI=0 -D_DEBUG -D_GLIBCXX_ASSERTIONS -D_GLIBCXX_USE_CXX11_ABI=1 -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -I/home/ckaf/circt/build/tools/circt/lib/Transforms -I/home/ckaf/circt/lib/Transforms -I/home/ckaf/circt/build/include -I/home/ckaf/circt/llvm/llvm/include -I/home/ckaf/circt/include -I/home/ckaf/circt/build/tools/circt/include -isystem /home/ckaf/circt/llvm/llvm/../mlir/include...

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. I...

I think that's what I need, but I still can't get it to work. ``` ➜ smt_check circt-opt --convert-comb-to-smt results/alu.hw.mlir results/alu.hw.mlir:14:10: error: failed to legalize operation 'comb.icmp' that was explicitly...

> Representing stateful circuits in SMTLIB is fundamentally non-trivial since SMTLIB has no concept of state/procedure/time (i.e., there's not really a clear way to represent a register in SMTLIB). Bounded...