- - Formal proof between two FSM descriptions
See the file man1/alc_origin.1.
- fsp [-V] format1 format2
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)).
uses a Reduced Ordered Binary Decision Diagrams representation 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
gives the path for the FSM descriptions. The default value is the current
gives some auxiliary pathes for the FSM descriptions. The default value is the
-V Sets verbose mode on. Each step of the formal proof is displayed on the
fsp fsm fsm digi digi2
See the file man1/alc_bug_report.1.