Control intensive ICs pose a significant challenge to
	the users of formal methods in designing hardware.
These ICs have to support a wide variety of requirements
	including synchronous and asynchronous operations,
	polling and interrupt-driven modes of operation,
	multiple concurrent threads of execution,
	non-trivial computational requirements, and programmability.
In this paper, we illustrate the use of formal methods 
	in the design of a control intensive IC
	called the ``Intel 8251'' Universal Synchronous/Asynchronous
	Receiver/Transmitter (USART),
	using our hardware description language `hopCP'.
A feature of hopCP is that it supports 
	communication via {\em asynchronous ports} 
	in addition to {\em synchronous} message passing.
Asynchronous ports are
	distributed shared variables writable by exactly one process.
We show the usefulness of this combination of communication constructs.
We outline algorithms
	to determine safe usages of 
	asynchronous ports, and also to discover
	other static properties of the specification.
We discuss a compiled-code concurrent functional simulator
	called {\sc CFSIM},
	as well as the use of {\em concurrent testers} for driving CFSIM.
The use of a semantically well specified and simple language,
	and the associated analysis/simulation tools
	helps conquer the complexity of specifying and validating
	control intensive ICs.