시뮬레이션(Simulation)은 배포의 용이성과 직관적인 워크플로우 덕분에 프리실리콘(pre-silicon) 검증에서 여전히 지배적인 접근 방식입니다. 그러나 시뮬레이션은 실행 가능한 시간 예산 내에서 가능한 실행 트레이스(execution traces)의 제한된 부분 집합만을 탐색하기 때문에, 희귀한 코너 케이스(corner cases)를 탐색하지 못해 잠재적인 버그를 찾아내지 못하는 경우가 많습니다. 반면, 형식 검증(formal verification)은 정확성에 대한 수학적으로 엄격한 보장을 제공합니다. 하지만 형식 검증의 실제 도입은 대규모 설계에 대한 확장성(scalability) 문제뿐만 아니라, 자극 중심(stimulus-driven) 작업에서 설계 동작의 시퀀스 중심 공리적 관점(sequence-centric axiomatic view)으로의 사고방식 변화로 인해 정확한 검증 의도를 포착하기 위한 정밀한 속성(properties)을 작성해야 하는 추가적인 어려움으로 인해 제약을 받습니다. 본 논문은 시뮬레이션을 "더 형식적으로(more formal)" 만듦으로써 검증에 형식 방법론(formal methods)을 적용하는 장벽을 낮추는 것을 목표로 합니다. 이를 위해 시뮬레이션의 친숙한 실행 의미론(execution semantics)을 유지하면서도, 솔버(solver) 기반의 심볼릭 신호(symbolic signals)와 상태 전이(state transitions)를 통해 보강하여 심볼릭 입력 및 조건 하에서 RTL 동작의 체계적인 탐색을 가능하게 하는 단어 수준의 심볼릭 시뮬레이션(symbolic simulation) 프레임워크인 Forbench를 소개합니다. Forbench는 제약 조건(constraints)을 정의하고, 심볼릭 (공)시뮬레이션(symbolic (co-)simulations)을 조정하며, 속성 체크(property checks)를 수행하기 위해 기존의 시뮬레이션 기반 프레임워크와 유사한 Python 인터페이스를 제공합니다. 이러한 접근하기 쉬운 인터페이스 외에도, 실험을 통해 Forbench가 커버리지(coverage)의 손실 없이 기존의 심볼릭 방법론들보다 현저한 속도 향상을 달성함을 보여줍니다.