Repository navigation

sync - #258

Merged

nanocoh merged 227 commits into

updatefrom

main

Sep 28, 2026

Commits on Jul 15, 2026
- Merge pull request #161 from keplertech/main
  nanocoh
  authored
  fae48b8
- reproduce with unit test
  nanocoh
  committed
  59cff31
- remove size nobs and fix X init
  nanocoh
  committed
  df443e8
- fix unit test
  nanocoh
  committed
  1c91a01
- strict F[0]
  nanocoh
  committed
  5f69217
- status update and unit test fixing
  nanocoh
  committed
  a654311
- unit test fixing
  nanocoh
  committed
  c1d07ae
- opt from PDR article + reset cache
  nanocoh
  committed
  9b39748
- opt from PDR article + reset cache
  nanocoh
  committed
  7185a43
- flags in readme + updating workflows
  nanocoh
  committed
  088ed8c
Commits on Jul 16, 2026
- update flags
  nanocoh
  committed
  d81d98e
- fix(sec): classify dual-rail X mismatches as inconclusive
  nanocoh
  committed
  96b2804
- fix(sec): reuse exact F[0] solvers across PDR batches
  nanocoh
  committed
  fa762f0
- remove timeout from tr test
  nanocoh
  committed
  edcfc1e
Commits on Jul 17, 2026
- Merge pull request #166 from keplertech/update
  nanocoh
  authored
  6c2af23
- wip(sec): add initialization-aware dual-rail PDR age discovery
  nanocoh
  committed
  c9058a9
- Merge origin/main into remove-internal-relations-between-designs
  nanocoh
  committed
  f6fc20e
- Make SEC PDR age discovery opt-in
  nanocoh
  committed
  7d7a03c
Commits on Jul 18, 2026
- unit test fix
  nanocoh
  committed
  8c72d18
- fix najaeda version
  nanocoh
  committed
  62271d7
- speed up pdr dual rail
  nanocoh
  committed
  8d1c5e3
Commits on Jul 19, 2026
- speed up dual-rail PDR with exact query caches
  nanocoh
  committed
  9aebc4f
- speed up exact dual-rail PDR query preparation
  nanocoh
  committed
  6237d57
- fix unit test
  nanocoh
  committed
  ea20fc7
Commits on Jul 20, 2026
- Align dual-rail SEC output proof semantics
  nanocoh
  committed
  c5f5b9f
- perf(sec): unblock exact dual-rail PDR residual proofs
  nanocoh
  committed
  d92e5e9
- perf(sec): share exact F[0] solver across PDR queries
  nanocoh
  committed
  7a7619b
Commits on Jul 21, 2026
- perf(sec): reuse exact PDR solver state
  nanocoh
  committed
  c327e2a
- fix(sec): preserve exact PDR predecessor solves
  nanocoh
  committed
  cb47217
- Restore exact PDR reuse and use singleton dual-rail batches
  nanocoh
  committed
  34ba3dc
- Use adaptive batching for dual-rail PDR
  nanocoh
  committed
  f711a12
Commits on Jul 22, 2026
- fix(sec): preserve exact PDR across adaptive batches
  nanocoh
  committed
  786bd4d
- fix(sec): separate dual-rail PDR mismatch and definedness proofs
  nanocoh
  committed
  c76cdfe
- test(sec): align CLI expectations with definedness proofs
  nanocoh
  committed
  b8f7627
- fix(sec): integrate dual-rail definedness into PDR
  nanocoh
  committed
  5b96366
Commits on Jul 23, 2026
- fix(sec): use steady-state dual-rail equivalence only
  nanocoh
  committed
  4665539
- perf(sec): reuse exact PDR frames across output batches
  nanocoh
  committed
  0c9cb77
- fix(sec): certify PDR invariants before cross-batch reuse
  nanocoh
  committed
  7ee39dd
- perf(sec): reduce PDR predecessor query overhead
  nanocoh
  committed
  67cec5b
- Speed up PDR generalization with narrow SAT probes
  nanocoh
  committed
  63d9743
- perf(sec): reuse PDR invariant certification solvers
  nanocoh
  committed
  69a7cd5
Commits on Jul 24, 2026
- fix(sec): bound PDR batch memory ownership
  nanocoh
  committed
  9b77f1e
Commits on Jul 25, 2026
- fix(sec): bound dual-rail PDR singleton SAT work
  nanocoh
  committed
  5806fb4
- perf(sec): bound cumulative PDR invariant certification
  nanocoh
  committed
  9541015
Commits on Jul 26, 2026
- first round eval updates and fixes
  nanocoh
  authored
  92f7134
