Separation logic for high-level synthesis. (2017)