SpeCuLog is a language for specifying logical circuits.
Circuits are specified by there inputs, outputs and registers and logical constraints that link them.
Then our tool synthesizes an AIGER file that meets this constraints when it is possible.
If it is not then it gives the valuation of inputs and registers for which the constraints cannot be met by the outputs and updates of the registers.
Speculog can be downloaded from the following
link.
The archive provides scripts to install ocaml-cudd and ocaml-aiger that are necessary to run speculog.
Once this tool library are installed, enter the directory
speculog and run the command
make this should build the neccessary executable.
To check that everything works, try the command
make test.
Speculog is a tool to generate AIGER files.
Speculog can also be used as an Ocaml library that provides all the necessary functions to generate AIGER files.
A syntax extension for Ocaml is also in also in development.
We here describe how to write with this syntax extension.
Variable Declaration and Types
Variables must be declared together with their types.
Apart from the classical Booleans and (unsigned) integers the user can also use 3 different kinds of types in conjunction:
- Arrays: var arr : (int 8)[4]; declares a variable arr which is an array of 4 integers of 8 bits each.
- Records: var rec : { x : int 8; y : int 8 }; declares a variable rec wich is a record with a field x and a field y both integers of 8 bits.
- Union: var signed : Pos of (int 4) | Neg of (int 3); declares a variable signed which is either a 4 bit integer constructed with Pos or a 3 bit integers constructed with Neg.
The
i-th element of an array
arr is accessed by
arr[i].
The field
x of a record
rec is accessed by
rec.x.
Access to union variables is through pattern matching, look for instance at the following example that increments a signed integer:
match signed with
| Pos x -> Pos (x+1)
| Neg x -> if x = 0 then Pos 1 else Neg (x - 1)
Expressions
Speculog supports the following expressions.
- Boolean operations,
negation:
! e
implication:
e --> f
equivalence:
e <-> f
conjunction:
e & f
disjunction:
e || f
xor:
e ^ f
-
Integer comparisons,
e = f ,
e < f ,
e >= f ,
e <= f ,
e > f
-
Integer operations,
e + f ,
e - f ,
e * f ,
e / f ,
e mod f
-
Conditional: if e then f else g
Synthesis
A circuit specification is a list of variable declarations followed by a serie of instruction that describe how the variables should be updated.
The updates are described in this way:
v <- e ; where
v is a variable and
e an expression.
It can optionally contain a description of how the variables should be initialized, in that case we use the keywords
init and
updates respectively to define the initial configuration and the updates respectively.
Full Example
Here is a small example of a speculog file available in
examples/ex1.spec to demonstrate the basic use of speculog.
var request : bool;
var state : ready | busy;
init state <- ready;
updates state <- if state = ready & request then busy else ready;
To synthesize a circuit from this file, run the command
./speculogSynth.byte examples/ex1.spec.
This prints on the standard output an AIGER file corresponding to this specification.
By redirecting the output to a file
ex1.aig (
./speculogSynth.byte examples/ex1.spec >ex1.aig),
we can then simulate the execution of the circuit using the simulation tool:
./simulation.byte ex1.aig.
For more examples, have a look at the
examples directory of Speculog.
Speculog can also be used as an OCaml library to write Aiger files.
For an example see the file
robots.ml in the example directory.
You can also consult the
API.
For remarks or questions please contact
Romain Brenguier.