Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,14 @@ jobs:
run: cabal run gatework -- --netlist fixtures/tco.net --duration 22 --output /tmp/tco.vcd --set d=1 --at 4 d=0 --at 8 d=1 --at 14 rst=1 --at 16 rst=0
- name: Compare the clock-to-output delay demo with the golden file
run: diff fixtures/tco.golden.vcd /tmp/tco.vcd
- name: Run the buffer demo
run: cabal run gatework -- --netlist fixtures/buffer.net --duration 8 --output /tmp/buffer.vcd --set d=0 --at 2 d=1 --at 4 d=0 --at 6 d=z
- name: Compare the buffer demo with the golden file
run: diff fixtures/buffer.golden.vcd /tmp/buffer.vcd
- name: Run the MUX demo
run: cabal run gatework -- --netlist fixtures/mux.net --duration 10 --output /tmp/mux.vcd --set d0=0,d1=1,sel=0 --at 2 sel=1 --at 4 sel=x --at 6 d0=1,d1=1 --at 8 sel=z
- name: Compare the MUX demo with the golden file
run: diff fixtures/mux.golden.vcd /tmp/mux.vcd
- name: Confirm a missing library file stops the run
run: |
if cabal run gatework -- --netlist fixtures/libadder.net --library fixtures/missing.net --duration 0 --output /tmp/none.vcd 2>/tmp/none.log; then
Expand Down
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ dist-newstyle/
*.dyn_o
*.vcd
!fixtures/*.golden.vcd
*.report
!fixtures/*.golden.report
.haskell-tools/
.stack-work/
.idea/
Expand Down
31 changes: 31 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,37 @@ All notable changes to Gatework appear in this file.
The format follows the Keep a Changelog convention.
This project uses semantic versioning.

## [0.17.0.0] - 2026-08-04

### Added

- Add the `MUX` gate with `(d0,d1,sel)` inputs.
- Select `d0` when `sel` is low.
- Select `d1` when `sel` is high.
- Resolve an unknown selector to the common branch value when both branches agree.
- Convert floating selected data to unknown.
- Support `MUX` on buses, modules, and delayed gate paths.
- Add a multiplexer waveform fixture, golden VCD, deterministic tests, and a QuickCheck property.

### Fixed

- Add the missing final newline to the buffer golden VCD.
- Bump the package version to 0.17.0.0.

## [0.16.0.0] - 2026-08-04

### Added

- Add the `BUF` gate for non-inverting signal transfer.
- Pass low, high, and unknown values through `BUF`.
- Convert floating `z` input to unknown `x` inside `BUF`.
- Support `BUF` on buses, modules, and delayed gate paths.
- Add a buffer waveform fixture, golden VCD, deterministic tests, and a QuickCheck property.

### Changed

- Bump the package version to 0.16.0.0.

## [0.15.0.0] - 2026-08-04

### Added
Expand Down
127 changes: 122 additions & 5 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,8 @@ You can do these tasks:
- Watch a flip-flop output commit after its clock-to-output delay.
- Capture data at the clock edge, not at the commit time.
- Delay an asserted reset by the same amount.
- Use a non-inverting `BUF` gate for known and unknown signal paths.
- Select data with a three-input `MUX` gate.

## Architecture

Expand Down Expand Up @@ -322,6 +324,67 @@ The run reports a pass only when every assertion holds.
| 4 | 1 | 0 | 1 | 0 | 0 |
| 6 | 0 | 0 | 1 | 1 | 1 |

## Buffer gate demo

Run a direct buffer and a delayed buffer.

```powershell
cabal run gatework -- --netlist fixtures/buffer.net --duration 8 --output buffer.vcd --set d=0 --at 2 d=1 --at 4 d=0 --at 6 d=z
```

The command writes this output:

```text
Wrote buffer.vcd
Signals: 3
Duration: 8 time units
Assertions: 9 passed
```

`BUF` passes low, high, and unknown values.
It maps a floating `z` input to `x`, because ordinary gates read floating inputs as unknown.
The delayed instance applies the existing gate delay rules.

| Time | d | y | delayed |
| --- | --- | --- | --- |
| 0 | 0 | 0 | 0 |
| 2 | 1 | 1 | 0 |
| 4 | 0 | 0 | 1 |
| 6 | z | x | 0 |
| 8 | z | x | x |

## Multiplexer gate demo

Run the multiplexer demo.

```powershell
cabal run gatework -- --netlist fixtures/mux.net --duration 10 --output mux.vcd --set d0=0,d1=1,sel=0 --at 2 sel=1 --at 4 sel=x --at 6 d0=1,d1=1 --at 8 sel=z
```

The command writes this output:

```text
Wrote mux.vcd
Signals: 5
Duration: 10 time units
Assertions: 9 passed
```

`MUX` uses `(d0,d1,sel)` input order.
A low selector chooses `d0`.
A high selector chooses `d1`.
An unknown selector returns the common branch value when both branches agree.
A floating selected value becomes `x`.
The delayed instance shows the same behavior two time units later.

| Time | d0 | d1 | sel | y | delayed |
| --- | --- | --- | --- | --- | --- |
| 0 | 0 | 1 | 0 | 0 | 0 |
| 2 | 0 | 1 | 1 | 1 | 0 |
| 4 | 0 | 1 | x | x | 1 |
| 6 | 1 | 1 | x | 1 | x |
| 8 | 1 | 1 | z | 1 | 1 |

## Hierarchical adder demo

Run the hierarchical ripple-carry adder.
Expand Down Expand Up @@ -930,6 +993,31 @@ The output `q` commits to 1 at time 4.
The reset rises at time 14.
The output `q` stays 1 until the reset commit lands at time 16.

The file `fixtures/buffer.golden.vcd` holds the buffer demo waveform.
Its timeline shows direct transfer, delayed transfer, and floating-input handling:

```text
#0
0!
0"
0#
#2
1!
1"
#4
0!
0"
1#
#6
z!
x"
0#
#8
x#
```

Here `!` is `d`, `"` is `y`, and `#` is `delayed`.

## Netlist format

Use one declaration per line.
Expand All @@ -948,7 +1036,7 @@ gate AND combine (n,b) -> y
dff state clock=clk d=a q=state_q init=0
```

Supported gates are AND, OR, XOR, NAND, NOR, XNOR, NOT, and TRIBUF.
Supported gates are AND, OR, XOR, NAND, NOR, XNOR, NOT, BUF, MUX, and TRIBUF.
NAND, NOR, and XNOR use two inputs.
A gate output must have a `wire` or `output` declaration.
A flip-flop uses `clock=`, `d=`, and `q=` fields.
Expand All @@ -957,6 +1045,24 @@ It accepts an optional `tco=` clock-to-output delay field.
Flip-flop clocks must be declared `clock` signals.
Clock periods use even integers of at least two.

The `BUF` gate is a non-inverting buffer.
It passes low, high, and unknown values.
It converts a floating `z` input to unknown `x`.

```text
gate BUF pass (d) -> y
```

The `MUX` gate selects one of two data inputs.
Its first input is `d0`.
Its second input is `d1`.
Its third input is `sel`.
A low selector selects the first input.
A high selector selects the second input.
An unknown selector compares the normalized data values.
Equal values pass through.
Different values produce `x`.

The `TRIBUF` gate is a tri-state buffer.
Its first input is the data signal.
Its second input is the enable signal.
Expand Down Expand Up @@ -1252,6 +1358,7 @@ Deterministic tests also cover gate delay parsing and invalid delay fields.
Deterministic tests also cover delayed transitions, delay accumulation, zero-delay behavior, multi-driver delays, and the initial settle.
Deterministic tests also cover rise and fall delay parsing, conflict rules, direction-specific transitions, and the asymmetric delay demo.
Deterministic tests also cover clock-to-output delay parsing, invalid tco fields, delayed commits, edge capture, delayed reset, wide register commits, and the golden output.
Deterministic tests also cover BUF and MUX truth values, bus behavior, delayed paths, and their golden outputs.
QuickCheck properties cover gate algebra, full adder correctness, scheduled input sampling, reset sampling, register width, and assertion soundness.
QuickCheck properties also compare the hierarchical adder and counter with their flat versions.
QuickCheck properties also cover the four-state model and the tri-state buffer truth table.
Expand All @@ -1264,6 +1371,7 @@ QuickCheck properties also compare a clock-to-output flip-flop with a delayed re
QuickCheck properties also compare the counter report with the simulated waveform.
QuickCheck properties also compare whole-bus input values with per-bit reference values.
QuickCheck properties also compare every VCD vector value with the per-bit waveform.
QuickCheck properties also cover BUF behavior and MUX selection across all four logic values.

QuickCheck runs one hundred random cases for each property.
The gate properties cover the complete truth table.
Expand All @@ -1275,7 +1383,9 @@ The entry-point property shows that both simulation entry points produce identic
The assertion property shows that real values pass and inverted values fail.
The hierarchy property shows that the hierarchical circuits match the flat circuits.
The four-state property shows that the gates keep their two-state behavior for known inputs.
The buffer properties show that an enabled buffer passes data and a disabled buffer floats.
The tri-state buffer property shows that an enabled driver passes data and a disabled driver floats.
The BUF property shows that direct transfer preserves known values and maps floating input to unknown.
The MUX property shows that an unknown selector passes equal branches and rejects different branches.
The bus XOR property compares a bus gate with per-bit evaluation.
The bus register property compares each register bit with a reference value.
The bus hierarchy property shows that a bus module matches its flat circuit.
Expand All @@ -1288,8 +1398,9 @@ The asymmetric-delay property compares each output sample with the directional r

## Test status

All tests pass on GHC 9.6.7 with Cabal 3.14 in the bundled container.
The CI workflow runs the same checks on Ubuntu with GHC 9.6.6.
The previous release passed on GHC 9.6.7 with Cabal 3.14 in the bundled container.
This workspace could not run Cabal because the executable is unavailable.
The CI workflow runs the checks on Ubuntu with GHC 9.6.6.
Golden tests compare each fixture VCD with its golden file.
The golden report test compares the counter report table with its golden file.
CI runs every demo and compares its output with the golden file.
Expand All @@ -1299,13 +1410,17 @@ CI runs the four-state vector demo and compares it with its golden file.
CI runs the gate delay demo and compares it with its golden file.
CI runs the asymmetric delay demo and compares it with its golden file.
CI runs the clock-to-output delay demo and compares it with its golden file.
CI runs the buffer demo and compares it with its golden file.
CI runs the MUX demo and compares it with its golden file.
CI confirms that a missing library file stops the run.
CI confirms that an invalid gate delay stops the run.

## Limitations

The simulator uses four logic values: low, high, unknown, and floating.
A floating value reads as unknown inside a gate.
The BUF gate preserves low, high, and unknown values.
The MUX gate returns `x` when an unknown selector chooses different branches.
Several gates can drive one wire.
The simulator resolves the driver values into one wire value.
Resolution treats z as neutral and known values as dominant.
Expand Down Expand Up @@ -1359,6 +1474,8 @@ The report prints every signal in the stable signal order.

## Roadmap

Release 0.17.0.0 completed the MUX gate and its waveform evidence.
Release 0.16.0.0 completed the BUF gate and its waveform evidence.
Release 0.15.0.0 completed the clock-to-output delay for flip-flops.
Release 0.14.0.0 completed separate rise and fall gate delays.
Release 0.13.0.0 completed configurable gate delays.
Expand All @@ -1376,7 +1493,7 @@ Release 0.2.0.0 completed scheduled input transitions.

Remaining work:

1. Add a buffer gate to the gate library.
1. Expand the gate library with additional circuit primitives.

## License

Expand Down
2 changes: 1 addition & 1 deletion fixtures/adder.golden.vcd
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ $date
generated deterministically by gatework
$end
$version
gatework 0.15.0.0
gatework 0.17.0.0
$end
$timescale 1ns $end
$scope module gatework $end
Expand Down
2 changes: 1 addition & 1 deletion fixtures/assert.golden.vcd
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ $date
generated deterministically by gatework
$end
$version
gatework 0.15.0.0
gatework 0.17.0.0
$end
$comment
assert y = 1 at 0
Expand Down
2 changes: 1 addition & 1 deletion fixtures/asymdelay.golden.vcd
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ $date
generated deterministically by gatework
$end
$version
gatework 0.15.0.0
gatework 0.17.0.0
$end
$comment
assert y = 1 at 0
Expand Down
41 changes: 41 additions & 0 deletions fixtures/buffer.golden.vcd
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
$date
generated deterministically by gatework
$end
$version
gatework 0.17.0.0
$end
$comment
assert y = 0 at 0
assert delayed = 0 at 0
assert y = 1 at 2
assert delayed = 0 at 2
assert y = 0 at 4
assert delayed = 1 at 4
assert y = x at 6
assert delayed = 0 at 6
assert delayed = x at 8
$end
$timescale 1ns $end
$scope module gatework $end
$var wire 1 ! d $end
$var wire 1 " y $end
$var wire 1 # delayed $end
$upscope $end
$enddefinitions $end
#0
0!
0"
0#
#2
1!
1"
#4
0!
0"
1#
#6
z!
x"
0#
#8
x#
17 changes: 17 additions & 0 deletions fixtures/buffer.net
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# A plain buffer preserves known values and reads floating input as unknown.
input d
output y
output delayed
wire y
wire delayed
gate BUF pass (d) -> y
gate BUF slow (d) -> delayed delay=2
assert y = 0 at 0
assert delayed = 0 at 0
assert y = 1 at 2
assert delayed = 0 at 2
assert y = 0 at 4
assert delayed = 1 at 4
assert y = x at 6
assert delayed = 0 at 6
assert delayed = x at 8
2 changes: 1 addition & 1 deletion fixtures/bus.golden.vcd
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ $date
generated deterministically by gatework
$end
$version
gatework 0.15.0.0
gatework 0.17.0.0
$end
$comment
assert x[0] = 1 at 0
Expand Down
2 changes: 1 addition & 1 deletion fixtures/counter.golden.vcd
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ $date
generated deterministically by gatework
$end
$version
gatework 0.15.0.0
gatework 0.17.0.0
$end
$timescale 1ns $end
$scope module gatework $end
Expand Down
2 changes: 1 addition & 1 deletion fixtures/delay.golden.vcd
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ $date
generated deterministically by gatework
$end
$version
gatework 0.15.0.0
gatework 0.17.0.0
$end
$comment
assert x = 1 at 0
Expand Down
Loading
Loading