问答题

　第1题
　什么是形式验证？形式验证与模拟验证有什么不同？请选择（多选）：
　(1) 从数学上完备地证明或验证电路的实现方案（简称实现）是否确实实现了电路设计描述（简称描述）的功能。
　(2) 是按照语言描述的顺序一步一步地运行来验证电路的功能。
　(3) 形式验证需要给出电路输入向量，以判断电路运行是否正确。
　(4) 形式验证的结果指出所要求的电路功能或性质是否正确。


　第2题
　形式验证与模拟验证各有什么优缺点？


　第3题
　什么是等价性验证？什么是性质验证？有什么区别？


　第4题
　BDD的概念是什么？如何表示布尔函数？有什么重要性质？


　第5题
　组合电路的等价性验证依据是什么？


　第6题
　用x₁,x₂,x₃,x₄的变量序，画出函数的BDD，并化简。


　第7题
　用x₂,x₄,x₃,x₁的变量序，画出函数的BDD，并化简。比较习题6与习题7的结果。


　第8题
　试用变量顺序s,x₁,x₂，画出下面的真值表相应的BDD,并进行化简。共有多少非叶子节点？

　第9题
　改用变量序x₁,x₂,s重新做习题7的要求。


　第10题
　改用变量序x₁,s,x₂重新做习题7的要求。比较习题8，习题9，习题10的结果，哪种变量序得到的节点最少？


　第11题
　综合时利用不管项得到的电路为什么会引起BDD的不同。组合电路等价性验证中如何处理不管信息引起的电路不一致问题？


　第12题
　模型检验的基本过程是什么？本章介绍的方法中，用________描述电路行为，用______描述性质。


　第13题
　什么是同步时序电路模型？与一般时序电路模型有什么区别？


　第14题
　CTL是个什么样的逻辑？如何表示电路性质？各个时间运算符的意义是什么？


　第15题
　试画出A[fUg]和E[fUg]的示意图。首先画出Afg和Efg，然后再根据Afg和Efg画出A[fUg]和E[fUg]。


　第16题
　如何根据有限自动机模型和CTL模型进行模型检验？


　第17题
　如何生成有限自动机模型？如何体现时序的同步？


　第18题
　仿照图6.11，画出case语句用if表示的流程图表示。


　第19题
　将下面的语句画出流程图表示。
　　IF Sel = '0' THEN
　　　　　　　　f <= x₁;
　　ELSE
　　　　　　　　f <= X₂;
　　END IF;


　第20题
　画出下面语句的流程图表示：
　　f <= "01" WHEN req1 = '1' ELSE
　　　　 "10" WHEN req2 = '1' ELSE
　　　　 "11" WHEN req3 = '1' ELSE
　　　　 "00";


　第21题
　画出下面语句组的流程图表示：
　　Tmp := 0;
　　FOR i IN 1 TO 3 LOOP
　　　IF X(i) = '1' THEN
　　　　　Tmp := Tmp + 1;
　　　END IF;
　　END LOOP;
　　Cout <= Tmp;