Skip to content

Commit

Permalink
moving more pieces over
Browse files Browse the repository at this point in the history
  • Loading branch information
@nbingham1
nbingham1 committed Sep 25, 2024
1 parent ac65287 commit 35f92fb
Show file tree
Hide file tree
Showing 4 changed files with 232 additions and 221 deletions.
243 changes: 23 additions & 220 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,21 +4,31 @@ Loom is a collection of tools for the design and verification of
asynchronous circuits. Not all of the tools are complete.

## Table of Contents
1. [Status of Tools](#status)
2. [Build](#build)
3. [Language Reference](#reference)
4. [Usage](#usage)
1. [Circuit Synthesis](#synthesis)
2. [Circuit Simulation](#simulation)
3. [Visualization](#visualization)
5. [Examples](#examples)
6. [Syntax Documentation](#syntax)
1. [Internal Representation of State](#state)
2. [Reset Behavior](#reset)
3. [Limited Non-Proper Nesting](#nesting)
1. [Example](#example)
3. [Build](#build)
2. [Development Status](#status)
4. [Language Reference](#reference)

<a name="example"></a>
## Example

<a name="build"></a>
## Build

```
sudo apt install ninja-build libqhull-dev libgraphviz-dev
git submodule update --init --recursive
make
```

To generate test binaries and then run the tests
```
make test
make check
```

<a name="status"></a>
## Status of Tools
## Development Status

### Synthesis
* **Templating (0%)** parameterize your module specifications.
Expand Down Expand Up @@ -67,21 +77,6 @@ asynchronous circuits. Not all of the tools are complete.
* **Waveforms (100%)** Export to VCD for viewing in GTKWave.
* **Event Rule (0%)** Debug your system using an event rule representation instead of waveforms.

<a name="build"></a>
## Build

```
sudo apt install ninja-build libqhull-dev libgraphviz-dev
git submodule update --init --recursive
make
```

To generate test binaries and then run the tests
```
make test
make check
```

<a name="reference"></a>
## Language Reference
[Quasi-Delay Insensitive Circuits](https://en.wikipedia.org/wiki/Quasi-delay-insensitive_circuit)
Expand Down Expand Up @@ -157,198 +152,6 @@ R.f-,R.t-,L.e+; [R.e&~L.f&~L.t];
R.e+; [~R.f&~R.t]; *[[R.f|R.t]; R.e-; [~R.f&~R.t]; R.e+])'1
```

<a name="synthesis"></a>
### Circuit Synthesis

Synthesize the production rules that implement the behavioral description.

**Usage:** `lm [options] <file>`

**Options:**
- `--no-cmos` uses bubble reshuffling instead of state variables to make the production rules cmos implementable, combine with `--rules` to avoid cmos implementability altogether.
- `--all` save all intermediate stages
- `-o,--out` set the filename prefix for the saved intermediate stages
- `-g,--graph` save the elaborated astg
- `-c,--conflicts` print the conflicts to stdout
- `-e,--encode` save the complete state encoded astg
- `-r,--rules` save the synthesized production rules
- `-b,--bubble` save the bubble reshuffled production rules
- `-s,--size` save the sized production rules

**Supported file formats:**
- `*.chp` communicating hardware processes
- `*.hse` handshaking expansions
- `*.prs` production rules
- `*.astg` asynchronous signal transition graph
- `*.spi` spice netlist

If you just want to generate the final circuit, simply run the following command:

```
lm wchb1b.hse
```

This is the generated production rule set.
```
v0->R.f-
~v0->R.f+
v1->R.t-
~v1->R.t+
R.t|R.f->L.e-
~R.f&~R.t->L.e+
v2->L.f'1-
~v2->L.f'1+
v3->L.t'1-
~v3->L.t'1+
R.t'1|R.f'1->R.e'1-
~R.f'1&~R.t'1->R.e'1+
R.e&L.f&_Reset->v0-
~R.e&~L.f|~_Reset->v0+
R.e&L.t&_Reset->v1-
~R.e&~L.t|~_Reset->v1+
L.e'1&v3&_Reset->v2- {v3}
~L.e'1|~v3|~_Reset->v2+
L.e'1&v2&_Reset->v3- {v2}
~L.e'1|~v2|~_Reset->v3+
```

This will print the production rules out on the console. If you want to see all of the intermediate steps, run this:

```
lm --all --out wchb1b wchb1b.hse
```

This will save the elaborated state space to `wchb1b_predicate.astg`, save the
complete state coded state space to `wchb1b_complete.astg`, and the final
production rules in `wchb1b.prs`. It will also display the set of state
conflicts found on the original specification to the console.

For example, this is what `wchb1b_complete.astg` looks like:
```
.model hse
.internal R.f R.t L.e R.e L.f L.t L.f'1 L.t'1 L.e'1 R.e'1 R.f'1 R.t'1 v0 v1 v2 v3
.predicate
p0 ~R.f&~R.t&L.e&~L.t&v0&v1|~R.f&~R.t&L.e&~L.f&L.t&v0&v1
p1 R.f&~R.t&~L.e&~L.t&~v0&v1
p2 R.f&~R.t&L.e&L.f&~L.t&~v0&v1|~R.f&R.t&L.e&~L.f&L.t&v0&~v1
p3 ~R.f&~R.t&~L.e&~L.f&~L.t&v0&v1|~R.f&R.t&~L.e&~R.e&~L.f&~L.t&v0&v1|~R.f&R.t&~L.e&~L.f&v0&~v1
p4 ~R.f&~R.t&~L.e&~L.f&~L.t&v0&v1|R.f&~R.t&~L.e&~L.t&~v0&v1|R.f&~R.t&~L.e&~R.e&~L.f&~L.t&v0&v1
p5 L.f'1&~L.t'1&~v2&v3
p6 ~L.f'1&L.t'1&v2&~v3|~L.f'1&~L.t'1&v2&v3|~L.f'1&L.t'1&~L.e'1&v2&v3
p7 ~L.f'1&~L.t'1&v2&v3|L.f'1&~L.t'1&~L.e'1&v2&v3|L.f'1&~L.t'1&~v2&v3
p8 R.e'1&~R.f'1|R.e'1&R.f'1&~R.t'1
p9 ~R.e'1&~R.f'1|~R.e'1&R.f'1&~R.t'1
p10 ~R.f&R.t&~L.e&~L.f&v0&~v1
p11 ~L.f'1&L.t'1&v2&~v3
p12 ~R.f&~R.t&L.e&R.e&L.f&~L.t&~v0&v1
p13 R.f&~R.t&~L.e&~R.e&~L.f&~L.t&v0&v1
p14 ~R.f&~R.t&L.e&R.e&~L.f&L.t&v0&~v1
p15 ~R.f&R.t&~L.e&~R.e&~L.f&~L.t&v0&v1
p16 ~L.f'1&~L.t'1&L.e'1&~v2&v3
p17 L.f'1&~L.t'1&~L.e'1&v2&v3
p18 ~L.f'1&~L.t'1&L.e'1&v2&~v3
p19 ~L.f'1&L.t'1&~L.e'1&v2&v3
.effective
p0 ~R.f&~R.t&L.e&~L.f&~L.t&v0&v1|~R.f&~R.t&L.e&~R.e&L.f&~L.t&v0&v1|~R.f&~R.t&L.e&~R.e&~L.f&L.t&v0&v1
p1 R.f&~R.t&~L.e&R.e&~L.t&~v0&v1|R.f&~R.t&~L.e&~R.e&L.f&~L.t&~v0&v1
p3 ~R.f&R.t&~L.e&~L.f&v0&~v1|~R.f&R.t&~L.e&~R.e&~L.f&~L.t&v0&v1
p4 R.f&~R.t&~L.e&~L.t&~v0&v1|R.f&~R.t&~L.e&~R.e&~L.f&~L.t&v0&v1
p5 L.f'1&~L.t'1&L.e'1&~v2&v3
p6 ~L.f'1&L.t'1&v2&~v3|~L.f'1&~L.e'1&v2&v3
p7 L.f'1&~L.t'1&~v2&v3|~L.t'1&~L.e'1&v2&v3
p8 R.e'1&~R.f'1&~R.t'1
p9 ~R.e'1&R.f'1&~R.t'1|~R.e'1&~R.f'1&R.t'1
p10 ~R.f&R.t&~L.e&~L.f&L.t&v0&~v1|~R.f&R.t&~L.e&R.e&~L.f&~L.t&v0&~v1
p11 ~L.f'1&L.t'1&L.e'1&v2&~v3
.graph
1->R.f+/0 p2
1->R.t+/1 p2
1->L.e-/2 p1 p10
1->R.f-/3 p3
1->R.t-/4 p4
1->L.e+/5 p0
1->L.f'1+/6 p5 p11
1->L.t'1+/7 p5 p11
1->L.f'1-/8 p6
1->L.t'1-/9 p7
R.f'1|R.t'1->R.e'1-/10 p9
~R.f'1&~R.t'1->R.e'1+/11 p8
R.e&L.f->v0-/12 p12
~R.e&~L.f&~L.t->v0+/13 p13
R.e&L.t->v1-/14 p14
~R.e&~L.f&~L.t->v1+/15 p15
L.e'1->v2-/16 p16
~L.e'1->v2+/17 p17
L.e'1->v3-/18 p18
~L.e'1->v3+/19 p19
p0 R.e&L.f->v0-/12 R.e&L.t->v1-/14
p1 ~R.e&~L.f&~L.t->v0+/13
p2 1->L.e-/2
p3 1->L.e+/5
p4 1->L.e+/5
p5 ~L.e'1->v2+/17
p6 L.e'1->v2-/16 L.e'1->v3-/18
p7 L.e'1->v2-/16 L.e'1->v3-/18
p8 R.f'1|R.t'1->R.e'1-/10
p9 ~R.f'1&~R.t'1->R.e'1+/11
p10 ~R.e&~L.f&~L.t->v1+/15
p11 ~L.e'1->v3+/19
p12 1->R.f+/0
p13 1->R.f-/3
p14 1->R.t+/1
p15 1->R.t-/4
p16 1->L.f'1+/6
p17 1->L.f'1-/8
p18 1->L.t'1+/7
p19 1->L.t'1-/9
.arbiter {p6 p7}
.marking {[R.f-,R.t-,L.e+,R.e+,L.f-,L.t-,L.f'1-,L.t'1-,L.e'1+,R.e'1+,R.f'1-,R.t'1-,v0+,v1+,v2+,v3+] p0 p8 p7 p6}
.end
```

This command also accepts `*.spi` files for automated cell layout.

```
lm nand.spi sky130.py
klayout nand.gds &
```

See [sky130.py](https://github.com/broccolimicro/floret/blob/main/tech/sky130.py)

<a name="visualization"></a>
### Visualization

Create visual representations of the circuit or behavior.

**Usage:** `lm plot [options] file...`

**Options:**
- `-o` Specify the output file name, formats other than 'dot' are passed onto graphviz dot for rendering
- `-l,--labels` Show the IDs for each place, transition, and arc
- `-lr,--leftright` Render the graph from left to right
- `-e,--effective` Show the effective encoding of each place
- `-p,--predicate` Show the predicate of each place
- `-r,--raw` Do not post-process the graph
- `-s,--sync` Render half synchronization actions

Use the following command to show the elaborated state space from the generated astg.

```
lm plot -p wchb1b_predicate.astg -o wchb1b.png
```

Use this command to show the labels associated with every place, transition, and arc.

```
lm plot -l wchb1b.hse -o wchb1b.png
```

Use the following command to show the elaborated state space of the complete state coding.

```
lm plot -p wchb1b_complete.astg -o wchb1b.png
```

<a name="examples"></a>
## Examples

Expand Down
Loading

0 comments on commit 35f92fb

Please sign in to comment.