下面我们来讨论输出函数,输出函数是赋值函数的一部分,但又不同于状态迁移函数,因为它是输出信号的值的来源,不能被化简掉。但如果我们不对它进行任何处理,把组合赋值的输出函数和时序赋值的输出函数一样理解,就相当于将组合赋值延后了一个时钟周期处理,我们就不能区分图6.19中的两种情况。这样就出现一个新问题:如果输出函数是组合赋值时应该如何处理?
  
图6.19 输出信号的组合赋值和时序赋值
 

  在上面的步骤中,经过删除组合赋值后,除了部分输出函数外,其它所有赋值函数都已是时序赋值,我们可以将组合输出赋值表达式中所有变量用它们的表达式代替,但这种替换必须是同时进行的,否则就会出现多次替换的情况。
  设Set_Out是输出函数的集合,Outi ∈ Set_Out是对象 Oi 赋值表达式,具体算法如下:
   {
    对于所有的Outi ∈ Set_Out {
     如果Outi与全局时钟无关 {
      同时将Outi中所有信号替换为它们的赋值函数表达式;
     }
    }
   }

  组合赋值不能作为一种新的状态。只把时钟赋值的变量作为状态变量,而把组合赋值当成布尔表达式中的一部分,这是同步时序电路模型中的重要的改进,是符合实际情况的,使所得到的模型更合理,规模也大大减小。

  经过上述化简操作后,我们就将一个复合可验证VHDL子集的验证描述转换为一个用BDD表示的有限状态机模型。这个模型接下来就可以用同步有限状态机的状态搜索算法对它进行可达性分析,模型检验等。
  
  
本节我们介绍了如何从VHDL描述生成有限状态机模型的方法。不是所有的VHDL语句都能处理。正像综合有可综合子集一样,验证也只能处理一个可验证子集。