- docs: document LEC and SEC verification options
  nanocoh
  committed
  afa1c89
- Merge pull request #168 from keplertech/remove-internal-relations-between-designs
  nanocoh
  authored
  a6f70fe
- docs: refresh SEC and sv2v configuration examples
  nanocoh
  committed
  907d13c
- Update README.md
  nanocoh
  authored
  cfb3b63
- Merge pull request #169 from keplertech/remove-internal-relations-between-designs
  nanocoh
  authored
  84c6c22
Commits on Jul 27, 2026
- naja fix for mutliple designs in lib files
  nanocoh
  committed
  f646b96
Commits on Jul 28, 2026
- ci: bump najaeda to 0.7.18
  nanocoh
  committed
  f359f6c
- test: regenerate Naja IF fixtures for 0.7.18
  nanocoh
  committed
  694e077
- naja fix for multiple design representation in lib files
  nanocoh
  authored
  08fa023
- Add configurable LEC boundary mismatch check
  nanocoh
  committed
  43f49bb
- Enable LEC boundary check by default
  nanocoh
  committed
  4141d97
Commits on Jul 29, 2026
- Add configurable LEC boundary mismatch check
  nanocoh
  authored
  30955cb
Commits on Jul 30, 2026
- Use Liberty sequential models in SEC
  nanocoh
  committed
  13778f4
- Merge remote-tracking branch 'origin/main' into new-feature
  nanocoh
  committed
  b9c1122
- Preserve Liberty clear/preset value in structural parsing in naja
  nanocoh
  committed
  a7b668f
- Generate Naja IF fixtures from local checkout in CI
  nanocoh
  committed
  d5a5a07
- Fix Naja Python build isolation in CI
  nanocoh
  committed
  47748e9
- Align Bazel with forked Naja
  nanocoh
  committed
  b310256
- Cover sequential model extraction edge cases
  nanocoh
  committed
  d3bf6ba
- Preserve Liberty nextstate_type in structural parsing
  nanocoh
  committed
  3e2cf75
Commits on Jul 31, 2026
- Build DB0 sequential models at construction in naja
  nanocoh
  committed
  e14989a
- Use Liberty sequential models in SEC
  nanocoh
  authored
  27cbb4f
- fix for blackbox parsing
  nanocoh
  committed
  9b98229
- fix for blackbox parsing
  nanocoh
  authored
  f34822f
Commits on Aug 1, 2026
- Merge pull request #182 from keplertech/main
  nanocoh
  authored
  07da964
- latest naja
  nanocoh
  committed
  5813cbe
- fix in naja for #181
  nanocoh
  authored
  5ba9015
Commits on Aug 2, 2026
- Add explicit Verilog top module selection
  nanocoh
  committed
  2ec5d2a
- Cover Verilog top option validation
  nanocoh
  committed
  d58b41d
- Merge pull request #185 from keplertech/main
  nanocoh
  authored
  d1ff11a
Commits on Aug 3, 2026
- Fix SEC frame-zero handling for combinational designs
  nanocoh
  committed
  5e077eb
- Reject mixed config and command-line options
  nanocoh
  committed
  ec579a3
- Fix SEC frame-zero handling for combinational designs
  nanocoh
  authored
  46bc3f6
- Add explicit verilog top module selection
  nanocoh
  authored
  9dd032c
Commits on Aug 4, 2026
- Build Naja natively with Bazel
  nanocoh
  committed
  3af3c86
- Fix Linux Bazel build
  nanocoh
  committed
  c7ba34c
- Fix Bazel 9 and Linux Python builds
  nanocoh
  committed
  281f909
- Fix Linux Bazel test linking
  nanocoh
  committed
  8732a88
- Unify Bazel fmt dependency
  nanocoh
  committed
  c3dfb08
- Build Slang natively with Bazel
  nanocoh
  committed
  86cec7e
- Fix empty Slang header globs
  nanocoh
  committed
  f22e10a
Commits on Aug 5, 2026
- Full bazel build
  nanocoh
  authored
  21abcf8
Commits on Aug 6, 2026
- Support shared divmod primitives in SEC
  nanocoh
  committed
  c610e3c
Commits on Aug 7, 2026
- Fix divmod CI integration and coverage
  nanocoh
  committed
  ad11350
- Merge main and resolve Naja dependency conflict
  nanocoh
  committed
  e12e9ef
Commits on Aug 8, 2026
- Support for divmod
  nanocoh
  authored
  5eced47
- Configure Naja Python primitive loading
  nanocoh
  committed
  c92689d
