马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。
您需要 登录 才可以下载或查看,没有账号?注册
x
本帖最后由 victorz11 于 2011-1-10 17:50 编辑
第四章 形式验证方法............................................................................................. 61 4.1 形式验证方法简介.................................................................................................................................... 61 4.1.1定理证明......................................................................................................... 61 4.1.2模型检验......................................................................................................... 62 4.1.3等价性检查...................................................................................................... 65 4.1.4 形式验证与模拟方法的比较............................................................................ 66 4.2 布尔代数与布尔函数................................................................................................................................ 68 4.3 决策图.......................................................................................................................................................... 70 4.3.1 BDD与ROBDD的概念...................................................................................... 70 4.3.2 变量次序........................................................................................................ 75 4.3.3 BDD的操作..................................................................................................... 78 4.3.4 小结............................................................................................................... 88 4.4 等价性检查................................................................................................................................................. 89 4.4.1等价性检查基本算法........................................................................................ 89 4.4.2 节点映射和约束.............................................................................................. 91 4.5 布尔可满足问题........................................................................................................................................ 94 4.5.1 组合门的建模................................................................................................. 95 4.5.2 消解算法........................................................................................................ 96 4.5.3 基于搜索的算法.............................................................................................. 97 4.5.4 隐含图和学习............................................................................................... 100 4.6 模型检验................................................................................................................................................... 103 4.6.1 模型检验的基本过程..................................................................................... 104 4.6.2 Kripke结构..................................................................................................... 106 4.6.3 时序逻辑...................................................................................................... 108 4.6.4显式模型检验................................................................................................ 114 4.6.5 符号模型检验............................................................................................... 119 4.6.6 形式验证技术展望........................................................................................ 128 习题................................................................................................................................................................... 128 第五章 划分、布图规划和布局........................................................................ 132 5.1 划分............................................................................................................................................................ 132 5.1.1 划分问题的图论表示..................................................................................... 135 5.1.2 划分算法的分类............................................................................................ 137 5.1.3 组迁移算法................................................................................................... 138 5.1.4 模拟退火算法和遗传算法.............................................................................. 141 5.2 布图规划................................................................................................................................................... 143 5.2.1 问题描述...................................................................................................... 144 5.2.2 布图规划算法的分类..................................................................................... 145 5.2.3 基于约束的布图规划..................................................................................... 146 5.2.4 基于整型规划的布图规划.............................................................................. 146 5.2.5 二元矩形算法............................................................................................... 148 5.2.6 基于层次树的算法........................................................................................ 149 5.3 布局............................................................................................................................................................ 150 5.3.1 问题描述...................................................................................................... 151 5.3.3 基于模拟的布局算法..................................................................................... 154 5.3.4 基于划分的布局算法..................................................................................... 161 5.3.5 其它布局算法............................................................................................... 163 5.3.6 性能驱动的布局............................................................................................ 164 习题................................................................................................................................................................... 166 |