The Orangepath project supports various internal synthesis engines. The aim is to include SSMG but some more simple engines are also provided. The other engines include the FSM generator, the PSL compiler and the restructurer.
Because all input is converted to the HPR machine and all output is from that internal form it is sensible to use the HPR library for translation purposes without doing any actual synthesis.
A synthesis engine rewrites one HPR machine as another.
The H2 front end tool allows access to the live path interface synthesiser.
The A* version is described on this web page. http://www.cl.cam.ac.uk/ djg11/wwwhpr/gpibpage.html
The follow-on to this work is being undertaken by MJ Nam.
The transactor synthesiser is described on this link
http://www.cl.cam.ac.uk/research/srg/han/hprls/orangepath/transactors
The H1 tool implements an asynchronous logic synthesiser described on this link.
http://www.cl.cam.ac.uk/ djg11/wwwhpr/dsasynch.html
The H1 tool implements a SAT-based logic synthesiser described on this link.
http://www.cl.cam.ac.uk/ djg11/wwwhpr/dslogic.html
(This synthesiser is currently not part of the main HPR revision control branch.)
The HPR tool contains a synthesiser/generator for synchronous FSMs that converts a program in the HPR imperative language in to a finite state machine. The language contains assignments, conditional gotos, fork/join and leaf calls to HPR library functions.
The input and output to the FSM generation process are HPR machines. The output machine uses the so-called XRTL style that is readily converted to Verilog RTL by a subsequent stage.
An additional input, from the command line, is an unwind budget: a number of basic blocks to consider in any loop unwind operation. Where loops are nested or fork in flow of control, the budget is divided amongs the various ways.
Minor changes in the operation of FSM synthesiser are controlled with the -synthcontrol command line option. The sequencer for a thread can be unpacked, normal or one-hot. Unpacked is selected with sequencer:unpacked.
Minor changes in the operation of FSM synthesiser are controlled with the -synthcontrol command line option. The sequencer for a thread can be unpacked, normal or one-hot.
The string preserve-sequencer should be supplied to keep the per-thread vestigal sequencer in RTL output structures. This makes the output code more readable but can make it less compact for synthesis, depending on the capabilites of the FPGA tools to do their own minimisation.
The string resets:synchronous should be passed in to introduce synchronous resets to the generated sequencer logic. This is the default.
The string resets:asynchronous should be passed in to introduce assynchronous resets to the generated sequencer logic.
The string resets:none should be passed in to supress reset logic for FPGA targets. FPGA's tend to have built-in, dedicated reset wiring.
-synthcontrol 'preserve-sequencer;resets:none;sequencer:packed'
The central data structure is the pending activation queue, where an activation consists of a program counter name, program counter value and environment mapping variables that have so far been changed to their new (symbolic) values.
The output is a list of finite-state-machine edges that are finally placed inside a single HPR parallel construct. The edges have to forms (g, v, e) (g, fname, [ args]) where the first form assigns e to v when g holds and the second calls function fname when g holds.
Both the pending activation queue and the output list have checkpoint annotations so that edges generated during a failed attempt at a loop unwind can be discarded.
The pending activation list is initialised with the entry points for each thread. Operation removes one activation and symbolically steps it through a basic block of the program code, at which time zero, one or two activations are returned. These are either added to the output list or to the pending activation list. An exit statement terminates the activation and a basic block terminating in a conditional branch returns two activations. A basic block is terminated with a single activation at a blocking native call, such as hpr_pause. When returned from the symbolic simulator, the activation may be flagged as blocking, in which case it is fed to the output queue. Otherwise, if the unwind budget is not used up the resulting activations are added to the pending queue.
A third queue records successfully processed activations. Activations are discarded and not added to the pending queue if they have already been successfully processed. Checking this requires comparison of symbolic environments. These are kept in a "close to normal form" form so that syntactic equivalence can be used. This list is also subject to rollback.
Operation continues until the pending activation queue is empty. A powerful proof engine for comparing activations would enable this condition to be checked more fully and avoid untermination with a greater number of designs.
The PSL synthesiser converts PSL temporal assertions into FSM-based runtime monitors.
The Sys-ML statechart synthesiser is built in to the front end of the H2 tool. It must be built in to other front ends that generate HPR VMs,
SSMG is the main refinement component that converts assertions to executable logic using goal-directed search. The SSMG synthesiser is described in a separate document and is a complete sub-project with respect to HPR.
The RTL-style machines can be restructured, so that different operations occur in different cycles, with automatic insertion of holding registers to maintain data values that would not be available when needed.
Restructuring is need to avoid structural hazards arising when an ALU or multiplier is not fully-pipeline or when a memory has insufficient ports for the level of concurrent access required.
