Repository navigation
Conversation
Enable one Verilog path for ALU, BCD and decoder logic by preserving widths, selections, comparisons, hierarchy and unique bit names through typed IR. Keep associative and literal grouping opt-in, and verify the logical behavior against independent arithmetic and display oracles.
Prevent settled dust and solid-block normalization from leaving downstream components in stale states after input changes. Keep external boundary drives during normalization, and make cloned route worlds share planes and rows so detailed routing can explore without repeated dense copies.
…ontracts Make generated combinational cells composable by reserving isolated IO, protecting pin approaches and preserving certified active output strength. Repair directional contacts, fanout fallback and pending-sink ranking; retain conservative local support rules and serialize the new routing and candidate contracts.
Establish reproducible Verilog-to-NBT checkpoints with independent static and transition verification, saved-NBT replay, and small verified viewer fixtures. Record the bounded 8-bit ADD/SUB routing failure separately from successful decoder, adder and 2/4-bit shared ADD/SUB results so future ALU work has honest baselines.
Keep the draft effort scoped to the full ALU and binary-to-decimal display pipeline, with explicit module contracts, staged completion criteria and verified progress. Preserve unresolved routing and transition-stability work so a working decoder is not mistaken for completion of the ALU.
Allow bounded SAT block minimization to compete with verified recipes while preserving independently drivable input boundaries, output contracts and provenance. Keep the backend opt-in and retain fallback candidates. Hash the persisted NBT representation so simulator-only power counters do not invalidate reusable Exact candidates, while retaining geometry and metadata checks.
Preserve the verified 4187-block decoder, its 3D baseline and reproducible experiment controls. Record actual Exact selection, adapter costs, cold generation time and the recipe-only Free3D control so global packing improvements are not attributed entirely to SAT. All saved decoder checkpoints pass independent NBT input and transition validation.
Expose the shared flattened combinational graph before physical partitioning so the four-input seven-output decoder can be solved without Global PnR or cell adapters. Preserve independent logical and NBT verification, fixed-face and free-pin controls, solver/encoding timing and explicit Unknown outcomes. Record five bounded attempts without claiming a new layout or an infeasibility proof.
Keep the 576-cell free-pin attempt and its solver/encoding measurements separate from successful cell-composition checkpoints. The four-worker 120-second run remained Unknown, so it provides neither a new NBT nor an infeasibility proof.
Add a reusable whole-decoder runner that verifies the constructed NBT before attempting separate compaction. Record bounded construction and restart failures to distinguish partial progress from a complete physical result and avoid claiming unexecuted compaction.
Provide opt-in template-constrained initial synthesis and stable polarity-compressed repeater ports so decoder construction can finish without Global PnR. Add per-case dust power justification and auxiliary vocabularies while preserving standalone model compatibility. Keep Cut internal to avoid materializing every cell pair.
Make ordinary Verilog to whole-decoder NBT reproducible without saved placement or Global PnR. Record independent input and transition verification, bounded template restrictions, and compaction measurements; retain the smaller verified baseline when compaction increases block count.
Make the published whole-decoder link resolve to its intended NBT instead of falling back to the first example. Fetch the example manifest without cached responses so newly published circuits appear after reload.
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
8-bit ALU와 이진수→BCD→7-segment 표시 회로를 일반 Verilog에서 NBT까지 컴파일하기 위한 누적 작업 PR이다. 7-segment 디코더를 첫 관통 사례로 삼았고, 이 브랜치에 ALU와 표시 회로의 물리 연결까지 계속 쌓는다. 전체 ALU가 완성된 상태가 아니므로 draft로 유지한다.
구현한 기반
PinAccess순서, 인증된 출력 세기 계약을 추가한다. 후보 cache와 snapshot에도 계약을 보존한다.검증된 물리 체크포인트
blank=08-bit ADD는 경계 사례와 고정 seed 무작위 입력을 포함한 제한된 검사이며, 전체 입력/전이 증명이 아니다. 4-bit ADD/SUB의 walk도 전체 순서쌍 검사가 아니다. 측정의 cache 상태와 재현 명령은 fixture 안내에 구분했다.
논리 단계에서는 ALU의 8개 연산/flags 524,288개 입력과 Double Dabble의 256개 입력을 독립 정답과 전수 비교했다. 이는 전체 ALU/표시 NBT 성공과 구분한다.
이 PR에 이어서 쌓을 작업
현재 8-bit ADD/SUB는 같은 예산의 12개 배치/순서 시도에서 모두 배선 실패했고, 성공 NBT가 없다. blank를 포함한 decoder도 정적 입력을 통과한 배치에서 전이 중 burnout이 검출되어 완료로 인정하지 않았다. 배치 선택 callback에서도 전이 검사를 수행해 이런 결과를 거절한다.
검증
cargo test --release --workspace --all-targets: core 444 passed, 0 failed, 56 ignored, 나머지 workspace/integration 검사 통과cargo check --release --workspace --all-targets통과npm run build:wasm(release) 및npm run build통과target/alu-display/에 둔다.전체 계획 · 구현 및 실패/성공 기록
Exact를 연결한 3D 압축
Global PnR에 bounded Exact SAT 셀 최소화 후보를 연결했다. 실제 외부 포트·NBT·모든 전이·역류 검증을 통과한 후보만 사용하고, provenance/cache/RCIR 설정을 보존한다.
같은 자유3D 대조군 대비 블록2.9%, 경계 상자 부피3.6% 감소다. 기존2층 대비 블록25.7% 감소지만 높이는16→64로 증가한다. 최초 Exact cold 실행은89.252초(후보 준비70.949초)였으며 최적성이나 전반적인 속도 개선을 주장하지 않는다. 최종 NBT의16개 입력·모든256개 전이·burnout 부재를 통과했다.
이번 확장 후 전체 release workspace는 core 447 passed, 0 failed, 56 ignored와 나머지 검사를 통과했다. 이후 cache v13의 NBT 내부 전력 카운터 정규화와 변조 거절, 실제 mixed Exact 셀 재로딩은 별도 회귀로 검증했다. 최종 workspace release check도 통과했다.
재현 명령과 조건별 측정
Decoder 전체를 단일 Exact 모델로 푸는 실험
20개 셀로 나누기 전의 공유 NOT/OR 그래프를 추출하는
lower_flat_logic_graph()와whole_decoder_exactrunner를 추가했다. 입력4개·출력7개·NOR28개를 하나의 SAT 모델에 동시에 넣으며, Global PnR와 물리 셀 recipe를 사용하지 않는다. 독립적인16개 입력의7개 출력 논리 검증과 기존 lowering/integration 회귀, workspace release check는 통과했다.자유 핀3×8×4/4×8×4/4×10×5 각30초,5×10×5의4-worker60초,면 인터페이스를 준5×10×5의4-worker60초 모두 UNKNOWN이었다. 추가 확대8×12×6(576칸)/4-worker120초도 변수390,656개·절2,925,936개,encoding1.279초·SAT120.621초의 UNKNOWN이었다.
총6회 모두 새 NBT를 찾지 못했으며 불가능 증명도 아니다. 기존4,187블록 결과는 개별 Exact 후보+Global PnR의 성공 사례로 별도 유지한다. 단일 모델은 현재 net 함수와 보수 vocabulary 범위에서의 물리 합성이며 무제한 Boolean 재합성의 최적해를 뜻하지 않는다.
조건별 결과와 재현 명령
전체 decoder의 Exact 구성 성공
일반 Verilog부터 공유 24-NOR 그래프를 만들고, 범용 NOR 템플릿에서 SAT가 배치 부분집합을 선택하는 단계별 Exact 구성으로 전체 7seg NBT를 완성했다. Global PnR나 기존 20개 물리 셀 분할을 사용하지 않는다.
이는 템플릿으로 탐색을 제한한 초기 구성의 성공이며, 위의 자유로운 단일 전역 SAT 모델이 성공했거나 전역 최적해를 찾았다는 뜻은 아니다. 출력 계약은 anywhere-observable이다. 전체 ALU·표시 통합은 아직 진행 중이므로 draft를 유지한다.
안정적인 보수 신호 경계, pitch 3 repeater 포트, 경우별 dust 전원 근거를 추가했다. 내부 Cut 술어의 불필요한 모든 셀 쌍 grounding도 제거했다. 기존 사용자 정의 모델과의 호환성을 유지한다.
최종 release 검증: core 456 passed, 0 failed, 56 ignored, integration 검사 통과, rsdsl 9 passed, native NBT wasm 3 passed, workspace all-target release check 통과. 기존 테스트의 NBT fixture 변경은 복원했다.
재현 스크립트 · 설계·제약·실험 기록 · 검증 요약 · NBT