Two years ago the ultra fine grained formal model for reconfigurable computing called the Synchronic A-Ram was introduced, which has unit time propagation delay between any two locations in memory. Formal models are abstracted from physical considerations, and usually have some characteristic that is physically implausible: the Turing machine performs instruction fetch in unit time regardless of the size of the instruction table, and lambda calculus performs beta reduction in one step regardless of the length of the expression.
Propagation delay may be introduced into the Synchronic A-Ram descriptions of FPGAs however, if the physical components of real architectures; logic blocks, switch blocks and wire segments etc are accurately represented in terms of the modelís fine grained primitive instructions. The amount of time required for a signal to pass through a succession of FPGA wire segments will be reflected in a Synchronic A-Ram program that accurately describes the wire segments, without any modification to the model.
Data transfer from one end of an FPGA wire segment to the other occurs in constant time, which would correspond to the constant time for the transfer of that wire segment in the Synchronic A-ram model. Consequently there is the prospect of the formalization of timing and logic operations in FPGA architectures in terms of a simple semantic model, and a formal basis for comparing them. To achieve that formalization however, access would be required to sufficiently detailed description down to the logic gate level of the architectures offered by Xilinx, Altera, Lattice Semi etc..
May I ask if anyone knows of some public repository where such descriptions are easily available without having to trawl through patent libraries, or is it the case that some aspects of designs are considered too commercially sensitive to reveal?