RTL Datapath Satisfiability Solving Using a Binary CSP Engine

We propose a binary constraint satisfaction problem （CSP ） based approach to the satisfiability problem of register-transfer level （RTL） datapaths,which is a critical issue in RTL verification and testing．The approach consists of three steps：datapath extraction,binary CSP modeling,and solution searching．In datapath extraction,we build the environments for all datapath units by making assignments to the Boolean interface variables and some word variables．Binary CSP modeling then translates the RTL datapath satisfiability problem to a binary CSP description,which in turn will be sent to a binary CSP engine and solved by conflict-directed backjumping search strategy． The answer will be either a witness of satisfiable instance or a unsatisfiable decision．Experimental results show that even without many optimization strategies exerted,the binary CSP based method still works fairly well,with better performance than LP-based method．