Scope

ff-spartan6 formalizes the construction, validation, and execution of digital designs for the Spartan-6 FPGA family. Its architecture and primitive layers cover lookup tables, carry chains, registers, memories, clocks, input/output resources, and the DSP48A1 arithmetic block. Its netlist development represents expressions as stable directed acyclic graphs, admits raw designs into checked forms, and normalizes combinational, registered, mixed, and scheduled circuits. Hierarchy modules model components, interfaces, feedback, provenance, resources, and the passage from composed designs to flat machines. A further semantics and validation layer connects executable state machines and traces with profile, port, parameter, cycle, and design checks, while import modules account for Yosys-derived artifacts.

Most important results

The library provides checked builders and associated soundness developments for carry chains, differential output buffers, and multiple normalized circuit forms. Certified flattening modules relate hierarchical composition, feedback, and resource pairing to flat designs while preserving provenance. Machine, simulation, refinement, equivalence, invariant, and trace modules give the modeled circuits an explicit behavioral account. Yosys JSON import, generated fixtures, worked examples, and regression workloads connect that formal account to realistic netlists and representative FPGA designs.