Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

home | help
FSP(1)			   CAO-VLSI Reference Manual			FSP(1)

NAME
       fsp    -	Formal proof between two FSM descriptions

SYNOPSIS
       fsp [-V]	format1	format2	file1  file2

DESCRIPTION
       Made  to	 run on	FSM descriptions, fsp supports the same	subset of VHDL
       as syf (for further informations	 about	this  subset  see  SYF(1)  and
       FSM(5)).	 fsp uses a Reduced Ordered Binary Decision Diagrams represen-
       tation and computes the product of the  two  FSM	 descriptions.	 After
       this  step,  it	explores the resulting FSM product and proves formally
       the equivalence between the two initial FSM  descriptions.   Those  two
       descriptions must have the same interface (VHDL entity).

ENVIRONMENT VARIABLES

       MBK_WORK_LIB  gives  the	 path  for  the	FSM descriptions.  The default
	      value is the current directory.

       MBK_CATA_LIB gives some auxiliary pathes	for the	FSM descriptions.  The
	      default value is the current directory.

OPTIONS
       -V  Sets	verbose	mode on. Each step of the formal proof is displayed on
       the standard output.

EXAMPLE
	    fsp	fsm fsm	digi digi2

SEE ALSO
	syf (1), fmi (1), fsm (5), xfsm	(1).

ASIM/LIP6			October	1, 1997				FSP(1)

NAME | SYNOPSIS | DESCRIPTION | ENVIRONMENT VARIABLES | OPTIONS | EXAMPLE | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=fsp&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help