diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 841c281..e81d4d7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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 diff --git a/.gitignore b/.gitignore index 2fae983..9d01073 100644 --- a/.gitignore +++ b/.gitignore @@ -5,6 +5,8 @@ dist-newstyle/ *.dyn_o *.vcd !fixtures/*.golden.vcd +*.report +!fixtures/*.golden.report .haskell-tools/ .stack-work/ .idea/ diff --git a/CHANGELOG.md b/CHANGELOG.md index 8f43dea..200e122 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/README.md b/README.md index fad869c..8c216f4 100644 --- a/README.md +++ b/README.md @@ -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 @@ -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. @@ -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. @@ -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. @@ -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. @@ -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. @@ -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. @@ -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. @@ -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. @@ -1299,6 +1410,8 @@ 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. @@ -1306,6 +1419,8 @@ CI confirms that an invalid gate delay stops the run. 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. @@ -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. @@ -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 diff --git a/fixtures/adder.golden.vcd b/fixtures/adder.golden.vcd index c32efb7..b920082 100644 --- a/fixtures/adder.golden.vcd +++ b/fixtures/adder.golden.vcd @@ -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 diff --git a/fixtures/assert.golden.vcd b/fixtures/assert.golden.vcd index 2189e75..4ea4a51 100644 --- a/fixtures/assert.golden.vcd +++ b/fixtures/assert.golden.vcd @@ -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 diff --git a/fixtures/asymdelay.golden.vcd b/fixtures/asymdelay.golden.vcd index 675f2bf..bb0b1c8 100644 --- a/fixtures/asymdelay.golden.vcd +++ b/fixtures/asymdelay.golden.vcd @@ -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 diff --git a/fixtures/buffer.golden.vcd b/fixtures/buffer.golden.vcd new file mode 100644 index 0000000..ae7d7e7 --- /dev/null +++ b/fixtures/buffer.golden.vcd @@ -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# diff --git a/fixtures/buffer.net b/fixtures/buffer.net new file mode 100644 index 0000000..dc58f2b --- /dev/null +++ b/fixtures/buffer.net @@ -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 \ No newline at end of file diff --git a/fixtures/bus.golden.vcd b/fixtures/bus.golden.vcd index d933094..6cea88b 100644 --- a/fixtures/bus.golden.vcd +++ b/fixtures/bus.golden.vcd @@ -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 diff --git a/fixtures/counter.golden.vcd b/fixtures/counter.golden.vcd index eaa139b..a383952 100644 --- a/fixtures/counter.golden.vcd +++ b/fixtures/counter.golden.vcd @@ -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 diff --git a/fixtures/delay.golden.vcd b/fixtures/delay.golden.vcd index 012b3c2..fcc7239 100644 --- a/fixtures/delay.golden.vcd +++ b/fixtures/delay.golden.vcd @@ -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 diff --git a/fixtures/gates.golden.vcd b/fixtures/gates.golden.vcd index 09c7768..7c09db4 100644 --- a/fixtures/gates.golden.vcd +++ b/fixtures/gates.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.17.0.0 $end $comment assert nand_out = 1 at 0 diff --git a/fixtures/haddader.golden.vcd b/fixtures/haddader.golden.vcd index d3e3ad9..afbb813 100644 --- a/fixtures/haddader.golden.vcd +++ b/fixtures/haddader.golden.vcd @@ -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 diff --git a/fixtures/hcounter.golden.vcd b/fixtures/hcounter.golden.vcd index 1f57be4..719bcf3 100644 --- a/fixtures/hcounter.golden.vcd +++ b/fixtures/hcounter.golden.vcd @@ -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 diff --git a/fixtures/libadder.golden.vcd b/fixtures/libadder.golden.vcd index d3e3ad9..afbb813 100644 --- a/fixtures/libadder.golden.vcd +++ b/fixtures/libadder.golden.vcd @@ -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 diff --git a/fixtures/mux.golden.vcd b/fixtures/mux.golden.vcd new file mode 100644 index 0000000..cffcb87 --- /dev/null +++ b/fixtures/mux.golden.vcd @@ -0,0 +1,46 @@ +$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 = x at 4 + assert delayed = 1 at 4 + assert y = 1 at 6 + assert delayed = x at 6 + assert delayed = 1 at 8 +$end +$timescale 1ns $end +$scope module gatework $end +$var wire 1 ! d0 $end +$var wire 1 " d1 $end +$var wire 1 # sel $end +$var wire 1 $ y $end +$var wire 1 % delayed $end +$upscope $end +$enddefinitions $end +#0 +0! +1" +0# +0$ +0% +#2 +1# +1$ +#4 +x# +x$ +1% +#6 +1! +1$ +x% +#8 +z# +1% diff --git a/fixtures/mux.net b/fixtures/mux.net new file mode 100644 index 0000000..f5880a7 --- /dev/null +++ b/fixtures/mux.net @@ -0,0 +1,19 @@ +# A multiplexer selects data and resolves equal branches when the selector is unknown. +input d0 +input d1 +input sel +output y +output delayed +wire y +wire delayed +gate MUX choose (d0,d1,sel) -> y +gate MUX slow (d0,d1,sel) -> 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 = x at 4 +assert delayed = 1 at 4 +assert y = 1 at 6 +assert delayed = x at 6 +assert delayed = 1 at 8 diff --git a/fixtures/reg2.golden.vcd b/fixtures/reg2.golden.vcd index 70d03af..94c5ffc 100644 --- a/fixtures/reg2.golden.vcd +++ b/fixtures/reg2.golden.vcd @@ -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 diff --git a/fixtures/register.golden.vcd b/fixtures/register.golden.vcd index 200b272..068bc93 100644 --- a/fixtures/register.golden.vcd +++ b/fixtures/register.golden.vcd @@ -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 diff --git a/fixtures/reset.golden.vcd b/fixtures/reset.golden.vcd index cccad76..d3c988c 100644 --- a/fixtures/reset.golden.vcd +++ b/fixtures/reset.golden.vcd @@ -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 diff --git a/fixtures/shared.golden.vcd b/fixtures/shared.golden.vcd index 96756a1..7b99122 100644 --- a/fixtures/shared.golden.vcd +++ b/fixtures/shared.golden.vcd @@ -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 = z at 0 diff --git a/fixtures/tco.golden.vcd b/fixtures/tco.golden.vcd index f84414e..ce97997 100644 --- a/fixtures/tco.golden.vcd +++ b/fixtures/tco.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.17.0.0 $end $comment assert q = 0 at 0 diff --git a/fixtures/tristate.golden.vcd b/fixtures/tristate.golden.vcd index 29cf0aa..c0a0eda 100644 --- a/fixtures/tristate.golden.vcd +++ b/fixtures/tristate.golden.vcd @@ -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 = z at 0 diff --git a/fixtures/unknown.golden.vcd b/fixtures/unknown.golden.vcd index 611b1e9..a4726a1 100644 --- a/fixtures/unknown.golden.vcd +++ b/fixtures/unknown.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.15.0.0 + gatework 0.17.0.0 $end $comment assert q = x at 0 diff --git a/fixtures/vector4.golden.vcd b/fixtures/vector4.golden.vcd index 3a91056..de9077e 100644 --- a/fixtures/vector4.golden.vcd +++ b/fixtures/vector4.golden.vcd @@ -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 diff --git a/gatework.cabal b/gatework.cabal index 7f0b98a..23d075d 100644 --- a/gatework.cabal +++ b/gatework.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: gatework -version: 0.15.0.0 +version: 0.17.0.0 synopsis: Event-driven digital logic simulation in Haskell description: Gatework parses typed netlists, runs combinational gates and D @@ -17,6 +17,8 @@ description: Buses render as multi-bit vectors in the VCD timeline. A gate can declare a delay with the delay=N field. A gate can declare separate rise and fall delays. + A one-input BUF gate transfers known values and maps floating input to unknown. + A three-input MUX gate selects one data input and resolves equal unknown branches. The scheduler delays each gate transition by the declared amount. A flip-flop can declare a clock-to-output delay with the tco=N field. The scheduler commits each flip-flop output after that delay. diff --git a/src/Gatework/Logic.hs b/src/Gatework/Logic.hs index 4dabde6..b28beab 100644 --- a/src/Gatework/Logic.hs +++ b/src/Gatework/Logic.hs @@ -14,7 +14,7 @@ import Data.List (foldl') data Logic = Low | High | Undefined | TriState deriving (Eq, Ord, Read, Show) -data GateType = And | Or | Xor | Not | Nand | Nor | Xnor | Tribuf +data GateType = And | Or | Xor | Not | Nand | Nor | Xnor | Buf | Mux | Tribuf deriving (Eq, Ord, Read, Show) gateArity :: GateType -> Int @@ -25,6 +25,8 @@ gateArity Not = 1 gateArity Nand = 2 gateArity Nor = 2 gateArity Xnor = 2 +gateArity Buf = 1 +gateArity Mux = 3 gateArity Tribuf = 2 parseGateType :: String -> Maybe GateType @@ -36,6 +38,8 @@ parseGateType value = case map toLower value of "nand" -> Just Nand "nor" -> Just Nor "xnor" -> Just Xnor + "buf" -> Just Buf + "mux" -> Just Mux "tribuf" -> Just Tribuf _ -> Nothing @@ -79,6 +83,12 @@ evalGate Xnor inputs evalGate Not inputs = case inputs of input : _ -> invert input [] -> Undefined +evalGate Buf inputs = case inputs of + [input] -> bufferValue input + _ -> Undefined +evalGate Mux inputs = case inputs of + [lowData, highData, select] -> muxValue lowData highData select + _ -> Undefined evalGate Tribuf inputs = case inputs of [dataValue, enable] -> tribufValue dataValue enable _ -> Undefined @@ -92,6 +102,22 @@ invert High = Low invert Undefined = Undefined invert TriState = Undefined +bufferValue :: Logic -> Logic +bufferValue TriState = Undefined +bufferValue value = value + +muxValue :: Logic -> Logic -> Logic -> Logic +muxValue lowData highData select = case select of + Low -> bufferValue lowData + High -> bufferValue highData + Undefined -> commonValue + TriState -> commonValue + where + commonValue = + let normalizedLow = bufferValue lowData + normalizedHigh = bufferValue highData + in if normalizedLow == normalizedHigh then normalizedLow else Undefined + tribufValue :: Logic -> Logic -> Logic tribufValue dataValue enable = case enable of Low -> TriState diff --git a/test/Spec.hs b/test/Spec.hs index 332809e..d718401 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -158,6 +158,14 @@ main = do deterministic <- sequence [ testParser , testParserAcceptsCommentsAndBlankLines + , testBufferTruth + , testBufferFixture + , testBufferBus + , testGoldenBufferVCD + , testMuxTruth + , testMuxFixture + , testMuxBus + , testGoldenMuxVCD , testParserRejectsUnknownGate , testParserRejectsWrongArity , testParserRejectsEmptyInputs @@ -343,6 +351,8 @@ main = do , ("four-state gates match the two-state reference", quickCheckResult propTwoStateMatchesReference) , ("undefined inputs commute in binary gates", quickCheckResult propUndefinedCommutative) , ("TRIBUF follows its truth table", quickCheckResult propTribufTruth) + , ("BUF follows its four-state truth table", quickCheckResult propBufferTruth) + , ("MUX follows its four-state selection table", quickCheckResult propMuxTruth) , ("an enabled buffer passes known data", quickCheckResult propTribufEnable) , ("tri-state fixture stays consistent", quickCheckResult (propTribufFixtureSound tristate)) , ("unknown fixture starts unclocked", quickCheckResult (propUnknownFixtureSampling unknown)) @@ -1123,6 +1133,146 @@ testNandNorXnorTruth = , evalGate Xnor [High, High] == High ] +testBufferTruth :: IO Bool +testBufferTruth = + check "BUF passes known values and maps floating input to unknown" $ + and + [ evalGate Buf [Low] == Low + , evalGate Buf [High] == High + , evalGate Buf [Undefined] == Undefined + , evalGate Buf [TriState] == Undefined + , evalGate Buf [] == Undefined + ] + +testBufferFixture :: IO Bool +testBufferFixture = do + source <- readFile "fixtures/buffer.net" + case parseNetlist source of + Left _ -> check "buffer fixture simulates delayed copies" False + Right netlist -> check "buffer fixture simulates delayed copies" $ case + simulateWithScheduledInputs netlist [ ("d", Low) ] + [(2, "d", High), (4, "d", Low), (6, "d", TriState)] 8 of + Right simulation -> + null (simulationFailures simulation) + && length (simulationAssertions simulation) == 9 + && valueAt simulation "y" 0 == Low + && valueAt simulation "y" 2 == High + && valueAt simulation "y" 6 == Undefined + && valueAt simulation "delayed" 2 == Low + && valueAt simulation "delayed" 4 == High + && valueAt simulation "delayed" 6 == Low + && valueAt simulation "delayed" 8 == Undefined + Left _ -> False + +testBufferBus :: IO Bool +testBufferBus = case parseNetlist (unlines + [ "input a[4]" + , "output y[4]" + , "wire y[4]" + , "gate BUF copy (a) -> y" + ]) of + Left _ -> check "BUF applies bitwise across a bus" False + Right netlist -> check "BUF applies bitwise across a bus" $ case + simulateWithInputs netlist (busInputs "a" 9 4) 0 of + Right simulation -> + valueAt simulation "y[0]" 0 == High + && valueAt simulation "y[1]" 0 == Low + && valueAt simulation "y[2]" 0 == Low + && valueAt simulation "y[3]" 0 == High + Left _ -> False + +testGoldenBufferVCD :: IO Bool +testGoldenBufferVCD = do + source <- readFile "fixtures/buffer.net" + golden <- readFile "fixtures/buffer.golden.vcd" + let actual = do + netlist <- parseNetlist source + simulation <- + simulateWithScheduledInputs netlist [ ("d", Low) ] + [(2, "d", High), (4, "d", Low), (6, "d", TriState)] 8 + pure (renderVCD simulation) + check "buffer VCD matches golden file" (actual == Right golden) + +testMuxTruth :: IO Bool +testMuxTruth = + check "MUX selects data and resolves equal unknown branches" $ + and + [ evalGate Mux [Low, High, Low] == Low + , evalGate Mux [Low, High, High] == High + , evalGate Mux [Low, High, Undefined] == Undefined + , evalGate Mux [High, High, Undefined] == High + , evalGate Mux [TriState, TriState, TriState] == Undefined + , evalGate Mux [TriState, High, Low] == Undefined + , evalGate Mux [Low, High] == Undefined + ] + +testMuxFixture :: IO Bool +testMuxFixture = do + source <- readFile "fixtures/mux.net" + case parseNetlist source of + Left _ -> check "mux fixture simulates selection and delay" False + Right netlist -> check "mux fixture simulates selection and delay" $ case + simulateWithScheduledInputs netlist + [("d0", Low), ("d1", High), ("sel", Low)] + [ (2, "sel", High) + , (4, "sel", Undefined) + , (6, "d0", High) + , (6, "d1", High) + , (8, "sel", TriState) + ] + 10 of + Right simulation -> + null (simulationFailures simulation) + && length (simulationAssertions simulation) == 9 + && valueAt simulation "y" 0 == Low + && valueAt simulation "y" 2 == High + && valueAt simulation "y" 4 == Undefined + && valueAt simulation "y" 6 == High + && valueAt simulation "delayed" 2 == Low + && valueAt simulation "delayed" 4 == High + && valueAt simulation "delayed" 6 == Undefined + && valueAt simulation "delayed" 8 == High + Left _ -> False + +testMuxBus :: IO Bool +testMuxBus = case parseNetlist (unlines + [ "input a[4]" + , "input b[4]" + , "input sel[4]" + , "output y[4]" + , "wire y[4]" + , "gate MUX choose (a,b,sel) -> y" + ]) of + Left _ -> check "MUX applies selection bitwise across a bus" False + Right netlist -> check "MUX applies selection bitwise across a bus" $ case + simulateWithInputs netlist + (busInputs "a" 9 4 ++ busInputs "b" 6 4 ++ busInputs "sel" 3 4) + 0 of + Right simulation -> + valueAt simulation "y[0]" 0 == Low + && valueAt simulation "y[1]" 0 == High + && valueAt simulation "y[2]" 0 == Low + && valueAt simulation "y[3]" 0 == High + Left _ -> False + +testGoldenMuxVCD :: IO Bool +testGoldenMuxVCD = do + source <- readFile "fixtures/mux.net" + golden <- readFile "fixtures/mux.golden.vcd" + let actual = do + netlist <- parseNetlist source + simulation <- simulateWithScheduledInputs netlist + [("d0", Low), ("d1", High), ("sel", Low)] + [ (2, "sel", High) + , (4, "sel", Undefined) + , (6, "d0", High) + , (6, "d1", High) + , (8, "sel", TriState) + ] + 10 + pure (renderVCD simulation) + check "mux VCD matches golden file" (actual == Right golden) + testGatesFixture :: IO Bool testGatesFixture = do source <- readFile "fixtures/gates.net" @@ -2506,6 +2656,9 @@ evalTwoState Xnor inputs = invertTwo (foldl' xorTwo Low inputs) evalTwoState Not inputs = case inputs of input : _ -> invertTwo input [] -> Low +evalTwoState Buf inputs = case inputs of + [input] -> if input == High then High else Low + _ -> Low evalTwoState Tribuf _ = Low xorTwo :: Logic -> Logic -> Logic @@ -2527,6 +2680,7 @@ propTwoStateMatchesReference (Known left) (Known right) = , evalGate Nor [left, right] == evalTwoState Nor [left, right] , evalGate Xnor [left, right] == evalTwoState Xnor [left, right] , evalGate Not [left] == evalTwoState Not [left] + , evalGate Buf [left] == evalTwoState Buf [left] ] propUndefinedCommutative :: Known -> Bool @@ -2556,6 +2710,26 @@ propTribufEnable (Known dataValue) = evalGate Tribuf [dataValue, Low] == TriState && evalGate Tribuf [dataValue, High] == dataValue +propBufferTruth :: FourState -> Bool +propBufferTruth (FourState value) = + evalGate Buf [value] == if value == TriState then Undefined else value + +propMuxTruth :: FourState -> FourState -> FourState -> Bool +propMuxTruth (FourState lowData) (FourState highData) (FourState select) = + evalGate Mux [lowData, highData, select] == expected + where + expected = case select of + Low -> normalize lowData + High -> normalize highData + Undefined -> commonValue + TriState -> commonValue + commonValue = + let normalizedLow = normalize lowData + normalizedHigh = normalize highData + in if normalizedLow == normalizedHigh then normalizedLow else Undefined + normalize TriState = Undefined + normalize value = value + propTribufFixtureSound :: Netlist -> Property propTribufFixtureSound netlist = forAll (elements [Low, High]) $ \dataValue ->