- Merge pull request #194 from keplertech/main
  nanocoh
  authored
  a2496bb
Commits on Aug 9, 2026
- Add Xilinx Python primitive support
  nanocoh
  committed
  3d4379c
- Fix Naja module install destination
  nanocoh
  committed
  80c46cb
Commits on Aug 10, 2026
- Fix Bazel Naja runtime exports
  nanocoh
  committed
  27b00f1
- Cover Naja Python path setup
  nanocoh
  committed
  6f70395
Commits on Aug 11, 2026
- Organize examples and document Python primitives
  nanocoh
  committed
  060a115
- Configure Naja Python primitive loading
  nanocoh
  authored
  f166317
- Document TinyRocket example commands
  nanocoh
  committed
  5a17f30
- Add examples section to python-primitives.md
  nanocoh
  authored
  0752f50
- Update README.md
  nanocoh
  authored
  212b877
- Update README.md
  nanocoh
  authored
  243b4b7
- Update docs
  nanocoh
  authored
  609bd07
Commits on Aug 12, 2026
- Document Xilinx examples
  nanocoh
  committed
  62d03c9
- Merge branch 'new-feature' of https://github.com/keplertech/kepler-formal into new-feature
  nanocoh
  committed
  6f08410
- Examples docs
  nanocoh
  authored
  b21bff0
