HOME
UP
  PREV
NEXT (ABD - Naive Path to State Conversion)
ABD - PSL Properties and Macros
PSL defines some simple path to state macros
- rose(X) means { !X; X }
- fell(X) means { X; !X }
Others are easy to define:
- stable(X) can be defined as { X; X } || { !X; !X }
- changed(X) can be defined as { X; !X } || { !X; X }
- onehot(X) can be defined as X is a power of 2
- onehot0(X) can be defined as onehot(X) || (X==0)