VLSI CAD 2

Bayesian Optimization 설명

안녕하세요. 오늘은 Bayesian optimization에 대해서 설명해보려고 합니다.제가 연구에 자주 사용하는 최적화 모델인데, 내용이 어려워서 한 번 정리하는 용도예요.연구를 예시로 들어서 설명을 할 수 있습니다.OptimizaitonOptimization. 즉, 최적화는 결국 내가 어떠한 입력을 넣었을 때, 최고의 효율을 갖는 출력을 뽑는 과정입니다. 이 과정에서는 parameter, objective function (=fitness function), opt. model 등 여러 요소가 사용됩니다. 아래의 그림을 보면서 천천히 설명해 보겠습니다.  Frequency (circuit speed)를 objective로 설정했다고 가정해 봅시다. Freq.를 출력하기 위해서는 단순하게는 clock ..

Satisfiability Modulo Theories (SMT) solver Z3

SMT 란 ?컴퓨터 과학 및 수학에서 SMT는 해당 mathematical formulation (수학적 공식)을 만족하는 지 결정하는 문제입니다. 기존의 Boolean satisfiability (SAT)는 Boolean formulation만 표현할 수 있지만, SMT는 추가적으로 실수, 정수, list, array, bit vector, 그리고 str과 같은 다양한 data를 사용한 보다 복합적인 formulation을 해결할 수 있습니다. 다음은 SAT의 예시입니다.$$(A\lor \neg B)\land (B \lor C)$$이 SAT 문제의 해결책은 A, B, C에 Boolean value를 할당하여, 표현식을 참으로 만드는 조합을 찾는 것입니다.예로 A=1, B=0, C=1이면 표현식은 참이 ..

VLSI CAD/Solver 2024.05.16