blackboxes and whiteboxes. Use ``read_verilog -specify`` to enable this
functionality. (By default specify .. endspecify blocks are ignored.)
+- The module attribute ``abc_box_id`` specifies a positive integer linking a
+ blackbox or whitebox definition to a corresponding entry in a `abc9`
+ box-file.
+
+- The port attribute ``abc_scc_break`` indicates a module input port that will
+ be treated as a primary output during `abc9` techmapping. Doing so eliminates
+ the possibility of a strongly-connected component (i.e. a combinatorial loop)
+ existing. Typically, this is specified for sequential inputs on otherwise
+ combinatorial boxes -- for example, applying ``abc_scc_break`` onto the `D`
+ port of a LUTRAM cell prevents `abc9` from interpreting any `Q` -> `D` paths
+ as a combinatorial loop.
+
+- The port attribute ``abc_carry_in`` and ``abc_carry_out`` attributes mark
+ the carry-in and carry-out ports of a box. This information is necessary for
+ `abc9` to preserve the integrity of carry-chains.
+
Non-standard or SystemVerilog features for formal verification
==============================================================