Formale Sprachen fuer Pipelining

[Martin S. (strubi)]

Moin,

komplexe Pipelines machen bekanntlich in klassischer HDL keinen Spass, 
deswegen der Ruf nach uebergeordneten Formalismen, die a) Beschreibung 
vereinfachen b) formale Verifikation (automatisch) erlauben.

Also im Prinzip das, was ein aufwendiger DSP-Compiler bereits macht, 
aber mit feinkoernigerer Kontrolle, dass es mit beliebigem Resourcen-Set 
- sprich FPGA funktioniert (und das bitte abseits C -> HDL-Ansaetzen).

Im Grunde genommen ist der Workflow momentan so:
- Berechnungsformel/Datenzugriffsmethode als Prototyp programmieren
- Mit bitgenauen (fixpoint)-Datentypen erweitern
- Ausgabe in eine Zwischendarstellung einer Pipeline
- Analyse/Verifikation, Latency-Matching verzahnter Pipelines
- Synthese/Ausgabe in HDL aus der Zwischenform

Fuer einfache Vorwaertsberechnungen ist das recht "straightforward", 
schwieriger wirds bei Rekursionen wie allgemeinen IIR, wo man die 
Pipeline nicht beliebig tief machen kann (wegen Feedback des Resultats 
in einer spaeteren Stufe in eine fruehere Stufe).
Da benoetigt es zusaetzliche Formalismen, um allfaellig noetige 
vorwaertsschauende Logik (Stichwort "lookahead") zu generieren.

Ist jemandem noch neben den Scala/Haskell/PipelineC-basierenden 
Ansaetzen noch eine Zwischenform (lesbar, also weniger LLVM-%-dekoriert) 
bekannt, mit der man effektiv arbeiten kann, heisst, dass laufende 
Verifikationen bei der Umstellung der Pipeline automatisch vonstatten 
gehen koennen?