Jane Street 리버스 엔지니어링 챌린지 해결기

GDS 파일로 주어진 ASIC을 회로로 복원·시뮬레이션하고 120비트 입력을 역산해 정답 메시지 (* TWO STARS *)를 찾아냄 gdstk와 SKY130 문서로 도형·레이어·핀을 식별하고, 맞닿은 배선을 그래프로 합쳐 Verilog 회로로 변환함 워밍업에서 약 1,000개 부품과 20여 종의 셀을 처리한 뒤, 본 퍼즐에서는 약 10,000개 부품과 81종의 셀까지 추출 범위를 넓힘 모든 입력을 대입하는 대신 출력 조건을 시간 역순으로 제약식화하고, Z3에 수천 개의 제약을 전달해 동시에 높아져야 하는 신호들의 입력을 계산함 직접 만든 시뮬레이터와 도구 탓에 시행착오가 커졌지만, 검증 과정에서 실제 ASIC 연결 오류까지 발견했고 최종 해답도 Jane Street에서 확인받음 GDS 파일에서 메시지 단서 찾기 Jane Street의 원래 챌린지는 칩을 기술하는 GDS 파일을 역으로 분석해 ASIC이 수행하는 작업을 알아내는 문제임 워밍업에는 실제 칩 설계를 비롯한 추가 정보가 제공됨 본 퍼즐에는 GDS와 VCD 파일이 주어지지만 회로에 관한 정보는 훨씬 적음 GDS 내부에서 clk, rst, VGND, VPWR 같은 이름과 sky130_fd_sc_hd__ 접두사를 가진 논리 소자를 발견함 Python 라이브러리 gdstk로 워밍업 GDS를 읽자 27개 셀이 확인됨 본 퍼즐의 VCD 파일에서 ASCII처럼 보이는 값을 추출하자 TRY AGAIN이 반복돼, 회로 내부에 메시지 출력 기능이 있음을 확인함 챌린지에 사용한 코드는 GitHub 저장소에 공개함 직접 만든 도구가 만든 우회로 기존 도구를 조사하기보다 SQLite3를 구동부로 삼은 회로 시뮬레이터부터 직접 제작함 Python에서 회로를 설계하기 어렵자 별도의 하드웨어 기술 언어와 파서를 만들고, 입력 스크립트와 출력 검증용 하네스도 추가함 파형 뷰어까지 직접 만들려다 중단하고 surfer를 사용함 GDS 작업을 단순화하려고 raylib 기반의 기본 뷰어도 제작했지만 블록 배치 문제를 해결하지 못해 자체 도구 개발을 포기함 GDS 구조와 SKY130 셀 해석 Jane Street가 안내한 GDS Viewer로 워밍업 회로를 살펴보며 입력 위치를 대략 표시하고, 파일 속 배선 위치와 기존 회로 정보로 이를 확인함 GDS는 서로 다른 재료에 해당하는 여러 표준 레이어와 폭으로 칩의 3차원 기하 구조를 나타냄 오른쪽 위의 Jane Street 로고만 추출하려 했...