- Readme update (#200)
  nanocoh
  authored
  e58e3f2
Commits on Aug 14, 2026
- allow : in liberty identifiers in naja (#202)
  nanocoh
  authored
  453cc25
Commits on Aug 21, 2026
- Report opaque terminals (#201)
  nanocoh
  authored
  d86614c
- update naja
  nanocoh
  committed
  a3c9c78
- Merge pull request #206 from keplertech/updateNaja
  nanocoh
  authored
  f519971
- Remove SEC clock-gate latch heuristic
  nanocoh
  committed
  7295650
- Handle clock-gate truth-table arity as opaque in SEC
  nanocoh
  committed
  21ee745
Commits on Aug 22, 2026
- Remove SEC clock-gate latch heuristic
  nanocoh
  authored
  a1a56e9
- Fix SEC regression coverage handling
  nanocoh
  committed
  65b4bdd
Commits on Aug 25, 2026
- init optional MCP server
  xtofalex
  committed
  ade649a
- Merge pull request #210 from xtofalex/mcp
  nanocoh
  authored
  7499733
- Fix SEC regression coverage handling + imc output batching
  nanocoh
  authored
  536902c
Commits on Aug 26, 2026
- Fix SV2V primitive collisions and constant SEC inputs
  nanocoh
  committed
  3084172
Commits on Aug 27, 2026
- Materialize constant sequential inputs in SEC
  nanocoh
  committed
  2a47ae3
- update naja
  nanocoh
  committed
  9d5443d
- Update clock-gate regression for Naja state-cell handling
  nanocoh
  committed
  df23122
Commits on Aug 28, 2026
- Add SEC reset bootstrap config
  nanocoh
  committed
  169cfc1
Commits on Aug 30, 2026
- Improve reset bootstrap coverage
  nanocoh
  committed
  ddeb005
- Cover SEC reset validation paths
  nanocoh
  committed
  d6ccfd0
- Add SEC reset bootstrap config
  nanocoh
  authored
  491c622
- Fix SV2V primitive collisions and constant SEC inputs
  nanocoh
  authored
  27cf790
Commits on Sep 1, 2026
- Add native Python package for Kepler Formal
  nanocoh
  committed
  6316d8b
- Fix table-select truth table input ordering
  nanocoh
  committed
  4b527d3
- Bundle isolated NajaEDA runtime in Python package
  nanocoh
  committed
  28908b8
- Bundle isolated NajaEDA runtime in Python package
  nanocoh
  committed
  5948397
- Update Naja state-cell handling
  nanocoh
  committed
  9f5d525
- Fix table-select truth table input ordering
  nanocoh
  authored
  8b597e3
- Fix Python package CI checks
  nanocoh
  committed
  9f6662d
- Fix manylinux Bison version for Python wheels
  nanocoh
  committed
  e178762
- Build Cap'n Proto with PIC for Python wheels
  nanocoh
  committed
  f665ebc
Commits on Sep 2, 2026
- Fix dual-rail PDR scheduling for hard output batches
  nanocoh
  committed
  49b5556
- Merge pull request #224 from keplertech/fix8
  nanocoh
  authored
  3a0e0ab
- Merge pull request #225 from keplertech/main
  nanocoh
  authored
  843aae8
- Merge pull request #226 from keplertech/main
  nanocoh
  authored
  ef43e58
- Add structured driver coverage tests
  nanocoh
  committed
  a799de3
Commits on Sep 4, 2026
- Update Naja state-cell handling
  nanocoh
  authored
  fcb3d23
- fix: update Naja for Liberty state cells
  nanocoh
  committed
  ec128fa
- fix: update Naja for automatic variable selects
  nanocoh
  committed
  071446c
Commits on Sep 5, 2026
- fix: update Naja for Liberty state cells and automatic variable selects
  nanocoh
  authored
  4992da5
Commits on Sep 7, 2026
- feat: export prepared SEC problems as BTOR2
  nanocoh
  committed
  524ffba
- fix: prefer vendored GoogleTest headers in test builds
  nanocoh
  committed
  86b912c
- test: clear BoolExpr cache after BTOR2 exporter cases
  nanocoh
  committed
  a1a6f2a
- test: cover BTOR2 export validation and strategy options
  nanocoh
  committed
  f28626b
- Update Naja to latest main and sync Bazel pin
  nanocoh
  committed
  f1feae2
Commits on Sep 8, 2026
- Fix GoogleTest header precedence in CMake tests
  nanocoh
  committed
  3b69efd
- Merge pull request #232 from keplertech/fix8
  nanocoh
  authored
  aa5cf7a
- preparation for py release
  nanocoh
  authored
  11d8ac4
- Fix Python CLI arguments and nested NajaEDA dependency discovery
  nanocoh
  committed
  c3d8d08
- Add PyPI publishing and match NajaEDA wheel coverage
  nanocoh
  committed
  ccc767a
Commits on Sep 9, 2026
- Report X/Z constants and source locations in SEC skips
  nanocoh
  committed
  717f921
- Add tests for SEC unknown-constant diagnostic coverage
  nanocoh
  committed
  0718e54
Commits on Sep 10, 2026
- Report X/Z constants and source locations in SEC skips
  nanocoh
  authored
  62da988
- Merge main into fix9 and preserve BTOR2 driver integration
  nanocoh
  committed
  d3f71c2
- feat: export prepared SEC problems as BTOR2
  nanocoh
  authored
  4b6b1bf
- Share NajaEDA runtime and verify live Python designs
  nanocoh
  committed
  1ad14a3
Commits on Sep 11, 2026
- Merge main into fix7 and preserve shared-runtime driver builds
  nanocoh
  committed
  16aa74b
- Fix Windows shared Naja SDK paths and cover cache invalidation
  nanocoh
  committed
  a449c45
- Add initial NixOS CLI package and installed smoke checks
  nanocoh
  committed
  666b621
- Match Nix package targets to Python wheel platforms
  nanocoh
  committed
  cc49419
- Fix Glucose proof output compatibility on Windows
  nanocoh
  committed
  c5ca350
- Disable unused C++ module scanning in Darwin Nix builds
  nanocoh
  committed
  1bfbbf4
- Disable implicit TBB linkage for Windows Python builds
  nanocoh
  committed
  5e342b7
- Add manual publishing to the keplertech Nix cache
  nanocoh
  committed
  9650767
- Add initial NixOS CLI package and installed smoke checks
  nanocoh
  authored
  0e0abf2
Commits on Sep 12, 2026
- Fix reduced truth-table input dependencies in logic clouds
  nanocoh
  committed
  ec170c8
- Fix reduced truth-table input dependencies in logic clouds
  nanocoh
  authored
  503443a
- Simplify Nix binary installation instructions
  nanocoh
  committed
  c5db7bf
- Document minimal Nix installation under Distribution
  nanocoh
  committed
  5f45c9d
- Restore Cachix setup in installation instructions
  nanocoh
  committed
  2dca9d7
- Test prebuilt Nix profile installation from Cachix
  nanocoh
  committed
  62c83d6
- Link to official Nix installation instructions
  nanocoh
  committed
  13a8c51
- nix installation instructions
  nanocoh
  authored
  571ae59
Commits on Sep 13, 2026
- Merge remote-tracking branch 'origin/main' into fix7
  nanocoh
  committed
  985adcd
- Remove Python API and MCP sections from README
  nanocoh
  committed
  f2fa0bd
- Remove Python API and MCP sections from README
  nanocoh
  committed
  23c8df1
- Merge pull request #239 from keplertech/updateReadme
  nanocoh
  authored
  f70c2e3
Commits on Sep 14, 2026
- Separate thin native drivers from the shared verification API
  nanocoh
  committed
  e0e5571
- Merge branch 'keplertech:main' into main
  nanocoh
  authored
  506d9c0
- Relicense first-party code as Apache-2.0
  nanocoh
  committed
  a657782
- Adding version information and associated CLI flag
  xtofalex
  committed
  9b99d6b
- Keep Python verification on borrowed NajaEDA designs
  nanocoh
  committed
  6425f0d
- Merge branch 'main' into versioning
  xtofalex
  committed
  82c9de0
Commits on Sep 15, 2026
- Adding version information and associated CLI flag
  nanocoh
  authored
  1716a71
- Relicense first-party code as Apache-2.0
  nanocoh
  authored
  d871c7c
- Release borrowed verification loggers after each call
  nanocoh
  committed
  82473cc
- Merge upstream main and preserve borrowed-design Python API
  nanocoh
  committed
  9d092c1
- Fix Kissat bitfield layout in Windows wheels
  nanocoh
  committed
  eee880d
Commits on Sep 16, 2026
- Bined python to najaeda
  nanocoh
  authored
  1289f70
- Add source-built Python regression with TinyRocket live designs
  nanocoh
  committed
  df9c9b5
- Update README.md
  nanocoh
  authored
  226e8bb
- Add source-built Python regression with TinyRocket live designs
  nanocoh
  authored
  036c19f
- Add opt-in published NajaEDA Python release flow
  nanocoh
  committed
  e3f6b6e
- Gate published NajaEDA wheel tests on release requests
  nanocoh
  committed
  cbdda43
- Merge branch 'keplertech:main' into main
  nanocoh
  authored
  72e711a
- Merge pull request #247 from nanocoh/main
  nanocoh
  authored
  4aea9d6
- Avoid unavailable Naja object APIs in published Windows wheels
  nanocoh
  committed
  8cc1031
- Update Readme
  nanocoh
  authored
  d2c3254
- Avoid unavailable Naja object APIs in published Windows wheels
  nanocoh
  authored
  0ce1f2e
- Separate default wheel regression from the publication gate
  nanocoh
  committed
  0898999
Commits on Sep 17, 2026
- Separate default wheel regression from the publication gate
  nanocoh
  authored
  1c826a9
Commits on Sep 19, 2026
- Add explicit paired instance boundaries
  nanocoh
  committed
  b3acbe6
- Expand paired boundary validation coverage
  nanocoh
  committed
  dfdef98
- Use logical extraction boundaries without netlist mutation
  nanocoh
  committed
  9fee8b7
- Fix truth-table test helper declaration after boundary extension
  nanocoh
  committed
  f88cab4
- Limit instance boundaries to leaves and use original DNL connectivity
  nanocoh
  committed
  7ea53e1
- Summarize SEC regression runtime, verdicts, and output coverage
  nanocoh
  committed
  ce21c97
Commits on Sep 20, 2026
- Add explicit paired instance boundaries
  nanocoh
  authored
  4a4ad38
- Add optional certified internal relation learning for SEC
  nanocoh
  committed
  c3c4a9a
- Reuse certified internal relations throughout exact IMC
  nanocoh
  committed
  a544142
- Disable two SEC matrix jobs that stall pull requests
  nanocoh
  committed
  a0c34b6
- Add optional certified internal relation learning for SEC
  nanocoh
  authored
  c7b8fe6
- Certify internal relations by literal substitution instead of assumptions
  
  claude
  authored and
  nanocoh
  committed
  726805a
Commits on Sep 21, 2026
Commits on Sep 22, 2026

Commits

Commits on Jul 15, 2026

Commits on Jul 16, 2026

Commits on Jul 17, 2026

Commits on Jul 18, 2026

Commits on Jul 19, 2026

Commits on Jul 20, 2026

Commits on Jul 21, 2026

Commits on Jul 22, 2026

Commits on Jul 23, 2026

Commits on Jul 24, 2026

Commits on Jul 25, 2026

Commits on Jul 26, 2026

Commits on Jul 27, 2026

Commits on Jul 28, 2026

Commits on Jul 29, 2026

Commits on Jul 30, 2026

Commits on Jul 31, 2026

Commits on Aug 1, 2026

Commits on Aug 2, 2026

Commits on Aug 3, 2026

Commits on Aug 4, 2026

Commits on Aug 5, 2026

Commits on Aug 6, 2026

Commits on Aug 7, 2026

Commits on Aug 8, 2026

Commits on Aug 9, 2026

Commits on Aug 10, 2026

Commits on Aug 11, 2026

Commits on Aug 12, 2026

Commits on Aug 14, 2026

Commits on Aug 21, 2026